A Timed Extension for ALTARICA

• Autorzy: Cassez F. , Pagetti C. , Roux O.
• Języki publikacji: EN

Abstrakty

EN

In this paper we present a timed extension of the AltaRica formalism. Following previous works, we first extend the semantics of AltaRicawith time and define timed components and timed nodes. Moreover we lift the priority features of AltaRicato the timed case. We obtain a timed version of AltaRica, called Timed AltaRica. Finally we give a translation of a Timed AltaRicaspecification into a usual timed automaton. These are the semantic foundations of a high-level hierarchical language for the specification of timed systems.

Słowa kluczowe

EN

AltaRica; semantics; Timed Automata

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2004
• Tom: Vol. 62, nr 3,4
• Strony: 291--332
• Opis fizyczny: Bibliogr. 32 poz., wykr.

Twórcy

autor

Cassez F.

• IRCCyN, UMR CNRS 6597, 1 rue de la Noë, BP 92101, 44321 Nantes Cedex 3, France

autor

Pagetti C.

• IRCCyN, UMR CNRS 6597, 1 rue de la Noë, BP 92101, 44321 Nantes Cedex 3, France

autor

Roux O.

• IRCCyN, UMR CNRS 6597, 1 rue de la Noë, BP 92101, 44321 Nantes Cedex 3, France

Bibliografia

• [1] G. Berry and G. Gonthier. The ESTEREL synchronous programming language: Design, semantics, implementation. Science of Computer Programming, 19(2):87-152,1992.
• [2] N. Halbwachs, P. Caspi, P. Raymond, and D. Pilaud. The synchronous data-flow programming language LUSTRE. Proceedings of the IEEE, 79(9): 1305-1320, September 1991.
• [3] P. Le Guemic, M. Le Borgne, T. Gautier, and C. Le Maire. Programming real-time applications with SIGNAL. Proceedings of the IEEE, 79(9):1321-I336, September 1991.
• [4] F. Cassez and O. Roux. Compilation of the ELECTRE reactive language into finite transition systems. Theoretical Computer Science, 146(l-2):109-143,juillet 1995.
• [5] P. Pettersson and K, G. Larsen. UPPAAL2k. Bulletin of the European Association for Theoretical Computer Science. 70:40-^4, February 2000.
• [6] F Laroussinie and K. G. Larsen. CMC: A tool for compositional model-checking of real-time systems. In Proc. IFIP Joint Int. Conf Formal Description Techniques & Protocol Specification, Testing, and Verification (FORTE-PSTV'98), pages 439-456. Kluwer Academic Publishers. 1998.
• [7] M. Bozga, C. Daws, O. Maier, A. Olivero, S. Tripakis, and S. Yovine. KRONOS: A model-checking tool for real-time systems. In A. J. Hu and M. Y. Vardi. editors, Proc. 10th International Conference on Computer Aided Verification, Vancouver, Canada, Lecture Notes in Computer Science, volume 1427, pages 546-550. Springer-Verlag, 1998.
• [8] T. A. Henzinger, P. H. Ho, and H. Wong-Toi. HYTECH: A model checker for hybrid systems. International Journal on Software Tools for Technology Transfer, 1(1-2): 110-122, 1997.
• [9] G. Point and A. Rauzy. ALTARICA - Constraint automata as a description language. European Journal on Automation, 1999. Special issue on the Modelling of Reactive Systems.
• [10] G. Point. ALTARICA.' Contribution ê l'unification des mthodes formelles et de la suret de fonctionnement. PhD thesis, University of Bordeaux I, January 2000.
• [11] A. Arnold, A. Griffault, G. Point, and A. Rauzy. The ALTARICA formalism for describing concurrent systems. Fundamenta Infomiaticae, 40: 109-124, 2000.
• [12] A. Griffault. S. Lajeunesse, G. Point, A. Rauzy, J.-P. Signoret, and P. Thomas. The ALTARICA language. In Proceedings of the International Conference on Safety and Reliability, ESREL'98. Balkema Publishers, June 20-24, 1998.
• [13] A. Arnold, D. Begay, and P. Crubille. Construction and analysis of transition systems with MEC. World Scientific, 1994.
• [14] A. Arnold. An experience with MEC in a real industrial project. Formal specifications: Foundations, Methods, Tools and Applications, Konstancin-Jeziorna (Pologne), 1995.
• [15] A. Vincent. Conception et ralisation d'un vrificateur de modles ALTARICA. PhD thesis, University of Bordeaux I. 2003.
• [16] A. Griffaull and A. Vincent. The MEC 5 model checker. In R. Alur and D. A. Peled, editors, Proc. 16th Intemational Conference on Computer Aided Verification, Boston. MA. tJSA, Lecture Notes in Computer Science, volume 3114, pages 488-491. Springer-Verlag, 2004.
• [17] R. Alur and D. Dill. A theory of timed automata. Theoretical Computer Science B. 126:183-235, 1994.
• [18] T. A. Henzinger. The theory of hybrid automata. In Proceedings 11th 'Annual IEEE Symposium on Logic in Computer Science, pages 278-292, New Brunswick, New Jersey, 27-30 July 1996. IEEE Computer Society Press.
• [19] R. Alur, C. Courcoubetis, N. Halbwachs. T. A. Henzinger. P.-H. Ho. X. Nicollin. A. Olivero. J. Sifakis, and S. Yovine. The algorithmic analysis of hybrid systems. Theoretical Computer Science, 138(l):3-34, 1995.
• [20] Gerd Behrmann, Alexandre David, Kim G. Larsen, Oliver Möller, Paul Pettersson, and Wang Yi. UPPAAL-Present and Future. In Proceedings of the 40th IEEE Conference on Decision and Control (CDC'2001). Orlando, Florida, USA. December 4-7, 2001.
• [21] B. Bérard, M. Bidoit, A. Finkei, F. Laroussinie. A. Petit. L. Petrucci, and P. Schnoebelen. Systems and Software Verification. Model-Checking Techniques and Tools. Springer-Verlag. 2001.
• [22] J. Sifakis and S. Yovine. Compositional specification of timed systems. In 13th Annual Symp. on Theoretical Aspects of Computer Science. STACS'96.. Lecture Notes in Computer Science, volume 1046, pages 347-359, 1996. Invited paper.
• [23] K. G. Larsen, P. Pettersson. and W. Yi. Compositional and Symbolic Model-Checking of Real-Time Systems. In Proc. of the /6th IEEE Real-Time Systems Symposium (RTSS)., pages 76-87. IEEE Computer Society Press, December 1995.
• [24] P. Bouyer, C. Dufourd, E. Fleury, and A. Petit. Are timed automata updatable ? In Proc. 12th International Conference on Computer Aided Verification {CAV'2000l Chicago, IL, USA. volume 1855, pages 464-479. Springer, July 2000.
• [25] A. Arnold. Finite transition systems. Prentice-Hall, Masson. 1994.
• [26] S, Bornot and J. Sifakis. On the composition of hybrid systems. In Hybrid systems: Computation and Control HSCC, Berkeley, CA, USA, invited talk. Lecture Notes in Computer Science, volume 1386, pages 69-83, Springer, April 1998.
• [27] S. Bornot, G. Goessler, and J. Sifakis. On the construction of live timed systems. In Tools and Algorithms for Construction and Analysis of Systems (TACAS), Lecture Notes in Computer Science, volume 1785, pages 109-126,2000.
• [28] S. Bornot, J. Sifakis, and S. Tripakis. Modeling urgency in timed systems. COMPOS'97, Malente, Germany, Lecture Notes in Computer Science, volume 1536, pages 103-129, 1998.
• [29] S. Bornot and J. Sifakis. An algebraic frame work for urgency. Information and Computation, 163(1):172-202. 2000.
• [30] J. Sifakis and S. Yovine. Compositional specification of timed systems (extended abstract). In Symposium on Theoretical Aspects of Computer Science (STACS), Lecture Notes in Computer Science, volume 1046, pages 347-359, 1996. Invited paper.
• [31] C. Daws, A. Olivero, S. Tripakis, and S. Yovine. The tool KRONOS. In Hybrid Systems III: Verification and Control, Lecture Notes in Computer Science, volume 1066, pages 208-219, Rutgers University, New Brunswick, NJ, USA, 22-25 October 1995. Springer.
• [32] C. Pagetti. Extension temporisée du langage ALTARICA. PhD thesis, Ecole Centrale de Nantes et University de Nantes. April 2004.