Iulia Dragomir

I Dragomir, M Bozga, Iulian Ober et al.

Model-Based Systems Engineering (MBSE) is a development approach aiming to build correct-by-construction systems, provided the use of clear, unambiguous and complete models to describe them along the design process. The approach is supported by several engineering tools that automate the development steps, for example the production of code, documentation, test cases and more. TASTE [1] is pragmatic MBSE toolset supported by ESA that encapsulates several technologies to design a system (data modelling, architecture modelling, behaviour modelling/implementation), to automatically generate the binary application(s), and to validate it. One topic left open in TASTE is the formal verification of a system design with respect to specified properties. In this paper we describe our approach based on the IF model-checker [4] to enable the formal verification of properties on TASTE designs. The approach is currently under development in the ESA MoC4Space project.

Iulia Dragomir, Viorel Preoteasa, Stavros Tripakis

We present the Refinement Calculus of Reactive Systems Toolset, an environment for compositional modeling and reasoning about reactive systems, built on top of Isabelle, Simulink, and Python.

Viorel Preoteasa, Iulia Dragomir, Stavros Tripakis

Simulink is a de-facto industrial standard for the design of embedded systems. In previous work, we developed a compositional analysis framework for Simulink models in Isabelle -- the Refinement Calculus of Reactive Systems (RCRS), which allows checking compatibility and substitutability of components. However, standard type checking was not considered in that work. In this paper we present a method for the type inference of hierarchical block diagrams using the Isabelle theorem prover. A Simulink diagram is translated into an (RCRS) Isabelle theory. Then the Isabelle's powerful type inference mechanism is used to infer the types of the diagram based on the types of the basic blocks. One of the aims is to handle formally as many diagrams as possible. In particular, we want to be able to handle even those diagrams that may have typing ambiguities, provided that they are accepted by Simulink. This method is implemented in our toolset that translates Simulink diagrams into Isabelle theories and simplifies them. We evaluate our technique on several case studies, most notably, an automotive fuel control system benchmark provided by Toyota.

Iulia Dragomir, Viorel Preoteasa, Stavros Tripakis

Simulink is the de facto industrial standard for designing embedded control systems. When dealing with the formal verification of Simulink models, we face the problem of translating the graphical language of Simulink, namely, hierarchical block diagrams (HBDs), into a formalism suitable for verification. In this paper, we study the translation of HBDs into the compositional refinement calculus framework for reactive systems. Specifically, we consider as target language an algebra of atomic predicate transformers to capture basic Simulink blocks (both stateless and stateful), composed in series, in parallel, and in feedback. For a given HBD, there are many possible ways to translate it into a term in this algebra, with different tradeoffs. We explore these tradeoffs, and present three translation algorithms. We report on a prototype implementation of these algorithms in a tool that translates Simulink models into algebra terms implemented in the Isabelle theorem prover. We test our tool on several case studies including a benchmark Simulink model by Toyota. We compare the three translation algorithms, with respect to size and readability of generated terms, simplifiability of the corresponding formulas, and other metrics.