Model-based design of cyber physical systems
Marco Di Natale, Scuola Superiore Sant Anna of Pisa, Italy
Pieter Mosterman - The Mathworks
(Schedule -with times- subject to change)
SESSION 1: Modeling
Jim Tung - MathWorks (1:30pm - 2:00pm)
Introduction to Model-Based Design of Cyber-Physical Systems
This presentation discusses the key concepts and specific modeling, analysis,
and code generation techniques used in Model-Based Design to design, develop, and verify a complex system.
The talk will use an automotive control system as a primary example,
though the presentation will also discuss issues that arise in other types of systems. Slides (pdf)
Pieter J. Mosterman - MathWorks (2:00pm - 2:30pm)
Heterogeneous Models in Model-Based Design
Break (2:30pm - 2:45pm)
The use of computational models to design engineered systems has become indispensable.
A model is a system that represents another system where the model contains less detail
than the system it represents with the intent to solve a particular problem.
The range of problems that must be tackled in design combined with the broadly
varying levels of detail that are necessary in the corresponding models
invariably leads to heterogeneity in many forms across model syntax and semantics.
This presentation introduces the execution
semantics found in Model-Based Design tools such as Simulink, Stateflow, SimEvents, and Simscape.
The semantics are compared and
contrasted and challenges in combining the different semantics are highlighted. Slides (pdf)
SESSION 2: Verification
Rajeev Alur - University of Pennsylvania
(2:45pm - 3:15pm)
Formal Verification of Hybrid Systems
In formal verification, a designer first constructs a model, with mathematically
precise semantics, of the system under design, and performs extensive analysis with
respect to correctness requirements. The appropriate mathematical model for embedded
control systems is hybrid systems that combines the traditional state-machine based models
for discrete control with classical differential-equations based models for continuously
evolving physical activities. In this talk, we briefly review selected existing approaches
to formal verification of hybrid systems, along with directions for future research. Slides (pdf)
Stefano Tonetta - Fondazione Bruno Kessler
(3:15pm - 3:45pm)
NuSMV support to model-based design of safety-critical systems
Model checking with NuSMV has been successfully applied to support the verification of
safety-critical systems by different industrial companies.
The model checker is used as back-end in CASE tools where semantics-preserving
translations allow to verify front-end languages such as MATLAB, Stateflow, Simulink, and AADL.
We will overview the different functionalities
that this model-based approach offers including verification of functional
requirements, requirements validation, and safety assessment. We will show how the
advancements in SMT-based formal verification allows to apply this technology to
infinite-state systems with discrete-time or continuous dynamics. Slides (pdf)
Zhi Han - MathWorks
(3:45pm - 4:15pm)
Accelerating Model-Based Development with Integrated Formal Verification using Simulink Design Verifier
Break (4:15pm - 4:30pm)
Design of complex cyber-physical systems such as automobiles, airplanes, and satellites is a multifaceted task. Model-Based Design has gained much popularity by providing visual abstractions for controller design and useful functionalities such as automatic synthesis of high quality embedded code. In environments for Model-Based Design, models serve the same purpose as C/C++ code has served in the past. With numerical simulations and formal analysis techniques based on simulation, Model-Based Design tools such as Simulink and Stateflow provide valuable early verification, leading to their widespread use in the embedded systems industry. While simulation remains a useful tool, formal verification techniques have shown their advantage in their exhaustive nature and the soundness of the results they produce. In this talk we will discuss Simulink Design Verifier, a formal verification tool seamlessly integrated with the Simulink/Stateflow modeling environment. We will first discuss the design principle of Simulink Design Verifier and present a few workflows for using formal verification in numerical simulation software. Then we will take some time to explore several different workflows for using Simulink Design Verifier: design error detection for common misuses and runtime exceptions, test generation for design understanding, and property proving for guaranteeing correctness of safety properties. We will also discuss the formal verification technologies used by Simulink Design Verifier and how they are integrated to provide a fully automated verification tool. The talk will conclude with a few remarks on future investments based on feedback from lead industry adopters of formal verification tools.
SESSION 3: Task Implementation
Marco Di Natale - Scuola Superiore S. Anna.
(4:30pm - 5:00pm)
Task Models and Wait-free Protocols for Flow-preserving Implementations of Simulink Models
In the model-based development of software systems, the input of the process
is a functional model, typically described according to a synchronous reactive formalism,
as in Simulink. The software implementation and the task structure originate from this model
as the result of a synthesis (code-generation) process.
Hence, tasks are not provided in advance, but are defined by the designer or
generated by a synthesis algorithm with the constraint that the semantic
properties of the model (communication flows) are preserved.
In this talk, we outline the constraints that apply to the synthesis process and we
describe how real-time analysis is a necessary tool for the definition of
communication mechanisms that preserve the semantics of the functional model and
for the construction of an efficient (possibly optimal) task model.
We discuss challenges and solutions for the definition of the task and
communication implementations for single-core, multicore and distributed execution platforms.