Abstract
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.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic decomposition: A synopsis. SIGSAM Bull. 10(1), 10–12 (1976)
de Moura, L., Bjørner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)
Deng, Y., Rajhans, A., Julius, A.A.: STRONG: A trajectory-based verification toolbox for hybrid systems. In: Joshi, K., Siegle, M., Stoelinga, M., D’Argenio, P.R. (eds.) QEST 2013. LNCS, vol. 8054, pp. 165–168. Springer, Heidelberg (2013)
Donzé, A.: Breach, A toolbox for verification and parameter synthesis of hybrid systems. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 167–170. Springer, Heidelberg (2010)
Donzé, A., Maler, O.: Systematic simulation using sensitivity analysis. In: Bemporad, A., Bicchi, A., Buttazzo, G. (eds.) HSCC 2007. LNCS, vol. 4416, pp. 174–189. Springer, Heidelberg (2007)
Duggirala, P.S., Mitra, S., Viswanathan, M.: Verification of annotated models from executions. In: Proceedings of the 13th International Conference on Embedded Software (EMSOFT 2013), Montreal, Canada (2013)
Johnson, S.C., Lohr, G.W., McKissick, B.T., Guerreiro, N.M., Volk, P.: Simplified aircraft-based paired approach: Concept definition and initial analysis. Technical Report NASA/TP-2013-217994, NASA, Langley Research Center (2013)
Liberzon, D.: Switching in Systems and Control. In: Systems and Control: Foundations and Applications. Birkhauser, Boston (2003)
Lohmiller, W., Slotine, J.J.E.: On contraction analysis for non-linear systems. Automatica 32(6), 683–696 (1998)
Manna, Z., Pnueli, A.: A hierarchy of temporal properties. In: Proceedings of the Sixth Annual ACM Symposium on Principles of Distributed Computing (PODC 1987), Vancouver, British Columbia, Canada, p. 205. ACM (1987)
Nghiem, T., Sankaranarayanan, S., Fainekos, G., Ivancić, F., Gupta, A., Pappas, G.J.: Monte-carlo techniques for falsification of temporal properties of non-linear hybrid systems. In: Proceedings of the 13th ACM International Conference on Hybrid Systems: Computation and Control (HSCC 2010), Stockholm, Sweden, pp. 211–220. ACM (2010)
Perry, R.B., Madden, M.M., Torres-Pomales, W., Butler, R.W.: The simplified aircraft-based paired approach with the ALAS alerting algorithm. Technical Report NASA/TM-2013-217804, NASA, Langley Research Center (2013)
Wood, G., Zhang, B.: Estimation of the Lipschitz constant of a function. Journal of Global Optimization 8, 91–103 (1996)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Duggirala, P.S., Wang, L., Mitra, S., Viswanathan, M., Muñoz, C. (2014). Temporal Precedence Checking for Switched Models and Its Application to a Parallel Landing Protocol. In: Jones, C., Pihlajasaari, P., Sun, J. (eds) FM 2014: Formal Methods. FM 2014. Lecture Notes in Computer Science, vol 8442. Springer, Cham. https://doi.org/10.1007/978-3-319-06410-9_16
Download citation
DOI: https://doi.org/10.1007/978-3-319-06410-9_16
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-06409-3
Online ISBN: 978-3-319-06410-9
eBook Packages: Computer ScienceComputer Science (R0)