(BA) Dataflow Notation for SAML

Betreuer: Michael Lipaczewski
Student: Robert Heumüller
Zeitraum:

Thesis:

Description:

The „System Analysis Modeling Language“ language was introduced by Matthias Güdemann as the core of a framework for model based safety analysis that he developed in his dissertation. The unique feature of this framework, compared to other model based systems, is SAML’s tool-independence. Instead of supplying an analysis software devoted to its own models, Güdemamn provided algorithms for the translation of SAML models into semantically equivalent NuSMV and PRISM models. This way both symbolic and probabilistic analyses of SAML models can be conducted. Since then, SAML has been further evolved in the scope of the VECS Project at Otto-von-Guericke University Magdeburg. On the one hand SAML has been enriched with many features, aiming to make the creation of complex models as efficient as possible. On the other hand, the modeling process still requires a large amount of expertise and care, because of the unfamiliar time semantics: In SAML all components of a model become active at once in every timestep. Most users are however accustomed to describing processes as series of ordered steps, similar to the description of algorithms. This paper introduces an extension to SAML, which allows a more intuitive approach based on the dataflow design paradigm. The fundamental idea of dataflow is that technical systems can be represented as a series of interconnected components. Each of the components realizes a dedicated function, comparable to an electronic circuit. (Input-)values flow through the components in the order dictated by the network. They are repeatedly transformed, finally producing the system’s output-values. Other analysis frameworks that support dataflow-driven model creation already exist today. Particularly for safety critical applications, e.g. in aeronautics, the verification of the deployed systems is essential. Esterel Scade is a prominent representative of tools used in this field. It features a graphical editor for its dataflow-based modeling language, as well as formal model verification and a certified code generator.

(BA) Dataflow Notation for SAML