Model-based design of cyber physical systems

Organizers:
Marco Di Natale, Scuola Superiore Sant Anna of Pisa, Italy
Pieter Mosterman - The Mathworks

Program

(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
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)

Break     (2:30pm - 2:45pm)

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
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. Slides (pdf)

Break     (4:15pm - 4:30pm)

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. Slides (pdf)