Abstract
The paper describes a transformational approach for the specification and formal verification of concurrent and real-time systems.At upper level, one system is specified using the timed process algebra RT-LOTOS. The output of the proposed transformation is a Time Petri net (TPN). The paper particularly shows how a TPN can be automatically constructed from an RT-LOTOS specification using a compositionally defined mapping. The proof of the translation consistency is sketched in the paper and developed in[1].
The RT-LOTOS to TPN translation patterns formalized in the paper are being implemented. in a prototype tool. This enables reusing TPNs verification techniques and tools for the profit of RT-LOTOS.
Chapter PDF
References
Sadani, T., Boyer, M., de Saqui-Sannes, P., Courtiat, J.P.: Effective representation of regular RT-LOTOS terms by finite time petri nets. Technical Report 05605, LAAS/CNRS (2006)
Courtiat, J.P., Santos, C., Lohr, C., Outtaj, B.: Experience with RT-LOTOS, a temporal extension of the LOTOS formal description technique. Computer Communications 23(12) (2000)
RT-LOTOS: Real-time LOTOS home page, http://www.laas.fr/RT-LOTOS/
Yovine, S.: Kronos: A verification tool for real-time systems. Software Tools for Technology Transfer 1(123–133) (1997)
Bengtsson, J., Larsen, K.G., Larsson, F., Pettersson, P., Yi, W.: UPPAAL - a tool suite for automatic verification of real-time systems. In: Alur, R., Sontag, E.D., Henzinger, T.A. (eds.) HS 1995. LNCS, vol. 1066, pp. 232–243. Springer, Heidelberg (1996)
Sadani, T., Courtiat, J., de Saqui-Sannes, P.: From RT-LOTOS to time Petri nets. new foundations for a verification platform. In: Proc. of 3rd IEEE Int. Conf. on Software Engineering and Formal Methods (SEFM) (2005)
Best, E., Devillers, R., Koutny, M.: Petri Net Algebra. Monographs in Theoretical Computer Science: An EATCS Series. Springer, Heidelberg (2001) ISBN: 3-540-67398-9.
ISO - Information processing systems - Open Systems Interconnection: LOTOS - a formal description technique based on the temporal ordering of observational behaviour. ISO International Standard 8807:1989, ISO (1989)
Milner, R.M.: Communications and Concurrency. Prentice-Hall, Englewood Cliffs (1989)
Hoare, C.: Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs (1985)
Courtiat, J.P.: Formal design of interactive multimedia documents. In: König, H., Heiner, M., Wolisz, A. (eds.) FORTE 2003. LNCS, vol. 2767, Springer, Heidelberg (2003)
ISO/IEC: Information technology - enhancements to LOTOS (E-LOTOS). Technical Report 15437:2001, ISO/IEC (2001)
Merlin, P.: A study of the recoverability of computer system. PhD thesis, Dep. Comput. Sci., Univ. California, Irvine (1974)
Merlin, P., Faber, D.J.: Recoverability of communication protocols. IEEE Transactions on Communications COM-24(9) (1976)
Berthomieu, B., Menasche, M.: Une approche par énumération pour l’analyse des réseaux de Petri temporels. In: Actes de la conférence IFIP 1983, pp. 71–77 (1983)
Berthomieu, B., Diaz, M.: Modeling and verification of time dependant systems using Time Petri Nets. IEEE Transactions on Software Engineering 17(3) (1991)
Katz, S., Grumberg, O.: A framework for translating models and specifications. In: Butler, M., Petre, L., Sere, K. (eds.) IFM 2002. LNCS, vol. 2335, p. 145. Springer, Heidelberg (2002)
Koutny, M.: A compositional model of time petri nets. In: Nielsen, M., Simpson, D. (eds.) ICATPN 2000. LNCS, vol. 1825, pp. 303–322. Springer, Heidelberg (2000)
Taubner, D.: Finite Representations of CCS and TCSP Programs by Automata and Petri Nets. LNCS, vol. 369. Springer, Heidelberg (1989)
Yi, W.: Real-time behaviour of asynchronous agents. In: Baeten, J.C.M., Klop, J.W. (eds.) CONCUR 1990. LNCS, vol. 458, Springer, Heidelberg (1990)
Goltz, U.: On representing CCS programs by finite Petri nets. In: Koubek, V., Janiga, L., Chytil, M.P. (eds.) MFCS 1988. LNCS, vol. 324, Springer, Heidelberg (1988)
Olderog, E.R.: Nets, Terms, and formulas. Cambridge University Press, Cambridge (1991)
Garavel, H., Sifakis, J.: Compilation and verification of LOTOS specifications. In: Logrippo, L., et al. (eds.) Protocol Specification, Testing and Verification, X. Proceedings of the IFIP WG 6.1 Tenth International Symposium, Ottawa, Ont., Canada, pp. 379–394. North-Holland, Amsterdam (1990)
Barbeau, M., von Bochmann, G.: Verification of LOTOS specifications: A Petri net based approach. In: Proc. of Canadian Conf. on Electrical and Computer Engineering (1990)
Larrabeiti, D., Quelmada, J., Pavón, S.: From LOTOS to Petri nets through expansion. In: Gotzhein, R., Bredereke, J. (eds.) Proc. of Int. Conf. on Formal Description Techniques and Theory, application and tools (FORTE/PSV 1996) (1996)
Barbeau, M., von Bochmann, G.: Extension of the Karp and Miller procedure to LOTOS specifications. Discrete Mathematics and Theoretical Computer Science 3, 103–119 (1991)
Barbeau, M., von Bochmann, G.: A subset of LOTOS with the computational power of place/transition-nets. In: Ajmone Marsan, M. (ed.) ICATPN 1993. LNCS, vol. 691. Springer, Heidelberg (1993)
Garavel, H., Lang, F., Mateescu, R.: An overview of cadp 2001. European Association for software science and technology (EASST) Newsletter 4 (2002)
Sisto, R., Valenzano, A.: Mapping Petri nets with inhibitor arcs onto basic LOTOS behavior expressions. IEEE Transactions on computers 44(12), 1361–1370 (1995)
Bolognesi, T., Lucidi, F., Trigila, S.: From timed Petri nets to timed LOTOS. In: Protocol Specification, Testing and Verification X (PSTV), Proceedings of the IFIP WG6.1 Tenth International Symposium on Protocol, pp. 395–408 (1990)
Durante, L., Sisto, R., Valenzano, A.: Integration of time Petri net and TE-LOTOS in the design and evaluation of factory communication systems. In: Proc. of the 2nd IEEE Workshop on Factory Communications Systems (WFCS 1997) (1997)
Marroquín Alonso, O., de Frutos Escrig, D.: Extending the petri box calculus with time. In: Colom, J.-M., Koutny, M. (eds.) ICATPN 2001. LNCS, vol. 2075, p. 303. Springer, Heidelberg (2001)
Berthomieu, B., Ribet, P., Vernadat, F.: The TINA tool: Construction of abstract state space for Petri nets and time Petri nets. Int. Journal of Production Research 42(14) (2004)
Apvrille, L., Courtiat, J.P., Lohr, C., de Saqui-Sannes, P.: TURTLE: A real-time UML profile supported by a formal validation toolkit. IEEE Transactions on Software Engineering 30(4) (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 IFIP International Federation for Information Processing
About this paper
Cite this paper
Sadani, T., Boyer, M., de Saqui-Sannes, P., Courtiat, JP. (2006). Effective Representation of RT-LOTOS Terms by Finite Time Petri Nets. In: Najm, E., Pradat-Peyre, JF., Donzeau-Gouge, V.V. (eds) Formal Techniques for Networked and Distributed Systems - FORTE 2006. FORTE 2006. Lecture Notes in Computer Science, vol 4229. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11888116_29
Download citation
DOI: https://doi.org/10.1007/11888116_29
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-46219-4
Online ISBN: 978-3-540-46220-0
eBook Packages: Computer ScienceComputer Science (R0)