Verification of Concurrent Systems with Parametric Delays Using Octahedra

• Autorzy: Clarisó R. , Cortadella J.
• Języki publikacji: EN

Abstrakty

EN

A technique for the verification of concurrent parametric timed systems is presented. In the systems under study, each action has a bounded delay where the bounds are either constants or parameters. Given a safety property, the analysis computes automatically a set of constraints on the parameters that is sufficient to guarantee the property. The main contribution is an innovative representation of the parametric timed state space based on bit-vectors. Experimental results from the domain of timed circuits show that this representation improves the efficiency of the verification significantly with a small impact on the accuracy of the derived constraints.

Słowa kluczowe

EN

formal verification; abstract interpretation; parametric timed systems

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2007
• Tom: Vol. 78, nr 1
• Strony: 1--33
• Opis fizyczny: bibliogr. 31 poz., tab., wykr.

Twórcy

autor

Clarisó R.

autor

Cortadella J.

• Universitat Oberta de Catalunya, Rambla de Poblenou 156, 08018 Barcelona, Spain,

Bibliografia

• [1] Alur, R., Courcoubetis, C., Halbwachs, N., Henzinger, T., Ho, P.-H., Nicollin, X., Olivero, A., Sifakis, J., Yovine, S.: The algorithmic analysis of hybrid systems, Theoretical Computer Science, 1995, 3-34.
• [2] Alur, R., Dill, D. L.: A theory of timed automata, Theoretical Computer Science, 126(2), 1994, 183-235.
• [3] Alur, R., Henzinger, T. A., Vardi, M. Y.: Parametric Real-time Reasoning, ACM Symposium on Theory of Computing, 1993.
• [4] Amon, T., Borriello, G., Hu, T., Liu, J.: Symbolic Timing Verification of Timing Diagrams using Presburger Formulas, Proc. Design Automation Conf., 1997.
• [5] Annichini, A., Asarin, E., Bouajjani, A.: Symbolic Techniques for Parametric Reasoning about Counter and Clock Systems, Computer Aided Verification, 2000.
• [6] Arnold, A.: Finite Transition Systems, Prentice-Hall, Englewood Cliffs, NJ, 1994.
• [7] Belluomini, W. J., Myers, C. J.: Timed circuit verification using TEL structures, IEEE Transactions on Computers, 20(1), 2001, 129-146.
• [8] Blunno, I., Cortadella, J., Kondratyev, A., Lavagno, L., Lwin, K., Sotiriu, C.: Handshake protocols for desynchronization, Proc. Int. Symp. on Advanced Research in Asynchronous Circuits and Systems, 2004.
• [9] Chakraborty, S., Dill, D. L., Yun, K. Y.: Min-Max Timing Analysis and an Application to Asynchronous Circuits, Proceedings of the IEEE, 87(2), 1999, 332-346.
• [10] Chernikova,N.: Algoritmfor Discovering the Set of all Solutions of a Linear Programming Problem, U.S.S.R. Computational Mathematics and Mathematical Physics, 6(8), 1964, 282-293.
• [11] Chu, T.-A.: Synthesis of self-timed VLSI circuits from graph-theoretic specifications, Ph.D. Thesis, MIT, June 1987.
• [12] Clarisó, R., Cortadella, J.: The Octahedron Abstract Domain, Proc. Static Analysis Symp., 2004.
• [13] Clarisó, R., Cortadella, J.: Verification of timed circuits with symbolic delays, Proc. of Asia and South Pacific Design Automation Conf., 2004.
• [14] Clarisó, R., Cortadella, J.: The octahedron abstract domain, Science of Computer Programming, To appear.
• [15] Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, Proc. Symp. on Principles of Programming Languages, 1977.
• [16] Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program, Proc. Symp. on Principles of Programming Languages, 1978.
• [17] Dantzig, G., Eaves, B.: Fourier-Motzkin elimination and its dual, Journal of combinatorial theory, 14, 1973, 288-297.
• [18] Dill, D. L.: Timing assumptions and verification of finite-state concurrent systems, Automatic Verification Methods for Finite State Systems, LNCS 407, Springer-Verlag, 1989.
• [19] Halbwachs, N., Proy, Y.-E., Roumanoff, P.: Verification of Real-Time Systems using Linear Relation Analysis, Formal Methods in System Design, 11(2), 1997, 157-185.
• [20] Henzinger, T. A.,Manna, Z., Pnueli, A.: Timed Transition Systems, Proc. REXWorkshop Real-Time: Theory in Practice, 600, 1992.
• [21] McMullen, P.: The maximum number of faces of a convex polytope, Mathematica, (17), 1970, 179-184.
• [22] Merlin, P., Farber, D.: Recoverability of communication protocols, IEEE Transactions on Communications, 24(9), 1976, 1036-1043.
• [23] Miné, A.: The Octagon Abstract Domain, Analysis, Slicing and Tranformation (in Working Conference on Reverse Engineering), IEEE, IEEE CS Press, 2001.
• [24] Myers, C. J., Belluomini, W., Killpack, K., Mercer, E., Peskin, E., Zheng, H.: Timed Circuits: A New Paradigm for High-Speed Design, Proc. of Asia and South Pacific Design Automation Conference, 2001.
• [25] Peña, M. A., Cortadella, J., Kondratyev, A., Pastor, E.: Formal verification of safety properties in timed circuits, Proc. Int. Symp. on Advanced Research in Asynchronous Circuits and Systems, 2000.
• [26] Sankaranarayanan, S., Sipma, H., Manna, Z.: Scalable Analysis of Linear Systems using Mathematical Programming, Proc. of International Conference on Verification, Model Checking and Abstract Interpretation, number 3385 in LNCS, Springer-Verlag, 2005.
• [27] Schuster, S., Reohr, W., Cook, P., Heidel, D., ato, M. I., Jenkins, K.: Asynchronous Interlocked Pipelined CMOS Circuits Operating at 3.3 - 4.5GHz, IEEE Int. Solid-State Circuits Conf. (ISSCC), February 2000.
• [28] Stevens, K., Ginosar, R., Rotem, S.: Relative Timing, Proc. Int. Symp. on Advanced Research in Asynchronous Circuits and Systems, 1999.
• [29] Sutherland, I., Fairbanks, S.: GasP: A minimal FIFO control, Proc. Int. Symp. on Advanced Research in Asynchronous Circuits and Systems, 2001.
• [30] Wang, F.: Symbolic Parametric Safety Analysis of Linear Hybrid Systems with BDD-like Data-Structures, Computer Aided Verification, July 2004.
• [31] Yoneda, T., Kitai, T., Myers, C.: Automatic Derivation of Timing Constraints by Failure Analysis, Proc. Int. Conference on Computer Aided Verification, 2002.