Formal Model Engineering for Embedded Systems Using Real-Time Maude

Peter Csaba Ölveczky
(University of Oslo)

This paper motivates why Real-Time Maude should be well suited to provide a formal semantics and formal analysis capabilities to modeling languages for embedded systems. One can then use the code generation facilities of the tools for the modeling languages to automatically synthesize Real-Time Maude verification models from design models, enabling a formal model engineering process that combines the convenience of modeling using an informal but intuitive modeling language with formal verification. We give a brief overview six fairly different modeling formalisms for which Real-Time Maude has provided the formal semantics and (possibly) formal analysis. These models include behavioral subsets of the avionics modeling standard AADL, Ptolemy II discrete-event models, two EMF-based timed model transformation systems, and a modeling language for handset software.

Invited Presentation in Francisco Durán and Vlad Rusu: Proceedings Second International Workshop on Algebraic Methods in Model-based Software Engineering (AMMSE 2011), Zurich, Switzerland, 30th June 2011, Electronic Proceedings in Theoretical Computer Science 56, pp. 3–13.
Published: 29th June 2011.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: