Paper Info
Title
Lightweight Formal Method for Robust Routing in Track-based Traffic Control Systems
Abstract
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.
Year
DOI
Venue
2020
10.1109/MEMOCODE51338.2020.9315135
2020 18th ACM-IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE)
Keywords
DocType
ISBN
Track-based Traffic Control Systems,Robustness,Time Window,Tagged-signal Model,Alloy Language,Actor
Conference
978-1-7281-9149-2
Citations 
PageRank 
References 
0
0.34
0
Authors
6
Name
Order
Citations
PageRank
Maryam Bagheri100.34
Edward A. Lee262.96
Eunsuk Kang36415.95
Marjan Sirjani491557.77
Ehsan Khamespanah512814.13
A. Movaghar619732.28