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

HybridSynchAADL leverages the Hybrid PALS equivalence, so that it is sufficient to model and verify the simpler underlying synchronous designs.

HybridSynchAADL models are given a formal semantics and analyzed using Maude with SMT solving, which allows users to represent advanced control programs and communication features in Maude, while capturing timing uncertainties and continuous behaviors symbolically with SMT solving.

Tool Interface