Rigorous Model Engineering of Hierarchical Multirate CPSs in MR-HybridSynchAADL
摘要
Many collective adaptive systems, such as collections of autonomous vehicles, are cyber-physical systems (CPSs) consisting of a collection of components, with continuous environments and advanced control programs, that collaborate to achieve common goals. The collections may involve different kinds/brands of components, which may therefore operate with different frequencies. In addition, each component may be composed of multiple subsystems with different frequencies. In this paper, we extend the Multirate Synchronous AADL (without continuous behavior) and (single-rate) HybridSynchAADL languages, and define the MR-HybridSynchAADL modeling language and verification tool for hierarchical multirate CPSs with advanced control programs, continuous behaviors, and imprecise local clocks. 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. Our 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. 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.