Speaker
Description
Model-Based Systems/Software Engineering (MBSE) is an adopted development approach focusing on the correct construction and deployment of complex real-time critical systems. MBSE is provided by several commercial and/or open-source tools, such as TASTE. TASTE enables the system design, automatic generation of executables and validation. The aim of this activity is to equip TASTE with formal verification capabilities, by developing and integrating a model-checking approach for behavioural properties.
This activity has developed an open-source model-checker for TASTE based on the IF toolset. The technology has been integrated in the TASTE environment, creating a complete and useful development environment for real-time embedded applications.
More specifically:
- We defined a user-friendly model-checking workflow, seamlessly integrated in the TASTE environment and IDE.
- We defined a property language for formalizing requirements in TASTE. Three formalisms have been designed: Boolean Stop Condition for system invariants, Property Message Sequence Chart for (un-)desired system interactions, and Observer for complex properties monitoring and altering the system.
- We defined an approach to set the configuration for model-checking, in terms of subsystem subject to verification and available interactions with the environment (i.e., subtyping).
- We specified the model-checking approach preserving the TASTE semantics, via bi-directional model transformations to the IF toolset.
- We implemented the model-checking and validated it.
The technology has been validated on two case studies, one with the aim to assess the approach and another with the aim to identify the limitations. The case studies have showed the usefulness of the approach and tools, and the lessons learned are used in other activities involving the development of real-time embedded systems with TASTE.
Finally, the results of the activity have been disseminated in international venues and published in the TASTE documentation.
