PV3 ⊧ HybridSynchAADLchecks given requirements for HybridSynchAADL modelsModeling 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.
- Cyber-physical systems (CPSs)
- Synchronous systems
- Continuous systems
- Reachability analysis
- Symbolic reachability analysis
- Model of a synchronous cyber-physical system
- Specification/requirement to check
Expected outputDepends 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.
InternalsHybridSynchAADL (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:
- 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.
- Randomized simulation, which repeatedly executes the model until a counterexample of a requirement is found.
- Portfolio analysis which runs both previous methods in parallel and gives the results of the analysis that terminates first.