nach oben

Erschienen in:

2018 | OriginalPaper | Buchkapitel

A Translation from Alloy to B

verfasst von : Sebastian Krings, Joshua Schmidt, Carola Brings, Marc Frappier, Michael Leuschel

Erschienen in: Abstract State Machines, Alloy, B, TLA, VDM, and Z

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

In this paper, we introduce a translation of the specification language Alloy to classical B. Our translation closely follows the Alloy grammar, each construct is translated into a semantically equivalent component of the B language. In addition to basic Alloy constructs, our approach supports integers and orderings. The translation is fully automated by the tool “Alloy2B”. We evaluate the usefulness by applying AtelierB and ProB to the translated models, and show benefits for proof and solving with integers and higher-order quantification.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel Event-B Expression and Verification of Translation Rules Between SysML/KAOS Domain Models and B System Specifications

Nächstes Kapitel Extracting Symbolic Transitions from TLA Specifications

For the sake of readability, the example translation uses the same identifiers as the Alloy module. Of course, one has to ensure the translation is valid, e.g., identifiers do not collide with B’s keywords.

Let expressions are available in an extended version of B understood by ProB.

Quantifiers are used for typing but do not enforce restrictions on possible models.

CLP(FD) overflows are caught and handled by custom implementation.

Analysis cannot be performed since it requires higher-order quantification that could not be skolemized.

Abrial, J.-R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, New York (1996)CrossRef

Carlsson, M., Ottosson, G., Carlson, B.: An open-ended finite domain constraint solver. In: Glaser, H., Hartel, P., Kuchen, H. (eds.) PLILP 1997. LNCS, vol. 1292, pp. 191–206. Springer, Heidelberg (1997). https://doi.org/10.1007/BFb0033845CrossRef

ClearSy: Atelier B, User and Reference Manuals. Aix-en-Provence, France (2009). http://www.atelierb.eu/

Cunha, A.: Bounded model checking of temporal formulas with Alloy. In: Ait Ameur, Y., Schewe, K.D. (eds.) ABZ 2014. LNCS, vol. 8477, pp. 303–308. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-662-43652-3_29CrossRef

Frias, M.F., Galeotti, J.P., Pombo, C.L., Aguirre, N.: DynAlloy: upgrading alloy with actions. In: Proceedings of the ICSE, pp. 442–451 (2005)

Frias, M.F., Pombo, C.L., Galeotti, J.P., Aguirre, N.: Efficient analysis of DynAlloy specifications. ACM Trans. Softw. Eng. Methodol. 17(1), 4:1–4:34 (2007)CrossRef

Ghazi, A.A.E., Taghdiri, M.: Analyzing alloy formulas using an SMT solver: a case study. CoRR, abs/1505.00672 (2015)

Hansen, D., Leuschel, M.: Translating TLA⁺ to B for validation with ProB. In: Derrick, J., Gnesi, S., Latella, D., Treharne, H. (eds.) IFM 2012. LNCS, vol. 7321, pp. 24–38. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-30729-4_3CrossRef

Jackson, D.: Alloy: a lightweight object modelling notation. ACM Trans. Softw. Eng. Methodol. 11, 256–290 (2002)CrossRef

10.

Jackson, D.: Software Abstractions: Logic, Language and Analysis. MIT Press, Cambridge (2006)

11.

Jaffar, J., Michaylov, S.: Methodology and implementation of a CLP system. In: Proceedings ICLP, pp. 196–218. MIT Press (1987)

12.

Krings, S., Leuschel, M.: Constraint logic programming over infinite domains with an application to proof. In: Proceedings of WLP. Electronic Proceedings in Theoretical Computer Science, EPTCS, vol. 234 (2016)

13.

Krings, S., Leuschel, M.: SMT solvers for validation of B and Event-B models. In: Ábrahám, E., Huisman, M. (eds.) IFM 2016. LNCS, vol. 9681, pp. 361–375. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-33693-0_23CrossRef

14.

Krings, S., Leuschel, M.: Proof assisted bounded and unbounded symbolic model checking of software and system models. Sci. Comput. Program. 158, 41–63 (2017)CrossRef

15.

Krings, S., Leuschel, M., Körner, P., Hallerstede, S., Hasanagić, M.: Three is a crowd: SAT, SMT and CLP on a chessboard. In: Calimeri, F., Hamlen, K., Leone, N. (eds.) PADL 2018. LNCS, vol. 10702, pp. 63–79. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-73305-0_5CrossRef

16.

Leuschel, M., Bendisposto, J., Dobrikov, I., Krings, S., Plagge, D.: From animation to data validation: the ProB constraint solver 10 years on. In: Boulanger, J.-L. (ed.) Formal Methods Applied to Complex Systems: Implementation of the B Method, pp. 427–446. Wiley ISTE, Hoboken (2014)

17.

Leuschel, M., Butler, M.: ProB: a model checker for B. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 855–874. Springer, Heidelberg (2003). https://doi.org/10.1007/978-3-540-45236-2_46CrossRef

18.

Leuschel, M., Butler, M.: ProB: an automated analysis toolset for the B method. Int. J. Softw. Tools Technol. Transf. 10(2), 185–203 (2008)CrossRef

19.

Macedo, N., Cunha, A.: Alloy meets TLA+: an exploratory study. CoRR, abs/1603.03599 (2016)

20.

Malik, P., Groves, L., Lenihan, C.: Translating Z to Alloy. In: Frappier, M., Glässer, U., Khurshid, S., Laleau, R., Reeves, S. (eds.) ABZ 2010. LNCS, vol. 5977, pp. 377–390. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-11811-1_28CrossRef

21.

Matos, P.J., Marques-Silva, J.: Model checking Event-B by encoding into Alloy. In: Börger, E., Butler, M., Bowen, J.P., Boca, P. (eds.) ABZ 2008. LNCS, vol. 5238, p. 346. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-87603-8_34CrossRef

22.

Meng, B., Reynolds, A., Tinelli, C., Barrett, C.: Relational constraint solving in SMT. In: de Moura, L. (ed.) CADE 2017. LNCS, vol. 10395, pp. 148–165. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-63046-5_10CrossRef

23.

Mikhailov, L., Butler, M.: An approach to combining B and Alloy. In: Bert, D., Bowen, J.P., Henson, M.C., Robinson, K. (eds.) ZB 2002. LNCS, vol. 2272, pp. 140–161. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45648-1_8CrossRef

24.

Milicevic, A., Jackson, D.: Preventing arithmetic overflows in Alloy. Sci. Comput. Program. 94, 203–216 (2014)CrossRef

25.

Milicevic, A., Near, J.P., Kang, E., Jackson, D.: Alloy*: a general-purpose higher-order relational constraint solver. In: Formal Methods in System Design, January 2017

26.

Near, J.P., Jackson, D.: An imperative extension to Alloy. In: Frappier, M., Glässer, U., Khurshid, S., Laleau, R., Reeves, S. (eds.) ABZ 2010. LNCS, vol. 5977, pp. 118–131. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-11811-1_10CrossRef

27.

Plagge, D., Leuschel, M.: Validating Z specifications using the ProB animator and model checker. In: Davies, J., Gibbons, J. (eds.) IFM 2007. LNCS, vol. 4591, pp. 480–500. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-73210-5_25CrossRef

28.

Plagge, D., Leuschel, M.: Validating B,Z and TLA⁺ using ProB and Kodkod. In: Giannakopoulou, D., Méry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 372–386. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-32759-9_31CrossRef

29.

Sülflow, A., Kühne, U., Wille, R., Große, D., Drechsler, R.: Evaluation of SAT-like proof techniques for formal verification of word-level circuits. In: Proceedings IEEE WRTLT, Beijing, China. IEEE Computer Society Press, October 2007

30.

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_49CrossRef

31.

Torlak, E., Taghdiri, M., Dennis, G., Near, J.P.: Applications and extensions of Alloy: past, present and future. Math. Struct. Comput. Sci. 23(4), 915–933 (2013)MathSciNetCrossRef

32.

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_29CrossRefMATH

Titel: A Translation from Alloy to B
verfasst von: Sebastian Krings
Joshua Schmidt
Carola Brings
Marc Frappier
Michael Leuschel
Verlag: Springer International Publishing
Buch: Abstract State Machines, Alloy, B, TLA, VDM, and Z
Print ISBN: 978-3-319-91270-7

Electronic ISBN: 978-3-319-91271-4

Copyright-Jahr: 2018
DOI: https://doi.org/10.1007/978-3-319-91271-4_6

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"