TY - GEN
T1 - Temporal precedence checking for switched models and its application to a parallel landing protocol
AU - Duggirala, Parasara Sridhar
AU - Wang, Le
AU - Mitra, Sayan
AU - Viswanathan, Mahesh
AU - Muñoz, César
PY - 2014
Y1 - 2014
N2 - This paper presents an algorithm for checking temporal precedence properties of nonlinear switched systems. This class of properties subsume bounded safety and capture requirements about visiting a sequence of predicates within given time intervals. The algorithm handles nonlinear predicates that arise from dynamics-based predictions used in alerting protocols for state-of-the-art transportation systems. It is sound and complete for nonlinear switch systems that robustly satisfy the given property. The algorithm is implemented in the Compare Execute Check Engine (C2E2) using validated simulations. As a case study, a simplified model of an alerting system for closely spaced parallel runways is considered. The proposed approach is applied to this model to check safety properties of the alerting logic for different operating conditions such as initial velocities, bank angles, aircraft longitudinal separation, and runway separation.
AB - This paper presents an algorithm for checking temporal precedence properties of nonlinear switched systems. This class of properties subsume bounded safety and capture requirements about visiting a sequence of predicates within given time intervals. The algorithm handles nonlinear predicates that arise from dynamics-based predictions used in alerting protocols for state-of-the-art transportation systems. It is sound and complete for nonlinear switch systems that robustly satisfy the given property. The algorithm is implemented in the Compare Execute Check Engine (C2E2) using validated simulations. As a case study, a simplified model of an alerting system for closely spaced parallel runways is considered. The proposed approach is applied to this model to check safety properties of the alerting logic for different operating conditions such as initial velocities, bank angles, aircraft longitudinal separation, and runway separation.
UR - http://www.scopus.com/inward/record.url?scp=84958522953&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84958522953&partnerID=8YFLogxK
U2 - 10.1007/978-3-319-06410-9_16
DO - 10.1007/978-3-319-06410-9_16
M3 - Conference contribution
AN - SCOPUS:84958522953
SN - 9783319064093
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 215
EP - 229
BT - FM 2014
PB - Springer-Verlag Berlin Heidelberg
T2 - 19th International Symposium on Formal Methods, FM 2014
Y2 - 12 May 2014 through 16 May 2014
ER -