Abstract
Due to the complexity and time-based aspects of modern systems, compositional verification and abstraction-based verification techniques have been proposed to deal with these issues by considering the verification of system components separately (composition) and working on more abstract structures (refinement). In this paper, we propose a revised definition of the product of timed automata (TA) and give a compositional semantics based on individual timed transition system (TTS) semantics. Moreover, we establish a new compositional refinement property where the refinement of timed systems composition is given by the refinement of each component. For this purpose, starting from the basic timed transition systems, we introduce an original composition operator endowed with good properties (associativity, trace inclusion, etc) and supporting communications via shared variables and synchronization of actions. Thereafter, we instantiate this framework for timed automata where we show how to associate such a TTS with two-levels static priority (committedness) to a TA and establish the compositionality theorem introduced by [5] with the mentioned refinement property.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Arnold, A.: Finite transition systems: semantics of communicating systems. Prentice Hall International Ltd., Hertfordshire (1994), Translator-Plaice, John
Behrmann, G., David, A., Larsen, K.G.: A Tutorial on Uppaal. Department of computer science, Aalborg university (2004)
Bengtsson, J., Wang, Y.: Timed automata: Semantics, algorithms and tools. In: Desel, J., Reisig, W., Rozenberg, G. (eds.) Lectures on Concurrency and Petri Nets. LNCS, vol. 3098, pp. 87–124. Springer, Heidelberg (2004)
Bensalem, S., Bozga, M., Sifakis, J., Nguyen, T.H.: Compositional verification for component-based systems and application. In: Cha, S(S.), Choi, J.-Y., Kim, M., Lee, I., Viswanathan, M. (eds.) ATVA 2008. LNCS, vol. 5311, pp. 64–79. Springer, Heidelberg (2008)
Berendsen, J., Vaandrager, F.: Compositional Abstraction in Real-Time Model Checking. In: 6th International Conference on Formal Modelling and Analysis of Timed Systems, Saint Malo, France, pp. 233–249 (September 2008)
Berthomieu, B., Bodeveix, J., Filali, M., Garavel, H., Lang, F., Peres, F., Saad, R., Stoecker, J., Vernadat, F., Gaufillet, P., Lang, F.: The syntax and semantics of FIACRE. LAAS Laboratory, University of Toulouse (2009)
Bornot, S., Gößler, G., Sifakis, J.: On the construction of live timed systems. In: Graf, S. (ed.) TACAS 2000. LNCS, vol. 1785, pp. 109–126. Springer, Heidelberg (2000)
Bouyer, P., Markey, N., Reynier, P.A.: Robust model-checking of linear-time properties in timed automata. In: Correa, J.R., Hevia, A., Kiwi, M. (eds.) LATIN 2006. LNCS, vol. 3887, pp. 238–249. Springer, Heidelberg (2006)
Clarke, E.M., Long, D.E., McMillan, K.L.: Compositional model checking. In: LICS 1989, pp. 353–362 (1989)
Coq, Technical report, INRIA, http://coq.inria.fr
David, A., Hakansson, J., Larsen, K.G., Pettersson, P.: Model checking Timed Automata with Priorities Using DBM Subtraction, pp. 128–142. Springer, Heidelberg (2006)
Henzinger, T.A., Manna, Z., Pnueli, A.: Timed transition systems (1992)
Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs (1985)
Jensen, H.E., Larsen, K.G., Skou, A.: Scaling up UPPAAL:automatic verification of real-time systems using compositionality and abstraction. In: Joseph, M. (ed.) FTRTFT 2000. LNCS, vol. 1926, p. 19. Springer, Heidelberg (2000)
Larsen, K.G., Pettersson, P., Wang, Y.: UPPAAL in a nutshell. Journal on Software Tools for Technology Transfert (1997)
Milner, R.: Communication and Concurrency. Prentice Hall Ltd., Englewood Cliffs (1989)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bodeveix, JP., Boudjadar, A., Filali, M. (2011). An Alternative Definition for Timed Automata Composition. In: Bultan, T., Hsiung, PA. (eds) Automated Technology for Verification and Analysis. ATVA 2011. Lecture Notes in Computer Science, vol 6996. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-24372-1_9
Download citation
DOI: https://doi.org/10.1007/978-3-642-24372-1_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-24371-4
Online ISBN: 978-3-642-24372-1
eBook Packages: Computer ScienceComputer Science (R0)