Abstract
We present a verification methodology for cooperating traffic agents covering analysis of cooperation strategies, realization of strategies through control, and implementation of control. For each layer, we provide dedicated approaches to formal verification of safety and stability properties of the design. The range of employed verification techniques invoked to span this verification space includes application of pre-verified design patterns, automatic synthesis of Lyapunov functions, constraint generation for parameterized designs, model-checking in rich theories, and abstraction refinement. We illustrate this approach with a variant of the European Train Control System (ETCS), employing layer specific verification techniques to layer specific views of an ETCS design.
This work was partly supported by the German Research Council (DFG) as part of the Transregional Collaborative Research Center “Automatic Verification and Analy- sis of Complex Systems” (SFB/TR 14 AVACS, http://www.avacs.org/).
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
Alur, R., Grosu, R., Hur, Y., Kumar, V., Lee, I.: Modular specification of hybrid systems in CHARON. In: Lynch, N.A., Krogh, B.H. (eds.) HSCC 2000. LNCS, vol. 1790, pp. 6–19. Springer, Heidelberg (2000)
Alur, R., Grosu, R., Lee, I., Sokolsky, O.: Compositional modeling and refinement for hierarchical hybrid systems. Journal of Logic and Algebraic Programming 68(1-2), 105–128 (2006)
Balluchi, A., Benvenuti, L., Engell, S., Geyer, T., Johansson, K., Lamnabhi-Lagarrigue, F., Lygeros, J., Morari, M., Papafotiou, G., Sangiovanni-Vincentelli, A., Santucci, F., Stursberg, O.: Hybrid control of networked embedded systems. European Journal on Control, Fundam. Issues in Control 11(4-5), 478–508 (2006)
Beckert, B., Giese, M., Hähnle, R., Klebanov, V., Rümmer, P., Schlager, S., Schmitt, P.H.: The KeY System 1.0 (deduction component). In: Pfenning, F. (ed.) CADE 2007. LNCS, vol. 4603, Springer, Heidelberg (2007)
Beckert, B., Hähnle, R., Schmitt, P.H. (eds.): Verification of Object-Oriented Software. LNCS (LNAI), vol. 4334. Springer, Heidelberg (2007)
Bohn, J., Damm, W., Klose, J., Moik, A., Wittke, H.: Modeling and validating train system applications using Statemate and live sequence charts. In: Proc. Conference on Integrated Design and Process Technology. Society for Design and Process Science (2002)
Borchers, B.: CSDP, a C library for semidefinite programming. Optimization Methods and Software 10(1), 613–623 (1999)
Boyd, S., Ghaoui, L.E., Feron, E., Balakrishnan, V.: Linear Matrix Inequalities in System and Control Theory. In: SIAM (1994)
Branicky, M.S.: Multiple Lyapunov functions and other analysis tools for switched and hybrid systems. IEEE Transactions on Automatic Control 43(4) (1998)
Cervin, A., Henriksson, D., Lincoln, B., Eker, J., Arzén, K.: How does control timing affect performance? IEEE Control Systems Magazine 23(2), 16–30 (2003)
Damm, W., Disch, S., Hungar, H., Jacobs, S., Pang, J., Pigorsch, F., Scholl, C., Waldmann, U., Wirtz, B.: Exact state set representations in the verification of linear hybrid systems with large discrete state space. Technical report, AVACS (2007)
Damm, W., Disch, S., Hungar, H., Pang, J., Pigorsch, F., Scholl, C., Waldmann, U., Wirtz, B.: Automatic verification of hybrid systems with large discrete state space. In: Graf, S., Zhang, W. (eds.) ATVA 2006. LNCS, vol. 4218, pp. 276–291. Springer, Heidelberg (2006)
Damm, W., Hungar, H., Olderog, E.-R.: Verification of cooperating traffic agents. International Journal of Control 79(5), 395–421 (2006)
Damm, W., Pinto, G., Ratschan, S.: Guaranteed termination in the verification of LTL properties of non-linear robust discrete time hybrid systems. International Journal of Foundations of Computer Science 18(1), 63–86 (2007)
Donde, V., Hiskens, I.A.: Shooting methods for locating grazing phenomena in hybrid systems. Intern. Journal of Bifurcation and Chaos 16(3), 671–692 (2006)
Feng, G.: Stability analysis of piecewise discrete-time linear systems. IEEE Transactions on Automatic Control 47(7), 1108–1112 (2002)
Franklin, G.F., Powell, J.D., Workman, M.: Digital Control of Dynamic Systems. Pearson, London (1998)
Fränzle, M., Herde, C.: HySAT: An efficient proof engine for bounded model checking of hybrid systems. Formal Methods in System Design 30(3), 179–198 (2007)
Frehse, G.: Compositional verification of hybrid systems with discrete interaction using simulation relations. In: Proc. 13th IEEE Conference on Computer Aided Control Systems Design, IEEE Computer Society Press, Los Alamitos (2004)
Frehse, G.: Compositional Verification of Hybrid Systems using Simulation Relations. PhD thesis, Radboud Universiteit Nijmegen (2005)
Frehse, G.: PHAVer: Algorithmic verification of hybrid systems past HyTech. In: Morari, M., Thiele, L. (eds.) HSCC 2005. LNCS, vol. 3414, pp. 258–273. Springer, Heidelberg (2005)
Hager, G.: European ACAS operational evaluation – Final report. Technical Report EEC Report No. 316, Eurocontrol (1997)
Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. MIT Press, Cambridge (2000)
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)
Henzinger, T.A.: The theory of hybrid automata. In: Proc. 11th IEEE Symposium on Logic in Computer Science, pp. 278–292. IEEE Computer Society Press, Los Alamitos (1996)
Henzinger, T.A., Ho, P.-H., Wong-Toi, H.: Algorithmic analysis of nonlinear hybrid systems. IEEE Transactions on Automatic Control 43(5), 540–554 (1998)
Henzinger, T.A., Horowitz, B., Majumdar, R., Wong-Toi, H.: Beyond HyTech: Hybrid systems analysis using interval numerical methods. In: Lynch, N.A., Krogh, B.H. (eds.) HSCC 2000. LNCS, vol. 1790, pp. 130–144. Springer, Heidelberg (2000)
Johansson, M., Rantzer, A.: Computation of piecewise quadratic Lyapunov functions for hybrid systems. IEEE Transactions on Automatic Control 43 (1998)
Khalil, H.K.: Nonlinear Systems, 2nd edn. Prentice-Hall, Englewood Cliffs (1996)
Kratz, F., Sokolsky, O., Pappas, G.J., Lee, I.: R-Charon, a modeling language for reconfigurable hybrid systems. In: Hespanha, J.P., Tiwari, A. (eds.) HSCC 2006. LNCS, vol. 3927, pp. 392–406. Springer, Heidelberg (2006)
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)
Lofberg, J.: YALMIP: a toolbox for modeling and optimization in Matlab. In: IEEE Intern. Symp. Computer Aided Control Systems Design, pp. 284–289. IEEE Computer Society Press, Los Alamitos (2004)
Loos, R., Weispfenning, V.: Applying linear quantifier elimination. The Computer Journal 36(5), 450–462 (1993)
Lyapunov, M.A.: Problème général de la stabilité du movement. Ann. Fac. Sci. Toulouse. 9, 203–474 (1907), (Translation of a paper published in Comm. Soc. Math. Kharkow, 1893, reprinted Ann. Math. Studies No. 17, Princeton Univ. Press (1949)
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.W.: Hybrid I/O automata revisited. In: Di Benedetto, M.D., Sangiovanni-Vincentelli, A.L. (eds.) HSCC 2001. LNCS, vol. 2034, pp. 403–417. Springer, Heidelberg (2001)
Lynch, N.A., Segala, R., Vaandrager, F.W.: Hybrid I/O automata. Information and Computation 185(1), 105–157 (2003)
Mishchenko, A., Chatterjee, S., Jiang, R., Brayton, R.K.: FRAIGs: A unifying representation for logic synthesis and verification. Technical report, EECS Dept., UC Berkeley (2005)
Nesterov, Y., Nemirovskii, A.: Interior Point Polynomial Algorithms in Convex Programming. In: SIAM (1994)
Oehlerking, J., Burchardt, H., Theel, O.: Fully automated stability verification for piecewise affine systems. In: Buttazzo, G., Bemporad, A., Bicchi, A. (eds.) HSCC 2007. LNCS, vol. 4416, pp. 741–745. Springer, Heidelberg (2007)
Pettersson, S.: Analysis and Design of Hybrid Systems. PhD thesis, Chalmers University of Technology, Gothenburg (1999)
Platzer, A.: Differential dynamic logic for verifying parametric hybrid systems. In: Olivetti, N. (ed.) TABLEAUX 2007. LNCS, vol. 4548, Springer, Heidelberg (2007)
Platzer, A.: Differential logic for reasoning about hybrid systems. In: Buttazzo, G., Bemporad, A., Bicchi, A. (eds.) HSCC 2007. LNCS, vol. 4416, pp. 746–749. Springer, Heidelberg (2007)
Platzer, A.: A temporal dynamic logic for verifying hybrid system invariants. In: Proc. International Symposium on Logical Foundations of Computer Science. LNCS, vol. 4514, pp. 457–471. Springer, Heidelberg (2007)
Platzer, A.: Towards a hybrid dynamic logic for hybrid dynamic systems. In: Blackburn, P., Bolander, T., Braüner, T., de Paiva, V., Villadsen, J. (eds.) Proc. LICS Intern. Workshop on Hybrid Logic. ENTCS (2007)
Platzer, A., Clarke, E.M.: The image computation problem in hybrid systems model checking. In: Proc. 10th Workshop on Hybrid Systems: Computation and Control. LNCS, vol. 4416, pp. 473–486. Springer, Heidelberg (2007)
Segelken, M.: Abstraction and counterexample-guided construction of omega-automata for model checking of step-discrete linear hybrid models. In: Proc. 19th Conference on Computer Aided Verification. LNCS, Springer, Heidelberg (2007)
Silva, B.I., Richeson, K., Krogh, B.H., Chutinan, A.: Modeling and verification of hybrid dynamical system using CheckMate. In: Proc. 4th Conference on Automation of Mixed Processes (2000)
Somenzi, F., Bloem, R.: Efficient Büchi Automata from LTL Formulae. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 248–263. Springer, Heidelberg (2000)
Stauner, T.: Systematic Development of Hybrid Systems. PhD thesis, Technische Universität München (2001)
Stauner, T.: Discrete-time refinement of hybrid automata. In: Tomlin, C.J., Greenstreet, M.R. (eds.) HSCC 2002. LNCS, vol. 2289, pp. 407–420. Springer, Heidelberg (2002)
Tomlin, C., Pappas, G.J., Sastry, S.S.: Conflict resolution for air traffic management: A case study in multi-agent hybrid systems. IEEE Transactions on Automatic Control 43(4), 509–521 (1998)
Wende, D.: Fahrdynamik des Schienenverkehrs. Teubner (2003)
Yakubovich, V.: S-procedure in nonlinear control theory. Vestnik Leningrad University, pp. 62–71 (1971)
Zhou, C., Hansen, M.: Duration Calculus: A Formal Approach to Real-Time Systems. Springer, Heidelberg (2004)
Zhou, C., Hoare, C., Ravn, A.P.: A calculus of durations. Information Processing Letters 40(5), 269–276 (1991)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Damm, W. et al. (2007). Automating Verification of Cooperation, Control, and Design in Traffic Applications. In: Jones, C.B., Liu, Z., Woodcock, J. (eds) Formal Methods and Hybrid Real-Time Systems. Lecture Notes in Computer Science, vol 4700. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-75221-9_6
Download citation
DOI: https://doi.org/10.1007/978-3-540-75221-9_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-75220-2
Online ISBN: 978-3-540-75221-9
eBook Packages: Computer ScienceComputer Science (R0)