Magnifier: A Compositional Analysis Approach for Autonomous Traffic Control
Research output: Contribution to journal › Research article › Contributed › peer-review
Contributors
Abstract
Autonomous traffic control systems are large-scale systems with critical goals. To satisfy expected properties, these systems adapt themselves to possible changes in their environment and in the system itself. The adaptation may result in further changes propagated throughout the system. For each change and its consequent adaptation, assuring the satisfaction of properties of the system at runtime is important. A prominent approach to assure the correct behavior of these systems is verification at runtime, which has strict time and memory limitations. To tackle these limitations, we propose Magnifier, an iterative, incremental, and compositional verification approach that operates on an actor-based model where actors are grouped in components, and components are augmented with a coordinator. The Magnifier idea is zooming on the area (component) affected by a change and verifying the correctness of properties of interest of the system after adapting the component to the change. Magnifier checks if the change is propagating, and if that is the case, then it zooms out to perform adaptation on a larger area to contain the change. The process is iterative and incremental, and considers areas affected by the change one by one. In Magnifier, we use the Coordinated Adaptive Actor model (CoodAA) for traffic control systems. We present a formal semantics for CoodAA as a network of Timed Input-Output Automata (TIOAs), and prove the correctness of our compositional reasoning. We implement our approach in Ptolemy II. The results of our experiments indicate that the proposed approach improves the verification time and the memory consumption compared to the non-compositional approach.
Details
Original language | English |
---|---|
Pages (from-to) | 2732-2747 |
Number of pages | 16 |
Journal | IEEE Transactions on Software Engineering |
Volume | 48 |
Issue number | 8 |
Early online date | 29 Mar 2021 |
Publication status | Published - Aug 2022 |
Peer-reviewed | Yes |
External IDs
Scopus | 85103773430 |
---|---|
ORCID | /0000-0002-5321-9343/work/142236784 |
Keywords
ASJC Scopus subject areas
Keywords
- Ptolemy II, compositional verification, model@runtime, self-adaptive systems, track-based traffic control systems, compositional verification, model@runtime, Ptolemy II, Self-adaptive systems, track-based traffic control systems