AVATAR



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:
  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 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 testcase 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

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

  • 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.


Resources

Technical papers

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: