MR-HybridSynchAADL: formal modeling and analysis of multirate CPSs with advanced control programs and continuous dynamics
摘要
Many cyber-physical systems (CPSs) consist of a collection of components with both continuous environments and advanced control programs. Many such CPSs are either synchronous, in which the components operate in lockstep, or virtually synchronous, where the “underlying design” is synchronous but the system itself is asynchronous since it is a distributed system. A CPS may involve different kinds or brands of components, which may therefore operate with different frequencies. In addition, each component may be composed of multiple subsystems with different frequencies. This paper presents the MR-HybridSynchAADL modeling language and verification tool for modeling and analyzing the synchronous designs of synchronous and virtually synchronous hierarchical multirate CPSs with advanced control programs, continuous behaviors, and imprecise local clocks. For virtually synchronous CPSs, the Hybrid PALS synchronizer implies that verifying the much simpler underlying synchronous design also verifies the corresponding distributed system. We 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 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. We illustrate the use of MR-HybridSynchAADL on a collection of UAVs with different frequencies that deliver packets and adapt to their dynamically changing environments to avoid collisions.