AVATAR

AVATAR stands for Automated Verification of reAl Time softwARe.

AVATAR targets the modeling and formal verification of real-time embedded systems.

methodological phases of AVATAR:

1. Requirement capture. Requirements and properties are structured using AVATAR Requirement Diagrams. At this step, properties are just defined with a specific label.


2. Assumption modeling. Assumptions of the system may be captured with an assumption modeling diagram, based on a SysML requirement diagram.


3. System analysis. A system may be analyzed using usual UML diagrams, such as Use Case Diagrams, Interaction Overview Diagrams (Supported by UML2, not by SysML) and Sequence Diagrams.


4. System design. The system is designed in terms of communicating SysML blocks described in an AVATAR Block Diagram, and in terms of behaviors described with AVATAR State Machines.


5. Property modeling. The formal semantics of properties is defined within TEPE Parametric Diagrams (PDs). Since TEPE PDs involve elements defined in system design (e.g., a given integer attribute of a block), TEPE PDs may be defined only after a first system design has been performed.


6. Formal verification can be conducted over the system design, and for each test case defined in the Requirement Diagram.


7. Code generation can finally be used to generate a fully executable code. The latter can be compiled and executed on the SoCLib prototyping platform directly from TTool, or executed on your local host if the latter supports gcc and POSIX.

---

How to start?

Documentation

I suggest you start with the first two videos and the tutorial.

• My first Avatar model (video): how to make an AVATAR design, and how to perform simulations.


• Safety verification of Avatar models (video): how to perform formal safety verification from Avatar TTool models with the internal verifier of TTool


• This tutorial on AVATAR basics should help you to start as well.


• Advanced concepts on the Avatar model checker.


• If you wish to use UPPAAL for formal verification and not the internal verifier of TTool: Safety verification of Avatar models with UPPAAL (video). Note: you must have UPPAAL installed and configured on your computer to use UPPAAL as a verifier.


• C code generation from Avatar models (video): how to enhance model with user code, how to generate code, how to pilot the generated code from a GUI, how to trace the execution of the generated code. This tutorial on code generation should help you as well.


• These guided labs shall help you to start with AVATAR


• Modeling with AVATAR


• Validation with AVATAR


• Code generation from AVATAR models

Examples of AVATAR models

(save the xml files in your account, and open them with TTool)

• Coffee machine modeled with AVATAR (open the file with TTool)


• Client / server system modeled with AVATAR (open the file with TTool)


• Microwave oven modeled with AVATAR (open the file with TTool). The model addresses both safety and security constraints. C code generation is also shown in this model.


• Use of synchronous broadcast channels modeled with AVATAR (open the file with TTool). One broadcast channel has been used between a sender and two receivers. In the AVATAR simulation, you may observe that depending on the time value selected by the simulator, the message may be either lost, received only by receiver 1, or received by both receivers.


• Use of constant values in AVATAR designs.

---

Resources

Technical papers

• Paper on the TEPE Property language . This paper also briefly presents AVATAR. Published at UMLFM'2010.


• Paper on the proof of security properties . This paper also briefly presents AVATAR. Published at NOTERE'2011.


• Paper on code generation and virtual prototyping. Published and presented at ERTS 2012.

Presentations

• Slides presented at SysML France day, Feb. 2014


• Slides presented at ERTSS 2012 France


• Slides presented at UMLFM'2010


• Presentation on AVATAR given at the SysML Days, Paris, the 6th of December, 2010 (in French)


• Presentation on AVATAR. This presentation includes all methodological phases


• Movie presenting AVATAR code generation capabilities (30 Mo)

Configuration

If you wish to:

• Make proofs of safety properties from AVATAR models, you need to install and configure UPPAAL


• Make proofs of security properties from AVATAR models, you need to install and configure ProVerif


• Generate, compile and execute prototyping code from AVATAR models, you need to install and configure a C compiler


• Generate, compile and execute prototyping code on the SoCLib/MutekH platform from AVATAR models, you need to install and configure SoCLib and MutekH