Analyzing Data Models Using Alloy Analyzer and SMT.ppt

We see that Z3 verification time extremely fast: less than .1 seconds on average. However not all properties gave an answer to the verification query (4 didn’t). So performed property-based projection. Then all properties gave an answer. However in general a property may not given an answer, even after projection since we are generating SMT-LIB specs in the theory of uninterpreted functions, which is undecidable. A disadvantage of unbounded verification, but not bounded. Thus can be used as complimentary approaches. But bounded verification, even for smallest bound of 10 objects took up to tens of seconds whereas Z3 took less than .1 seconds. * Bounded: We also see that the number of variables and verification time have exponential growth with respect to increasing bound, as expected. Although the number of variables in the SMT specification are not directly comparable to the figures produced by Alloy, we can still observe that the SMT formula size is much smaller than the one used by the SAT solver (tens vs hundreds). * Since Alloy specializes in the verification of object models, it is rather surprising that there is such a drastic difference between the verication times of Z3 and Alloy. There may be several reasons why unbounded verication did so well. Last bullet: Thus SMT solvers can use information about the structure and semantics of a formula to make inferences about satisfiability more accurately as well as more efficiently than a SAT-based approach which converts the verification to SAT formulas using a Boolean encoding. In fact, due to increasing size of the Boolean encoding, bounded verification suffers from an exponential increase in verication time with increasing bound. * * We can construct a formal data model representing the objects and their relationships in a RoR application. S is the data model schema, identifying the sets and relations of the data model, C is a set of relational constraints and D is a set of dependency constraints. Th