HybridSynchAADL (Hybrid Synchronous AADL) is a verification tool which presents HybridSynchAADL modeling language and formal analysis for virtually synchronous cyber-physical systems with complex control programs, continuous behaviors, and bounded clock skews, network delays, and execution times.
HybridSynchAADL models are given a formal semantics and analyzed using Maude with SMT solving, which allows us to represent advanced control programs and communication features in Maude, while capturing timing uncertainties and continuous behaviors symbolically with SMT solving.