Lightweight Formal Method for Robust Routing in Track-based Traffic Control SystemsShow others and affiliations
2020 (English)In: 2020 18TH ACM-IEEE INTERNATIONAL CONFERENCE ON FORMAL METHODS AND MODELS FOR SYSTEM DESIGN (MEMOCODE), IEEE , 2020, p. 115-124Conference paper, Published paper (Refereed)
Abstract [en]
In this paper, we propose a robust solution for the path planning and scheduling of the moving objects in a Track-based Traffic Control System (TTCS). The moving objects in a TTCS pass over pre-specified sub-tracks. Each sub-track accommodates at most one moving object in-transit. Due to the uncertainties in the context of a TTCS, we assign an arrival time window to each moving object for each sub-track in its route, instead of an exact value. The moving object can safely enter into the sub-track in the mentioned time window. To develop a safe plan, we adapt the tagged-signal model and provide a rigorous mathematical formalism for the actor model of a TTCS. To illustrate the applicability of the provided semantics, we provide a formal model of TTCSs in the Alloy language and use its analyzer to verify the developed model against system safety properties.
Place, publisher, year, edition, pages
IEEE , 2020. p. 115-124
Keywords [en]
Track-based Traffic Control Systems, Robustness, Time Window, Tagged-signal Model, Alloy Language, Actor
National Category
Computer and Information Sciences
Identifiers
URN: urn:nbn:se:mdh:diva-55475DOI: 10.1109/MEMOCODE51338.2020.9315135ISI: 000661920400011Scopus ID: 2-s2.0-85100647290OAI: oai:DiVA.org:mdh-55475DiVA, id: diva2:1580618
Conference
18th ACM-IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE)
2021-07-152021-07-152022-01-04Bibliographically approved