Alexandre David
ABSTRACT
A specification theory combines notions of specifications and implementations with a satisfaction relation, a refinement relation and a set of operators supporting stepwise design. We develop a complete specifification framework for real-time systems using Timed I/O Automata as the specification formalism, with the semantics expressed in terms of Timed I/O Transition Systems. We provide constructs for refinement, consistency checking, logical and structural composition, and quotient of specifications --- all indispensable ingredients of a compositional design methodology. The theory is implemented on top of an engine for timed games, Uppaal-tiga, and illustrated with a small case study.
- R. Alur and D. L. Dill. A theory of timed automata. Theor. Comput. Sci., 126(2):183--235, 1994. Google Scholar
Digital Library
- R. Alur, T. A. Henzinger, O. Kupferman, and M. Y. Vardi. Alternating refinement relations. In CONCUR'98, volume 1466 of LNCS. Springer, 1998. Google ScholarDigital Library
- G. Behrmann, A. Cougnard, A. David, E. Fleury, K. G. Larsen, and D. Lime. Uppaal-tiga: Time for playing games! In CAV, volume 4590 of LNCS. Springer, 2007. Google ScholarDigital Library
- N. Bertrand, A. Legay, S. Pinchinat, and J.-B. Raclet. A compositional approach on modal specifications for timed systems. In ICFEM, LNCS. Springer, 2009. Google ScholarDigital Library
- N. Bertrand, S. Pinchinat, and J.-B. Raclet. Refinement and consistency of timed modal specifications. In LATA, volume 5457 of LNCS, Tarragona, Spain, 2009. Springer. Google ScholarDigital Library
- P. Bulychev, T. Chatain, A. David, and K. G. Larsen. Efficient on-the-fly algorithm for checking alternating timed simulation. In FORMATS, volume 5813 of LNCS, pages 73--87. Springer, 2009. Google ScholarDigital Library
- B. Caillaud, B. Delahaye, K. G. Larsen, A. Legay, M. Peddersen, and A. Wasowski. Compositional design methodology with constraint markov chains. Technical report, Hal-INRIA, 2009.Google Scholar
- F. Cassez, A. David, E. Fleury, K. G. Larsen, and D. Lime. Efficient on-the-fly algorithms for the analysis of timed games. In CONCUR, 2005. Google ScholarDigital Library
- K. Cerfins, J. C. Godskesen, and K. G. Larsen. Timed modal specification - theory and tools. In Proceedings of the 5th International Conference on Computer Aided Verification (CAV'93), volume 697 of LNCS, pages 253--267. Springer, 1993. Google ScholarDigital Library
- A. Chakabarti, L. de Alfaro, T. A. Henzinger, and M. I. A. Stoelinga. Resource interfaces. In R. Alur and I. Lee, editors, EMSOFT 03: 3rd Intl. Workshop on Embedded Software, LNCS. Springer, 2003.Google Scholar
- L. de Alfaro and M. Faella. An accelerated algorithm for 3-color parity games with an application to timed games. In CAV, volume 4590 of LNCS. Springer, 2007. Google ScholarDigital Library
- L. de Alfaro and T. A. Henzinger. Interface automata. In FSE, pages 109--120, Vienna, Austria, Sept. 2001. ACM Press. Google ScholarDigital Library
- L. de Alfaro and T. A. Henzinger. Interface-based design. In In Engineering Theories of Software Intensive Systems, Marktoberdorf Summer School. Kluwer Academic Publishers, 2004.Google Scholar
- L. de Alfaro, T. A. Henzinger, and R. Majumdar. Symbolic algorithms for infinite-state games. In K. G. Larsen and M. Nielsen, editors, CONCUR, volume 2154 of LNCS, pages 536--550. Springer, 2001. Google ScholarDigital Library
- L. de Alfaro, T. A. Henzinger, and M. I. A. Stoelinga. Timed interfaces. In A. L. Sangiovanni-Vincentelli and J. Sifakis, editors, EMSOFT, volume 2491 of LNCS, pages 108--122. Springer, 2002. Google ScholarDigital Library
- Z. Deng and J. W. s. Liu. Scheduling real-time applications in an open environment. In in Proceedings of the 18th IEEE Real-Time Systems Symposium, IEEE Computer, pages 308--319. Society Press, 1997. Google ScholarDigital Library
- S. J. Garland and N. A. Lynch. The IOA language and toolset: Support for designing, analyzing, and building distributed systems. Technical report, Massachusetts Institute of Technology, Cambridge, MA, 1998.Google Scholar
- T. A. Henzinger, Z. Manna, and A. Pnueli. Timed transition systems. In REX Workshop, volume 600 of LNCS, pages 226--251. Springer, 1991. Google ScholarDigital Library
- T. A. Henzinger and S. Matic. An interface algebra for real-time components. In IEEE Real Time Technology and Applications Symposium, pages 253--266. IEEE Computer Society, 2006. Google ScholarDigital Library
- T. A. Henzinger and J. Sifakis. The embedded systems design challenge. In FM, volume 4085 of LNCS, pages 1--15. Springer, 2006. Google ScholarDigital Library
- D. K. Kaynar, N. A. Lynch, R. Segala, and F. W. Vaandrager. Timed i/o automata: A mathematical framework for modeling and analyzing real-time systems. In RTSS, pages 166--177. IEEE Computer Society, 2003. Google ScholarDigital Library
- K. G. Larsen. Modal specifications. In J. Sifakis, editor, Automatic Verification Methods for Finite State Systems, volume 407 of LNCS, pages 232--246. Springer, 1989. Google ScholarDigital Library
- K. G. Larsen, U. Nyman, and A. Wasowski. Modal I/O automata for interface and product line theories. In R. D. Nicola, editor, ESOP, volume 4421 of LNCS, pages 64--79. Springer, 2007. Google ScholarDigital Library
- I. Lee, J. Y.-T. Leung, and S. H. Son. Handbook of Real-Time and Embedded Systems. Chapman, 2007. Google ScholarDigital Library
- N. Lynch. I/O automata: A model for discrete event systems. In Annual Conference on Information Sciences and Systems, pages 29--38, Princeton University, Princeton, N.J., 1988.Google Scholar
- N. A. Lynch and M. R. Tuttle. An introduction to input/output automata. Technical Report MIT/LCS/TM-373, The MIT Press, Nov. 1988.Google Scholar
- O. Maler, A. Pnueli, and J. Sifakis. On the synthesis of discrete controllers for timed systems (an extended abstract). In STACS, pages 229--242, 1995.Google ScholarCross Ref
- R. Milner. Communication and Concurrency. Prentice Hall, 1988. Google ScholarDigital Library
- R. D. Nicola and R. Segala. A process algebraic view of input/output automata. Theoretical Computer Science, 138, 1995. Google ScholarDigital Library
- E. W. Stark, R. Cleavland, and S. A. Smolka. A process-algebraic language for probabilistic I/O automata. In CONCUR, LNCS, pages 189--2003. Springer, 2003.Google ScholarCross Ref
- A. Tarski. A lattice-theoretical fixpoint theorem and its applications. Pacific Journal of Mathematics, 5:285--309, 1955.Google ScholarCross Ref
- L. Thiele, E. Wandeler, and N. Stoimenov. Real-time interfaces for composing real-time systems. In EMSOFT, pages 34--43. ACM, 2006. Google ScholarDigital Library
- F. W. Vaandrager. On the relationship between process algebra and input/output automata. In LICS, pages 387--398, 1991.Google ScholarCross Ref
Index Terms
- Timed I/O automata: a complete specification theory for real-time systems
Recommendations
Robust synthesis for real-time systems
Specification theories for real-time systems allow reasoning about interfaces and their implementation models, using a set of operators that includes satisfaction, refinement, logical and parallel composition. To make such theories applicable throughout ...
Timed Automata Patterns
Timed Automata have proven to be useful for specification and verification of real-time systems. System design using Timed Automata relies on explicit manipulation of clock variables. A number of automated analyzers for Timed Automata have been ...
Timed CSP and Object-Z
ZB'03: Proceedings of the 3rd international conference on Formal specification and development in Z and BIn this paper we discuss a simple integration of timed CSP and Object-Z. Following existing work, the components in such an integration are written as either Object-Z classes, or timed CSP processes, and are combined together using CSP parallel ...
Comments