Safety and Security Checking of Real-Time Systems Modeled in SysML
Instructor
|
Ludovic Apvrille
Telecom Paris
France
|
|
|
|
Brief Bio
Ludovic Apvrille obtained his M.Sc. in Computer Science, Network and Distributed Systems specialization in 1998 from ENSEIRB and ISAE. He then completed a Ph.D. in 2002, in the Department of Applied Mathematics and Computer Science at ISAE, in collaboration with LAAS-CNRS and Alcatel Space Industries (now, Thalès Alenia Space). After a postdoctoral term at Concordia University (Canada), he joined LabSoc in 2003 as an assistant professor at Telecom ParisTech, in the Communication and Electronics department. He obtained his HDR (Habilitation à Diriger les Recherches) in 2012. His research interests focus on tools and methods for the modeling and verification of embedded systems and Systems-on-Chip. Verification techniques target both safety and security properties. He's the inventor and the main contributor of the open-source UML/SysML toolkit named TTool. He's the team leader of the LabSoC.
|
Abstract
The AVATAR modeling language tunes the OMG-based SysML for real-time systems modeling, simulation and formal verification using the open-source tool TTool. The tutorial surveys the language, demonstrates formal checking of model against safety and security properties, and guides participants in their first steps with TTool.
Detailed Outline:
1) Introduce AVATAR, a SysML-based language supported by the TTool tool.
* Notion of model, basics of SysML.
* AVATAR method: assumptions, requirements, analysis, design, prototyping.
* AVATAR design: syntax and semantics of AVATAR block, semantics of communication channels, state machines.
* How to efficiently model and verifiy a real-time system with AVATAR. This includes the simulation and verification capabilities of both safety and security properties.
2) Demonstration : A micro-wave oven is used to demonstrate the modeling and verification capabilities of TTool.
* The micro-wave design models are first sketched, in particular the model of the main controller, and how safety-related and security-related features are abstracted.
* Simulation of the model with animation * Formal verification of the model. We will there explain how to model safety and security properties, and how they can be proved with a press-button approach.
* Prototyping of the model in a virtual hardware environment. We will show how to automatically generate software code of the model, and how to execute that code on a virtual hardware platform, directly from TTool.
3) Practice!
* Participants are asked to come with their laptop (Windows, MacOS, Linux). They will progressively make their own model of a simple system, and they will be able to simulate it. In particular, they will see how easy it is to make a model and validate it with TTool.
Keywords
SysML, Real-Time, Simulation, Formal Verification, Safety, Security.
Aims and Learning Objectives
- Introduce AVATAR, a SysML-based language supported by the TTool tool
- Demonstrate the simulation and verification capabilities offered by TTool
- Invite the participants to model and simulate a system using TTool.
Target Audience
Students, researchers and industry practitioners.
Prerequisite Knowledge of Audience
Basic knowledge of SysML or UML would be an asset, but not being mandatory.
Detailed Outline
1) Introduce AVATAR, a SysML-based language supported by the TTool tool.
* Notion of model, basics of SysML.
* AVATAR method: assumptions, requirements, analysis, design, prototyping.
* AVATAR design: syntax and semantics of AVATAR block, semantics of communication channels, state machines.
* How to efficiently model and verifiy a real-time system with AVATAR. This includes the simulation and verification capabilities of both safety and security properties.
2) Demonstration : A micro-wave oven is used to demonstrate the modeling and verification capabilities of TTool.
* The micro-wave design models are first sketched, in particular the model of the main controller, and how safety-related and security-related features are abstracted.
* Simulation of the model with animation
* Formal verification of the model. We will there explain how to model safety and security properties, and how they can be proved with a
press-button approach.
* Prototyping of the model in a virtual hardware environment. We will show how to automatically generate software code of the model, and how
to execute that code on a virtual hardware platform, directly from TTool.
3) Practice!
* Participants are asked to come with their laptop (Windows, MacOS, Linux). They will progressively make their own model of a simple system,
and they will be able to simulate it. In particular, they will see how easy it is to make a model and validate it with TTool.
http://ttool.telecom-paristech.fr/tutorial_modelsward2015.html
Applying Model Driven Engineering Technologies in the Creation of Domain Specific Modeling Languages
Instructors
|
Bruce Trask
Executive,
United States
|
|
|
|
Brief Bio
Bruce Trask has been developing real world complex Distributed Real-Time Embedded systems for over 24 years specializing in MDE as applied to these systems in the last 10 years. He has been involved with the entire lifecycle of most of the projects he has participated in from conception, through requirements, through development, testing, integration, fielding and support. He has also been teaching Modeling, MDE, Object Orientation, Design Patterns, UML, C++, CORBA and Framework courses for over 10 years. He is a regular speaker/presenter at international software industry conferences. He has delivered tutorials at the OMG. Bruce Trask is the CEO of MDE Systems Inc.
|
|
Angel Roman
United States
|
|
|
|
Brief Bio
Angel Roman is the Chief Software Architect of MDE Systems and an expert on the Eclipse
Development environment and its application frameworks and modeling frameworks. He has presented at various industry conferences on topics such as Software Defined Radios and MDE Technologies. He has been involved with projects concerning MDE, Eclipse Development, Embedded Linux Systems and OSGi.
|
Abstract
Model Driven Engineering (MDE) brings together multiple technologies and critical innovations and formalizes them into the next wave of software development methods. This tutorial will cover the basic patterns, principles and practices of MDE. The three main MDE categories include the development of Domain Specific Languages (DSL), Domain Specific Editors (and Views), and Domain Specific Transformation Engines or Generators. Expressed in terms of language development technology, these mirror the development of the Abstract Syntax, Concrete Syntax and Semantics of a new Domain Specific Language. This tutorial will cover the basic effective patterns, principles and practices for developing these MDE software artifacts. The tutorial will show how to apply these concepts as effective means with which to both raise levels of abstraction and domain specificity and thus increase power and value of tools and languages that allow developers to tackle the complexities of today’s software systems. It will also show how to effectively leverage abstraction without sacrificing the ability to robustly and precisely refine these abstractions to solve complex real world problems. To show these patterns and principles in action, this tutorial will cover the details of how to leverage MDE Language Workbenches and frameworks in support of robust software development.
Examples of General Purpose Programming Languages and Modeling tools failing to provide sufficient power in the face of increasing platform and system complexity abound. Model Driven Engineering has shown to be an effective means with which to both raise levels of abstraction and domain specificity and thus increase power and value of tools and languages that allow developers to tackle this complexity. With Model Driven Engineering one can effectively leverage abstraction without sacrificing the ability to robustly and precisely refine these abstractions to solve real world problems. These techniques are particularly applicable to many of today’s distributed applications some of which can be described as embedded, real-time, distributed, object-oriented, portable, heterogeneous, multithreaded, high performance, dynamic, resource-constrained, safety-critical, secure, networked, component based, faulttolerant and dynamic. Tackling these systems requires a maximum of tooling and language technology. As with any software solution, Model Driven Engineering itself however introduces new complexities. This tutorial will discuss what these are and how to address them in a way that allows Model Driven Engineering approaches to be the viable next wave for software development.