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

• Cyber-physical systems (CPSs)
• Synchronous systems
• Continuous systems
• Reachability analysis
• Symbolic reachability analysis
• Simulation

Expected input

• Model of a synchronous cyber-physical system
• Specification/requirement to check

Format:

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.

Internals

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:

• Constraints checking: validate that the model satisfies all the syntactic constraints of the modelling language
• Code generation: Synthesize Maude code from the model
• Formal analysis:
1. Symbolic reachability to verify that all possible behaviors satisfy a given requirement, if not then a counterexample is generated. This can guarantee the absence of a counterexample.
2. Randomized simulation, which repeatedly executes the model until a counterexample of a requirement is found.
3. Portfolio analysis which runs both previous methods in parallel and gives the results of the analysis that terminates first.

Extends SynchAADL

Comments

Note: HybridSynchAADL is an OSATE2 plugin