Advertisement

A First Step in the Translation of Alloy to Coq

  • Salwa SouafEmail author
  • Frédéric LoulergueEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11852)

Abstract

Alloy is both a formal language and a tool for software modeling. The language is basically first order relational logic. The analyzer is based on instance finding: it tries to refute assertions and if it succeeds it reports a counterexample. It works by translating Alloy models and instance finding into SAT problems. If no instance is found it does not mean the assertion is satisfied. Alloy relies on the small scope hypothesis: examining all small cases is likely to produce interesting counterexamples. This is very valuable when developing a system. However, Alloy cannot show their absence. In this paper, we propose an approach where Alloy can be used as a first step, and then using a tool we develop, Alloy models can be translated to Coq code to be proved correct interactively.

Keywords

First order relational logic Calculus of inductive construction Translation 

References

  1. 1.
    Arkoudas, K., Khurshid, S., Marinov, D., Rinard, M.: Integrating model checking and theorem proving for relational reasoning. In: Berghammer, R., Möller, B., Struth, G. (eds.) RelMiCS 2003. LNCS, vol. 3051, pp. 21–33. Springer, Heidelberg (2004).  https://doi.org/10.1007/978-3-540-24771-5_3CrossRefzbMATHGoogle Scholar
  2. 2.
    Blanchette, J.C., Nipkow, T.: Nitpick: a counterexample generator for higher-order logic based on a relational model finder. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 131–146. Springer, Heidelberg (2010).  https://doi.org/10.1007/978-3-642-14052-5_11CrossRefGoogle Scholar
  3. 3.
    Chlipala, A.: Certified Programming with Dependent Types. MIT Press, Cambridge (2014)zbMATHGoogle Scholar
  4. 4.
    Dennis, G.D.: A relational framework for bounded program verification. Ph.D. thesis, Massachusetts Institute of Technology (2009)Google Scholar
  5. 5.
    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).  https://doi.org/10.1007/978-3-540-71209-1_49CrossRefGoogle Scholar
  6. 6.
    Frappier, M., Fraikin, B., Chossart, R., Chane-Yack-Fa, R., Ouenzar, M.: Comparison of model checking tools for information systems. In: Dong, J.S., Zhu, H. (eds.) ICFEM 2010. LNCS, vol. 6447, pp. 581–596. Springer, Heidelberg (2010).  https://doi.org/10.1007/978-3-642-16901-4_38CrossRefGoogle Scholar
  7. 7.
    Geri, G., Indrakshi, R., Kyriakos, A., Behzad, B., Manachai, T., Siv, H.H.: An aspect-oriented methodology for designing secure applications. Inf. Softw. Technol. 51(5), 846–864 (2009)CrossRefGoogle Scholar
  8. 8.
    Glondu, S.: Towards certification of the extraction of Coq. Theses, Université Paris Diderot, June 2012Google Scholar
  9. 9.
    Jackson, D.: Automating first-order relational logic. In: ACM SIGSOFT International Symposium on Foundations of Software Engineering (FSE), pp. 130–139. ACM, New York (2000)Google Scholar
  10. 10.
    Jackson, D.: Software Abstractions, revised edn. MIT Press, Cambridge (2012)Google Scholar
  11. 11.
    Jackson, D., Vaziri, M.: Finding bugs with a constraint solver. In: Proceedings of the 2000 ACM SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2000, pp. 14–25. ACM, New York (2000)Google Scholar
  12. 12.
    Kang, E., Jackson, D.: Formal modeling and analysis of a flash filesystem in Alloy. In: Börger, E., Butler, M., Bowen, J.P., Boca, P. (eds.) ABZ 2008. LNCS, vol. 5238, pp. 294–308. Springer, Heidelberg (2008).  https://doi.org/10.1007/978-3-540-87603-8_23CrossRefGoogle Scholar
  13. 13.
    Kang, E., Jackson, D.O.: Designing and analyzing a flash file system with Alloy. Int. J. Softw. Inform. 3, 129–148 (2009)Google Scholar
  14. 14.
    Klein, G., et al.: seL4: formal verification of an operating-system kernel. Commun. ACM 53(6), 107–115 (2010)CrossRefGoogle Scholar
  15. 15.
    Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107–115 (2009)CrossRefGoogle Scholar
  16. 16.
    Marinov, D., Khurshid, S.: TesTera: a novel framework for automated testing of java programs. In: Proceedings 16th Annual International Conference on Automated Software Engineering (ASE 2001), pp. 22–31, November 2001Google Scholar
  17. 17.
    Moscato, M.M., Pombo, C.L., Frias, M.F.: Dynamite: a tool for the verification of Alloy models based on PVS. ACM Trans. Softw. Eng. Methodol. 23, 20:1–20:37 (2014)CrossRefGoogle Scholar
  18. 18.
    Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL — A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002).  https://doi.org/10.1007/3-540-45949-9CrossRefzbMATHGoogle Scholar
  19. 19.
    Paulin-Mohring, C.: Introduction to the calculus of inductive constructions. In: Woltzenlogel Paleo, B., Delahaye, D. (eds.) All about Proofs, Proofs for All. Studies in Logic (Mathematical logic and foundations), vol. 55. College Publications (2015)Google Scholar
  20. 20.
    Power, D., Slaymaker, M., Simpson, A.: Automatic conformance checking of role-based access control policies via Alloy. In: Erlingsson, Ú., Wieringa, R., Zannone, N. (eds.) ESSoS 2011. LNCS, vol. 6542, pp. 15–28. Springer, Heidelberg (2011).  https://doi.org/10.1007/978-3-642-19125-1_2CrossRefGoogle Scholar
  21. 21.
    Ramananandro, T.: Mondex, an electronic purse: specification and refinement checks with the Alloy model-finding method. Form. Asp. Comput. 20(1), 21–39 (2008)CrossRefGoogle Scholar
  22. 22.
    Seater, R., Jackson, D., Gheyi, R.: Requirement progression in problem frames: deriving specifications from requirements. Requir. Eng. 12(2), 77–102 (2007)CrossRefGoogle Scholar
  23. 23.
    Shao, D., Khurshid, S., Perry, D.E.: Whispec: white-box testing of libraries using declarative specifications. In: Proceedings of the 2007 Symposium on Library-Centric Software Design, LCSD 2007, pp. 11–20. ACM, New York (2007)Google Scholar
  24. 24.
    Song, D., et al.: Sok: Sanitizing for security. CoRR abs/1806.04355 (2018). http://arxiv.org/abs/1806.04355
  25. 25.
    Souaf, S., Berthomé, P., Loulergue, F.: A cloud brokerage solution: formal methods meet security in cloud federations. In: International Conference on High Performance Computing Simulation (HPCS). IEEE (2018)Google Scholar
  26. 26.
    The Coq Development Team: The Coq Proof Assistant. http://coq.inria.fr
  27. 27.
    Torlak, E.: A constraint solver for software engineering : finding models and cores of large relational specifications. Ph.D. thesis, Massachusetts Institute of Technology (2009)Google Scholar
  28. 28.
    Torlak, E., Taghdiri, M., Dennis, G., Near, J.: Applications and extensions of Alloy: past, present, and future. Math. Struct. Comput. Sci. 23, 915–933 (2013)MathSciNetCrossRefGoogle Scholar
  29. 29.
    Ulbrich, M., Geilmann, U., El Ghazi, A.A., Taghdiri, M.: A proof assistant for Alloy specifications. In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 422–436. Springer, Heidelberg (2012).  https://doi.org/10.1007/978-3-642-28756-5_29CrossRefzbMATHGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  1. 1.School of Informatics Computing and Cyber SystemsNorthern Arizona UniversityFlagstaffUSA
  2. 2.INSA Centre Val de Loire, LIFO EA 4022BourgesFrance

Personalised recommendations