Formal Model Engineering for Embedded Systems Using Real-Time Maude

TL;DR

This paper advocates using Real-Time Maude for formal semantics and analysis of embedded systems modeling languages, enabling automatic synthesis of verification models from design models for improved formal model engineering.

Contribution

It demonstrates how Real-Time Maude can provide formal semantics and analysis for diverse embedded system modeling formalisms, facilitating formal verification from informal models.

Findings

Real-Time Maude supports formal semantics for six different modeling formalisms.

It enables automatic synthesis of verification models from design models.

The approach enhances formal model engineering for embedded systems.

Abstract

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.