Magnifier: A Compositional Analysis Approach for Autonomous Traffic Control

Research output: Contribution to journalResearch articleContributedpeer-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 languageEnglish
Pages (from-to)2732-2747
Number of pages16
JournalIEEE Transactions on Software Engineering
Volume48
Issue number8
Early online date29 Mar 2021
Publication statusPublished - Aug 2022
Peer-reviewedYes

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

Library keywords