AVATAR stands for Automated Verification of reAl Time softwARe.
AVATAR targets the modeling and formal verification of real-time embedded systems.
The AVATAR profile reuses eight of the SysML diagrams (Package diagrams are not supported). AVATAR supports the following methodological phases:
- Requirement capture. Requirements and properties are structured using AVATAR Requirement Diagrams. At this step, properties are just defined with a specific label.
- Assumption modeling. Assumptions of system may be captured with an assumption modeling diagram, based on a SysML requirement diagram.
- 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.
- 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.
- 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.
- Formal verification can be conducted over the system design, and for each testcase defined in the Requirement Diagram.
- 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?
- Hello world system: explanations on how to make an AVATAR design, and how to perform simulations and formal verification from an AVATAR design
- These two 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 models adresses both safety and security constraints. C code generation is also shown is this model.
- Use of synchronous broadcast channels modeled with AVATAR (open the file with TTool). One broacast channel has been used between a sender and two receivers. In the AVATAR simulation, you may observe that depending on the time value which is selected by the simulator, the message may be either lost, received only by the receiver 1, or received by the two receivers.
- Use of constant values in AVATAR designs.
- 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.
- 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)
ConfigurationIf 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