Abstract
To evaluate a property of the form ‘for all x there exists some y’ with a relational model finder requires a generator axiom to force all instances of y to exist in the universe of discourse. Without the generator axiom the model finder will produce a spurious counter-example by simply not including an important instance of y. Generator axioms are generally considered to be expensive to evaluate, significantly limiting the scope of the analysis. We demonstrate that evaluating the generator axiom in a separate stage from the property results in substantial improvements in analysis speed and scalability
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Abad, P., Aguirre, N., Bengolea, V., Ciolek, D., Frias, M.F., Galeotti, J.P., Maibaum, T., Moscato, M., Rosner, N., Vissani, I.: Improving Test Generation under Rich Contracts by Tight Bounds and Incremental SAT Solving. In: ICST 2013 (2013)
Biere, A.: Handbook of Satisfiability, vol. 185. Ios PressInc. (2009)
Cunha, A.: Bounded model checking of temporal formulas with Alloy. arXiv preprint arXiv:1207.2746 (2012)
Derrick, J., Fitzgerald, J., Gnesi, S., Khurshid, S., Leuschel, M., Reeves, S., Riccobene, E. (eds.): ABZ 2012. LNCS, vol. 7316. Springer, Heidelberg (2012)
Dietrich, D., Shaker, P., Atlee, J., Rayside, D., Gorzny, J.: Feature Interaction Analysis of the Feature-Oriented Requirements-Modelling Language Using Alloy. In: MoDeVVa Workshop at MODELS Conference (2012)
Dietrich, D., Shaker, P., Gorzny, J., Atlee, J., Rayside, D.: Translating the Feature-Oriented Requirements Modelling Language to Alloy. Tech. Rep. CS-2012-12, University of Waterloo, David R. Cheriton School of Computer Science (2012)
Eén, N., Sörensson, N.: An Extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2004)
Fraikin, B., Frappier, M., St-Denis, R.: Modeling the supervisory control theory with Alloy. In: Derrick, et al. (eds.) [4]
Galeotti, J.P., Rosner, N., López Pombo, C.G., Frias, M.F.: Analysis of Invariants for Efficient Bounded Verification. In: Tonella, P., Orso, A. (eds.) Proc. 19th ISSTA, pp. 25–36. ACM (2010)
Ganov, S., Khurshid, S., Perry, D.E.: Annotations for Alloy: Automated Incremental Analysis Using Domain Specific Solvers. In: Aoki, T., Taguchi, K. (eds.) ICFEM 2012. LNCS, vol. 7635, pp. 414–429. Springer, Heidelberg (2012)
Jackson, D.: Software Abstractions: Logic, Language, and Analysis. MIT Press (2011)
Khurshid, S., Marinov, D.: TestEra: Specification-based testing of Java programs using SAT. Automated Software Engineering 11(4), 403–434 (2004)
Khurshid, S., Marinov, D., Shlyakhter, I., Jackson, D.: A Case for Efficient Solution Enumeration. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 272–286. Springer, Heidelberg (2004)
Montaghami, V., Rayside, D.: Extending Alloy with partial instances. In: Derrick, et al. (eds.) [4]
Nelson, T., Barratt, C., Dougherty, D., Fisler, K., Krishnamurthi, S.: The Margrave tool for firewall analysis. In: Proceedings of the 24th International Conference on Large Installation System Administration, pp. 1–8. USENIX Association (2010)
Nelson, T., Dougherty, D.J., Fisler, K., Krishnamurthi, S.: Toward a more complete Alloy. In: Derrick, et al. (eds.) [4]
Toda, S.: On the computational power of PP and (+)P. In: 30th Annual Symposium on Foundations of Computer Science, pp. 514–519 (October 1989)
Torlak, E., Jackson, D.: Kodkod: A relational model finder. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 632–647. Springer, Heidelberg (2007)
Vakili, A., Day, N.A.: Temporal logic model checking in Alloy. In: Derrick, et al. (eds.) [4]
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Montaghami, V., Rayside, D. (2014). Staged Evaluation of Partial Instances in a Relational Model Finder. In: Ait Ameur, Y., Schewe, KD. (eds) Abstract State Machines, Alloy, B, TLA, VDM, and Z. ABZ 2014. Lecture Notes in Computer Science, vol 8477. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-43652-3_32
Download citation
DOI: https://doi.org/10.1007/978-3-662-43652-3_32
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-43651-6
Online ISBN: 978-3-662-43652-3
eBook Packages: Computer ScienceComputer Science (R0)