Magnifier: A Compositional Analysis Approach for Autonomous Traffic Control

Publikation: Beitrag in FachzeitschriftForschungsartikelBeigetragenBegutachtung

Beitragende

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

OriginalspracheEnglisch
Seiten (von - bis)2732-2747
Seitenumfang16
FachzeitschriftIEEE Transactions on Software Engineering
Jahrgang48
Ausgabenummer8
Frühes Online-Datum29 März 2021
PublikationsstatusVeröffentlicht - Aug. 2022
Peer-Review-StatusJa

Externe IDs

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

Schlagworte

ASJC Scopus Sachgebiete

Schlagwörter

  • 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

Bibliotheksschlagworte