Using model checking to analyze static properties of declarative models

ASE, pp. 428-431, 2011.

Cited by: 1|Bibtex|Views4|DOI:https://doi.org/10.1109/ASE.2011.6100090
EI
Other Links: dl.acm.org|dblp.uni-trier.de|academic.microsoft.com

Abstract:

We show how static properties of declarative models can be efficiently analyzed in a symbolic model checker; in particular, we use Cadence SMV to analyze Alloy models by translating Alloy to SMV. The computational paths of the SMV models represent interpretations of the Alloy models. The produced SMV model satisfies its LTL specifications...More

Code:

Data:

Your rating :
0

 

Tags
Comments