PV3 HybridSynchAADLchecks given requirements for HybridSynchAADL models

Modeling language and formal analysis tool for virtually synchronous cyber-physical systems with complex control programs, continuous behaviors, bounded clock skews, network delays, and execution times.

Application domain/field

Expected input


HybridSynchAADL model

Expected output

Depends on the analysis that is chosen. It can check whether the model is well-formed. The formal analyses might give a counterexample if the specification is not satisfied.


HybridSynchAADL (the language) is a subset of the avionics modeling standard AADL and its behavioral annex to model control programs, and captures a synchronous subset of AADL with continuous behaviors. The formal analysis is done using a combination of Maude and Yices. It can do symbolic reachability analysis and randomized simulation. Symbolic reachability analysis can verify that all possible behaviors satisfy a given requirement, if not then a counterexample is generated. Randomized simulation repeatedly executes the model until a counterexample is found. The user can specify time-bounded invariant and reachability properties that should be checked. The tool can be used to do the following things: Extends SynchAADL


Note: HybridSynchAADL is an OSATE2 plugin
Simulation Synthesis


Related papers

Hybrid SynchAADL: Modeling and Formal Analysis of Virtually Synchronous CPSs in AADL (CAV '21)

Last publication date

15 July 2021

ProVerB specific

ProVerB is a part of SLEBoK. Last updated: February 2023.