Top

Published in:

2018 | OriginalPaper | Chapter

CASM-IR: Uniform ASM-Based Intermediate Representation for Model Specification, Execution, and Transformation

Authors : Philipp Paulweber, Emmanuel Pescosta, Uwe Zdun

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

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

The Abstract State Machine (ASM) theory is a well-known formal method, which can be used to specify arbitrary algorithms, applications or even whole systems. Over the past years, there have been many approaches to implement concrete ASM-based modeling and specification languages. All of those approaches define their type systems and operator semantics differently in their internal representation, which leads to undesired or unexpected behavior during the modeling, the execution, and code generation of such ASM specifications. In this paper, we present CASM-IR, an Intermediate Representation (IR), designed to aid ASM-based language engineering which is based on a well-formed ASM-based specification format. Moreover, CASM-IR is conceptualized from the ground up to ease the formalization of ASM-based analysis and transformation passes. The feasibility of CASM-IR solving the uniform ASM representation problem is depicted. Based on our CASM-IR implementation, we were able to integrate a front-end of our statically inferred Corinthian Abstract State Machine (CASM) modeling language.

Dont have a licence yet? Then find out more about our products and how to get one now:

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!

inform now

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!

inform now

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!

inform now

previous chapter On B and Event-B: Principles, Success and Challenges

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

For ASM applications of various domains, see: http://web.eecs.umich.edu/gasm.

For CASM project website, see: http://casm-lang.org.

For CASM concrete syntax description, see: http://casm-lang.org/syntax.

For CASM-IR type specification, see: http://casm-lang.org/ir/types.

For CASM-IR built-in specification, see: http://casm-lang.org/ir/builtins.

For CASM-IR constant specification, see: http://casm-lang.org/ir/constants.

For CASM-IR function specification, see: http://casm-lang.org/ir/functions.

For CASM-IR instr. specification, see: http://casm-lang.org/ir/instructions.

For Asmeta project, see: http://asmeta.sourceforge.net.

For EMF project, see: http://eclipse.org/modeling/emf.

For CoreASM open-source project, see: http://github.com/coreasm.

For AsmL documentation and project, see: http://asml.codeplex.com.

For XASM documentation, see http://sourceforge.net/projects/xasm.

For CASM open-source project, see: http://github.com/casm-lang.

Gurevich, Y.: Evolving Algebras 1993: Lipari Guide - Specification and Validation Methods, pp. 9–36. Oxford University Press Inc., New York (1995)

Gurevich, Y.: Sequential abstract-state machines capture sequential algorithms. ACM Trans. Comput. Logic (TOCL) 1(1), 77–111 (2000)MathSciNetCrossRef

Börger, E.: The origins and the development of the ASM method for high level system design and analysis. J. Univ. Comput. Sci. 8(1), 2–74 (2002)

Stärk, R.F., Schmid, J., Börger, E.: Java and the Java Virtual Machine: Definition, Verification, Validation. Springer, Heidelberg (2001). https://doi.org/10.1007/978-3-642-59495-3CrossRefMATH

Sasaki, H.: A formal semantics for Verilog-VHDL simulation interoperability by abstract state machine. In: Proceedings of the Conference on Design, Automation and Test in Europe, DATE 1999. ACM, New York (1999)

Lezuo, R.: Scalable translation validation; tools, techniques and framework. Ph.D. thesis, Wien Technische Universität Dissertation (2014)

Barnett, M., Schulte, W.: Spying on components: a runtime verification technique. In: Proceedings of the Workshop on Specification and Verification of Component-Based Systems, SAVCBS 2001, pp. 7–13 (2001)

Glässer, U., Veanes, M.: Universal plug and play machine models. In: Kleinjohann, B., Kim, K.H., Kleinjohann, L., Rettberg, A. (eds.) Design and Analysis of Distributed Embedded Systems. ITIFIP, vol. 91, pp. 21–30. Springer, Boston, MA (2002). https://doi.org/10.1007/978-0-387-35599-3_3CrossRef

Huggins, J.K., Campenhout, D.V.: Specification and verification of pipelining in the ARM2 RISC microprocessor. ACM Trans. Des. Autom. Electron. Syst. (TODAES) 3(4), 563–580 (1998)CrossRef

10.

Kleppe, A.G.: Software Language Engineering: Creating Domain-Specific Languages using Metamodels. Addisson-Wesley, Boston (2009)

11.

Völter, M.: Generic tools, specific languages. Ph.D. thesis, Delft University of Technology, June 2014

12.

Lezuo, R., Paulweber, P., Krall, A.: CASM - optimized compilation of abstract state machines. In: SIGPLAN/SIGBED Conference on Languages, Compilers and Tools for Embedded Systems (LCTES), pp. 13–22. ACM (2014)

13.

Paulweber, P., Zdun, U.: A model-based transformation approach to reuse and retarget CASM specifications. In: Butler, M., Schewe, K.-D., Mashkoor, A., Biro, M. (eds.) ABZ 2016. LNCS, vol. 9675, pp. 250–255. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-33600-8_17CrossRef

14.

Gurevich, Y., Rossman, B., Schulte, W.: Semantic essence of AsmL: extended abstract. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2003. LNCS, vol. 3188, pp. 240–259. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-30101-1_11CrossRef

15.

Farahbod, R., Gervasi, V., Glässer, U.: CoreASM: an extensible ASM execution engine. Fundam. Inf. 77(1–2), 71–104 (2007)MathSciNetMATH

16.

Gargantini, A., Riccobene, E., Scandurra, P.: A metamodel-based language and a simulation engine for abstract state machines. J. Univ. Comput. Sci. 14(12), 1949–1983 (2008)

17.

Börger, E., Stärk, R.: Abstract State Machines: A Method for High-Level System Design and Analysis. Springer, Heidelberg (2003). https://doi.org/10.1007/978-3-642-18216-7CrossRefMATH

18.

Lattner, C., Adve, V.: LLVM: a compilation framework for lifelong program analysis & transformation. In: Code Generation and Optimization, pp. 75–86. IEEE (2004)

19.

Arcaini, P., Bonfanti, S., Dausend, M., Gargantini, A., Mashkoor, A., Raschke, A., Riccobene, E., Scandurra, P., Stegmaier, M.: Unified Syntax for abstract state machines. In: Butler, M., Schewe, K.-D., Mashkoor, A., Biro, M. (eds.) ABZ 2016. LNCS, vol. 9675, pp. 231–236. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-33600-8_14CrossRef

20.

Anlauff, M.: XASM- an extensible, component-based abstract state machines language. In: Gurevich, Y., Kutter, P.W., Odersky, M., Thiele, L. (eds.) ASM 2000. LNCS, vol. 1912, pp. 69–90. Springer, Heidelberg (2000). https://doi.org/10.1007/3-540-44518-8_6CrossRefMATH

21.

Lezuo, R., Krall, A.: Using the CASM language for simulator synthesis and model verification. In: Proceedings of the 2013 Workshop on Rapid Simulation and Performance Evaluation: Methods and Tools, p. 6. ACM (2013)

22.

Lezuo, R., Barany, G., Krall, A.: CASM: implementing an abstract state machine based programming language. In: Software Engineering (Workshops), pp. 75–90 (2013)

23.

Schmid, J.: Introduction to AsmGofer. http://www.tydo.de/AsmGofer (2001)

24.

Del Castillo, G.: The ASM workbench: a tool environment for computer-aided analysis and validation of abstract state machine models. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 578–581. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-45319-9_40CrossRef

25.

Schmid, J.: Compiling abstract state machines to C++. J. Univ. Comput. Sci. 7(11), 1068–1087 (2001)

26.

Bonfanti, S., Carissoni, M., Gargantini, A., Mashkoor, A.: Asm2C++: a tool for code generation from abstract state machines to arduino. In: Barrett, C., Davies, M., Kahsai, T. (eds.) NFM 2017. LNCS, vol. 10227, pp. 295–301. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-57288-8_21CrossRef

27.

Merrill, J.: GENERIC and GIMPLE: a new tree representation for entire functions. In: Proceedings of the 2003 GCC Developers’ Summit, pp. 171–179 (2003)

Title: CASM-IR: Uniform ASM-Based Intermediate Representation for Model Specification, Execution, and Transformation
Authors: Philipp Paulweber
Emmanuel Pescosta
Uwe Zdun
Publisher: Springer International Publishing
Book: Abstract State Machines, Alloy, B, TLA, VDM, and Z
Print ISBN: 978-3-319-91270-7

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

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

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner