Uma abordagem para especificação e verificação de sistemas dependentes do tempo
Abstract
In this paper, we present an approach to specify and to verify time dependent systems; in this kind of systems (e.g. real-time systems, communication protocols and multimedia applications), time appears in a direct and explicit way. First, we present and justify the use of a timed process algebra, called RT-LOTOS which is a temporal extension of LOTOS, to specify time dependent systems. In the following we discuss about analysis and verification methods to be used in the systems and we present a proposal based on model checking which uses the real-time temporal logic TCTL on a timed graph obtained from the RT-LOTOS specification; this translation aims to improve and to facilitate the proposed method. At last, we describe a specification and verification environment which is being presently developed in our laboratory.
References
Blair, G.; Blair, L.; Bowman, H. e Chetwynd A., Formal Support for the Specification and Construction of Distributed Multimedia Systems (The Tempo Project) - Final Project Deliverable, Internal Report MPG-93-23, Lancaster University, 1993.
Bolognesi, T. et Lucidi, F., Timed Process Algebras with Urgent Interactions and a Unique Powerful Binary Operator, Proc. of the REX Workshop"Real time: Theory in Practice", LNCS 600, Springer Verlag, 1991.
Brams, G.W., Réseauz de Petri: Théorie et Pratique, Ed. Masson, Tomos 1 e 2, Paris, 1983.
Camargo, MS. de, Tomando LOTOS Apta para Especificar Sistemas Dependentes do Tempo, Tese de Doutorado, LCMI, Curso de Pós-Graduação em Eng. Elétrica, Universidade Federal de Santa Catarina, Florianópolis, Janeiro, 1995.
Camargo, M.S. de; e Farines, J.-M. Tornando LOTOS Apta para Especificar Sistemas Tempo-Real, Anais do 12 Simpósio Brasileiro de Redes de Computadores, Curitiba, maio, 1994.
Courtiat, J.P. et de Camargo, M.S. et Saidouni, D.E. RT.LOTOS: LOTOS Temporisé pour la Specification de Systémes Temps Réel, CFIP'O5 - Ingénierie des Protocoles, Eds: R. Dssouli et G. von Bochmann, Montréal, Setembro, 1993, HERMES, Paris, 1993, pags. 427-441.
Daws, C.; Olivero, A. e Yovine, S., Verifying ET-LOTOS programs with KRONOS, In Proc. of FORTE'M, Berne, Outubro, 1004.
LOTOS, A Formal Description Technique Based on the Ordering of Observational Behaviour, ISO IS 8807, Novembro, 1988.
Leduc, G. et Léonard, L. A Timed LOTOS Supporting a Dense Time Domain and Including New Timed Operatars, Proc. of the 5th International Conference on Formal Description Techniques, FORTE '92, North-Holland, 1993.
Marsan, MA. et ali, A LOTOS Extension for the Performance Analysis of Distributed Systems, IEEE/ACM Transactions on Networking, Vol.2, No.2, Abril, 1094, pp. 151-165.
Nicollin, X. et Sifakis, J. et Yovine, S., From ATP to Timed Graphs and Hibrid Systems, Proceedings of the REX Workshop, Mook, The Netherlands, Lecture Notes in Computer Science No. 600, Springer-Verlag, 1992, pp. 540-572.
Ostroff, J. S., Formal Methods for the Specification and Design of Real-Time Safety Critical Systems, Journal Systems Software, Vol. 18, 1992, pp. 33-60.
Quemada, J., et Azcorra, A., et Frutos, D., A Timed Caleulus for LOTOS, Proc. of the 2nd International Conference on Formal Description Techniques, FORTE '89, North-Holland, 1990.
Yi, Wang, A Calculus of Real Time Systems, Ph.D. Thesis, Department of Computer Sciences, Chalmers University of Technology, Goteborg, Sweden, 1991.
Yovine, S., Méthodes ct Outils pour la Vérification de Systémes Temporisés, Thèse de Docteur de Institut National Polytecnique de Grenoble, França, Maio, 1993.
