# 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:
*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.