Search: onr:"swepub:oai:DiVA.org:mdh-56418" >
Magnifier :
Magnifier : A Compositional Analysis Approach for Autonomous Traffic Control
-
- Bagheri, Maryam (author)
- Sharif University of Technology, Tehran, Iran
-
- Sirjani, Marjan (author)
- Mälardalens högskola,Inbyggda system,Reykjavik Univ, Sch Comp Sci, Reykjavik, Iceland
-
- Khamespanah, Ehsan (author)
- Reykjavik Univ, Iceland; University of Tehran, Iran
-
show more...
-
- Baier, Christel (author)
- Technische Universitt Dresden, Germany
-
- Movaghar, Ali (author)
- Sharif University of Technology, Tehran, Iran
-
show less...
-
(creator_code:org_t)
- 2022
- 2022
- English.
-
In: IEEE Transactions on Software Engineering. - 0098-5589 .- 1939-3520. ; 48:8, s. 2732-2747
- Related links:
-
https://doi.org/10.1...
-
show more...
-
https://urn.kb.se/re...
-
https://doi.org/10.1...
-
show less...
Abstract
Subject headings
Close
- 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.
Subject headings
- NATURVETENSKAP -- Data- och informationsvetenskap -- Datavetenskap (hsv//swe)
- NATURAL SCIENCES -- Computer and Information Sciences -- Computer Sciences (hsv//eng)
Keyword
- Adaptation models
- Control systems
- Runtime
- Tracking
- Semantics
- Iterative methods
- Computer science
- Self-adaptive Systems
- Model@Runtime
- Compositional Verification
- Track-based Traffic Control Systems
- Ptolemy II
Publication and Content Type
- ref (subject category)
- art (subject category)
Find in a library
To the university's database