Magnifier: A Compositional Analysis Approach for Autonomous Traffic Control

Research output: Contribution to book/conference proceedings/anthology/reportConference contributionContributed

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 languageEnglish
Title of host publicationIEEE Transactions on Software Engineering
Pages2732-2747
Number of pages15
Volume48
Publication statusPublished - 29 Mar 2021
Peer-reviewedNo

Publication series

SeriesIEEE Transactions on Software Engineering
ISSN0098-5589

External IDs

Scopus 85103773430
ORCID /0000-0002-5321-9343/work/142236784

Keywords

Keywords

  • self-adaptive systems, model@runtime, compositional verification, track-based traffic control systems, Ptolemy II