All the material (slides, models) are released with a CC BY-NC-SA 4.0 license.

ModelsWard'2015 Tutorial: Safety and Security Checking of Real-Time Systems Modeled in SysML

AVATAR targets the modeling and formal verification of real-time embedded systems. The tutorial intends to explain the main interest of Avatar for capturing safety and security constraints, and for performing safety and security-related formal proofs. The tutorial will be as follows:

1. Main Avatar feature. Slides.


2. Demonstration of Avatar/TTool. A full model will be presented (e.g., a microwave oven): requirements, analysis, design, code generation, and formal proofs.


3. Practise. You will be assisted to start making a first Avatar design with TTool, on your own laptop. Do install TTool before coming to the tutorial. You may also want to install UPPAAL and Proverif to perform safety and security proofs, but we won't have the time to make such proofs during the tutorial.

---

Resources

• Downloading and then installing TTool


• Avatar


• Tutorial information on the Modelsward'2015 website