PL EN


Preferencje help
Widoczny [Schowaj] Abstrakt
Liczba wyników
Tytuł artykułu

Verification of Concurrent Systems with Parametric Delays Using Octahedra

Wybrane pełne teksty z tego czasopisma
Identyfikatory
Warianty tytułu
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.
Wydawca
Rocznik
Strony
1--33
Opis fizyczny
bibliogr. 31 poz., tab., wykr.
Twórcy
autor
  • Universitat Oberta de Catalunya, Rambla de Poblenou 156, 08018 Barcelona, Spain, rclariso@uoc.edu
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.
Typ dokumentu
Bibliografia
Identyfikator YADDA
bwmeta1.element.baztech-article-BUS5-0010-0020
JavaScript jest wyłączony w Twojej przeglądarce internetowej. Włącz go, a następnie odśwież stronę, aby móc w pełni z niej korzystać.