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

MR-HybridSynchAADL modeling language specifies hierarchical multirate synchronous designs for distributed controllers interacting with continuous physical environments.

MR-HybridSynchAADL semantics define both a symbolic semantics for the synchronous composition of the components, capturing continuous behaviors and timing uncertainties, and a concrete semantics, for simulation, in rewriting logic, in a modular way to ensure consistency between these two semantics.

MR-HybridSynchAADL tool provides randomized simulation and Maude-with-SMT-based reachability analysis, and is fully integrated into the OSATE tool environment for the avionics modeling standard AADL.

Tool Interface