Uma abordagem para especificação e verificação de sistemas dependentes do tempo
Resumo
Neste artigo apresenta-se uma abordagem para especificação e verificação de sistemas dependentes do tempo; ou seja, sistemas nos quais o tempo intervém direta e explicitamente (ex. sistemas tempo-real, protocolos de comunicação e aplicações multimídia). Inicialmente, apresenta-se e justifica-se o uso de uma álgebra de processos temporizada, RT-LOTOS (uma extensão temporal de LOTOS) para especificação de sistemas dependentes do tempo. Em seguida, abordam-se os métodos para análise/verificação para esse tipo de sistemas e apresenta-se a proposta de uso dos Grafos Temporizados como modelo subjacente para facilitar a verificação utilizando uma técnica de verificação de modelos a partir da lógica temporal tempo-real TCTL. Por fim, descreve-se um ambiente para auxílio à verificação que encontra-se atualmente em fase de desenvolvimento.
Referências
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.
