aadl2sync

Architecture Description Languages (ADL) aim at defining systems by describing jointly software and hardware components and their interactions. ADL can describe functional interfaces to components and non-functional aspects (reliability, availability, timing, responsiveness, etc.). The objective is to be able to perform various analysis (schedulability, sizing analysis, safety analysis) very early in the development process. AADL (Architecture Analysis and Design Language) is one such ADL, that specifically targets real time embedded systems. It lets one describe the structure of such systems as an arborescent assembly of software components mapped onto an execution platform. The leaves of that arborescent description are made of component interfaces that are left un-implemented.

Given an AADL model and implementations for the component leaves, the aadltosync allows one to perform automatically simulation and formal verification. This is done by translating the AADL model into the Lustre programming language, for which simulation and formal verification tools exist. This tool chain allows one to focus on functional properties far before machine code generation and deployment phases. The main difficulty in this translation is to model intrinsically non-deterministic and a-synchronous AADL descriptions into a synchronous language. To do that, we use techniques based on sporadic activation condition (stuttering)[milner83], input addition (oracles), and quasi-synchronous clocks [caspi01].

  Publications

ACSD 2006 Simulation and verification of asynchronous systems by means of a synchronous model. Nicolas Halbwachs, Louis Mandel - Sixth International Conference on Application of Concurrency to System Design, ACSD 2006

EMSOFT’07 N. Halbwachs, E. Jahier, P. Raymond, X. Nicollin, D. Lesens Virtual execution of AADL models via a translation into synchronous programs Seventh International Conference on Embedded Software (EMSOFT 2007), September 30 - October 5, 2007 Salzburg, Austria

[TR-2008-10] Erwan Jahier, Nicolas Halbwachs, Pascal Raymond: Synchronous modeling and validation of schedulers dealing with shared resources, Verimag Technical Report number TR-2008-10, Jul 2008.x - also published in FASE’09

  Distribution

You can download the aadl2sync current version:

• PC/Linux: aadl2sync-0.31-linux.tgz
• PC/Cygwin: aadl2sync-0.31-cygwin.tgz

This distribution has been compiled for PC/Linux and PC/Cygwin architectures. But I should be able to provide other configurations (sparc/solaris, mac/PC, ...) of it if anyone wishes.

Note that the current version of the tool a beta version, which works on the couple of examples I’ve tried on. An example (with a Makefile) is included in the tarball.

More information is available in The aadl2sync Reference Manual .

  Change log

• PC/Linux version (24/01/2008)
  <a href="http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/aadl2sync/aadl2sync-0.31-cygwin.tgz"> PC/Cygwin version
  • A few bug fixes.

    
    

• aadl2sync-0.30-linux.tgz (26/07/2007)
  • Add a "—check-schedulability" option that adds an additional boolean output (schedul_ok) that is true as long as no dead-line is missed.

    
    

• aadl2sync-0.29-linux.tgz (25/07/2007)
  • Add support for delayed connections in the parser ("->>").
  • Reorder scheduling variables to match the corresponding component order in the aadl file. Give better name to scheduling variables. For instance, rename all the scheduling variables needs* by dispatched*, as it corresponds to the AADL standard terminology.
  • Use the quasi-synchonous clocks as real clocks (via current/when operators) instead of simulating the clock mechanism with boolean operators («qs_tick and ...»).

    
    

• aadl2sync-0.28-linux.tgz (19/06/2007)
  • Fix a bug in the generated scheduler: for 2 threads on the same processor, the compute execution time of the first was attributed to the second, and vice-versa.

    
    

• aadl2sync-0.27-linux.tgz (21/05/2007)
  • AADL components does are not required to be inside a package anymore.
    
  • Better error messages.
    
• aadl2sync-0.26-linux.tgz (10/05/2007)
  • New options are implemented:
    —scade to generate Scade compatible Lustre
    —one-file to generate 1 file instead of 6
    —v4-array to generate Lustre V4 arrays (versus expanded code)
  • Moreover, the arrays used for quasi-synchronous clocks are now expanded (in order to avoid the dependance on Lustre V4 array syntax). The old behavior can be obtained via the —v4-array option.
• aadl2sync-0.25-linux.tgz (3/05/2007)
• aadl2sync-0.24-linux.tgz (27/04/2007)