Abstract
This paper exploits design patterns employed in coordinating autonomous transport vehicles so as to ease the burden in verifying cooperating hybrid systems. The presented verification methodology is equally applicable for avionics applications (such as TCAS), train applications (such as ETCS), or automotive applications (such as platooning). We present a verification rule explicating the essence of employed design patters, guaranteeing global safety properties of the kind “a collision will never occur”, and whose premises can either be established by off-line analysis of the worst-case behavior of the involved traffic agents, or by purely local proofs, involving only a single traffic agent. In a companion paper we will show, how such local proof obligations can be discharged automatically.
This work was partly supported by the German Research Council (DFG) as part of the Transregional Collaborative Research Center “Automatic Verification and Analysis of Complex Systems” (SFB/TR 14 AVACS). See www.avacs.org for more information.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Abdul-Baki, B., Baldwin, J., Rudel, M.-P.: Independent validation and verification of the TCAS II collision avoidance subsystem. Aerospace and Electronic Systems Mag. 15(8), 3–21 (2000)
Alur, R., Courcoubetis, C., Henzinger, T.A., Ho, P.-H.: Hybrid automata: An algorithmic approach to the specification and verification of hybrid systems. In: Grossman, R.L., Ravn, A.P., Rischel, H., Nerode, A. (eds.) HS 1991 and HS 1992. LNCS, vol. 736, pp. 209–229. Springer, Heidelberg (1992)
Alur, R., Dill, D.: A theory of timed automata. Theoret. Comput. Sci. 126, 183–235 (1994)
Bohn, J., Damm, W., Klose, J., Moik, A., Wittke, H.: Modeling and validating train system applications using statemate and live sequence charts (2002)
Chutinam, A., Krogh, B.H.: Computing polyhedral approximations in flow pipes for dynamic systems. In: 37th IEEE Conference on Decision and Control, IEEE, Los Alamitos (1998)
Haxthausen, A.E., Peleska, J.: Formal development and verification of a distributed railway control system. IEEE Transactions on Software Engineering 26(8), 687–701 (2000)
Heitmeyer, C., Mandrioli, D. (eds.): Formal Methods for Real-Time Computing, number 5 in Trends in Software. Wiley, Chichester (1996)
Hoenicke, J., Olderog, E.-R.: CSP-OZ-DC: A combination of specification techniques for processes, data and time. Nordic Journal of Computing 9(4), 301–334 (2003)
Kalman, R.E., Bertram, J.E.: Control system analysis and system design via the second method of lyapunov – Part I: Continuous time systems. Transactions of the ASME, Journal of Basic Engineering 82, 371–393 (1960)
Leveson, N.G.: Safeware: System Safety and Computers. Addison-Wesley, Reading (1995)
Livadas, C., Lygeros, J., Lynch, N.A.: High-level modeling and analysis of TCAS. Proceedings of IEEE — Special Issue on Hybrid Systems: Theory & Applications 88(7), 926–947 (2000)
Lygeros, J., Godbole, D.N., Sastry, S.S.: Verified hybrid controllers for automated vehicles. IEEE Transactions on Automatic Control 43(4), 522–539 (1998)
Lynch, N.A., Segala, R., Vaandrager, F.: Hybrid I/O automata. Information and Computation 185(1), 105–157 (2003)
Olderog, E.-R., Ravn, A.P., Skakkebæk, J.U.: Refining system requirements to program specifications. In: Heitmeyer, C., Mandrioli, D. (eds.) Formal Methods for Real-Time Computing, pp. 107–134. Wiley, Chichester (1996)
Ravn, A.P.: Design of embedded real-time computing systems. Technical Report ID-TR: 1995-170, Tech. Univ. Denmark, Thesis for Doctor of Technics (1995)
Tomlin, C., Lygeros, J., Sastry, S.S.: A game theoretic approach to controller design for hybrid systems. Proc. of the IEEE 88(7), 949–970 (2000)
Tomlin, C., Pappas, G., Sastry, S.S.: Conflict resolution for air traffic management: A case study in multi-agent hybrid systems. IEEE Transactions on Automatic Control 43(4) (April 1998)
Zhou, C., Hansen, M.R.: Duration Calculus: A Formal Approach to Real-Time Systems. Springer, Heidelberg (2004)
Zhou, C., Hoare, C.A.R., Ravn, A.P.: A calculus of durations. Information Processing Letters 40(5), 269–276 (1991)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Damm, W., Hungar, H., Olderog, ER. (2004). On the Verification of Cooperating Traffic Agents. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, WP. (eds) Formal Methods for Components and Objects. FMCO 2003. Lecture Notes in Computer Science, vol 3188. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-30101-1_4
Download citation
DOI: https://doi.org/10.1007/978-3-540-30101-1_4
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-22942-1
Online ISBN: 978-3-540-30101-1
eBook Packages: Springer Book Archive