Validação de Especificações Formais de Sistemas Dependentes de Tempo Através de Simulação
Resumo
Este artigo apresenta uma abordagem baseada em simulação para a validação de sistemas dependentes de tempo, especificados numa extensão temporal da linguagem LOTOS denominada RT-LOTOS (Real-Time LOTOS). A primeira parte do artigo apresenta as principais características de RT-LOTOS, com uma discussão de sua sintaxe e semântica. A seguir, é apresentada uma metodologia de validação de especificações RT-LOTOS, baseada em simulação. Para tal, o presente artigo apresenta uma ferramenta que suporta a simulação interativa e automática das especificações, apresentando suas funcionalidades. Para uma melhor compreensão, no final do artigo é apresentado um estudo de caso, baseado na especificação de um protocolo, usando a ferramenta para a validação dos seus requisitos.
Palavras-chave:
Especificação e Validação de Sistemas, Sistemas Distribuídos Dependentes de Tempo, RT-LOTOS, Simulação
Referências
Information Processing Systems - Open Systems Interconnection - LOTOS - A formal description technique based on the temporal ordering of observational behaviour. S8807, 1988.
Quemada, J.; Fernandez, A.: Introduction of Quantitative Relative Time into LOTOS. In Protocol Specification, Testing and Verification VIL, p. 105-121, 1987
Azcorra, A. S.; Formal Modeling of Synchronous Systems. Ph.D. Thesis, Dpto. de Ingeniería de Sistemas Telemáticos, Universidad Politécnica de Madrid, Madrid, Espanha, 1990,
Regan, T; Multimidia in Temporal LOTOS. In IFIP - Protocol Specification, Testing and Verification, XIII (C-16), Dantine, A.; Leduc, G.; Wolper, P. (editors), Elsevier Science Publishers B. V. (North-Holland), p. 127-143, 1993.
Leduc, G.; Léonard, L.; A Formal Definition of Time in LOTOS. Research Report, Université de Liège, Institut d'Electricité Montefiori, Bélgica, 1994
Camargo, M. S. de; Tornando a Linguagem LOTOS Apta para Especificar Sistemas Dependentes do Tempo. Tese de Doutorado LCMI/UFSC, Florianópolis, 1995,
Working Draft on Enhancement to LOTOS, ISO/IEC JTC1/SC21/WG7, Project WI 1.21.20.2.3, January, 1997, Juan Quemada Ed.
Martins, R. F: Verificação de Sistemas Dependentes de Tempo a partir de Especificações escritas em RT-LOTOS. Dissertação de Mestrado LCMI/UFSC, Florianópolis, 1996.
Alur, R.; Henzinger, T. A.: Logics and Models for Real Time: A Survey. Proceedings of the REX Workshop, Mook, The Netherlands, June, 1991, Lecture Notes in Computer Science No.600, Springer-Verlag, 1992
Olivero, A.; Yovine, S.: KRONOS: A Tool for Verifying Real-Time Systems - User's Guide and and Reference Manual, Montbonnot Soint Martin, França, agosto 1993.
Plotkin, G. D: A Structural Approach to Operational Semantics, Report DAIMI-FN19, Computer Science Dept., Århus University, Dinamarca, 1981
Scheffel, R. M.: Um Simulador para Validação de Sistemas Dependentes de Tempo Descritos em RT-LOTOS. Dissertação de Mestrado CPGCC/UFSC, Florianópolis, 1997
Kirkwood, C. E: Verification of LOTOS Specifications using Term Rewriting Techniques Submitted for the Degree of Doctor of Philosophy. Department of Computing Science, University of Glasgow, June, 1994
Boullier, P.; Deschamp, P: Le Système SYNTAX: Manuel d'Utilisation et de Mise en Oeuvre sous UNIX. Project Languages et Traducteurs, INRIA, Setembro, 1988.
Boullier, P.; Deschamp, P.: SYNTAX: User Commands and C Library Functions. Project Languages et Traducteurs, INRIA, Junho, 1989.
Leduc, G.; Léonard, L.; Danthine, A.: The Tick-Tock case study for the assessment of timed FDTs. In the ISO95 transport service with multimidia support on HSLAN's and B-ISDN, 1994
Daws, C; Olivero, A; Yovine, S.: Verifing ET-LOTOS programs with KRONOS. In Proceedings of the FORTE'94, Berne, Switzerland, October, 1994
Courtiat, J. P.; Oliveira, R. D. de: On RT-LOTOS and its application to the formal design of multimedia protocols. In Annals of Telecommunications, vol 50, no. 1-1, p. 888-906, 1995
Courtiat, J.P. and de Camargo, M.S. and Saidouni, D.E: RT_LOTOS: LOTOS Temporisé pour la Spécification de Systèmes Temps Réel, CFIP'93 - Ingénierie des Protocoles, Dssouli, R. e Bochmann, G. von (Editeurs), HERMES, Paris, 1993
Camargo, M.S. de; Farines, J.-M.: Tornando LOTOS Apta para Especificar Sistemas Tempo-Real, Anais do 12 Simpósio Brasileiro de Redes de Computadores, Curitiba, maio, 1994.
Camargo, M.S. de; Farines, J.-M.: Uma abordagem para especificação e verificação de sistemas dependentes do tempo, Anais do IX Simpósio Brasileiro de Engenharia de Software, Recife, Outubro de 1995.
Martins, R.F.; Camargo, M.S. de; Farines, J-M.: Uma ferramenta para auxílio no processo de verificação de especificações em RT-LOTOS, Anais do X Simpósio Brasileiro de Engenharia de Software, São Carlos, Outubro de 1996
Pavón, S.; Larrabeiti, D.; Rabay, G: Lotos Laboratory - User Manual (version 3R6), LOLA/N5/V10. Departamento de Ingenieria Telematica, Universidad Politécnica de Madrid. Madrid - Espanha, 1995.
Leduc, G.; Leonard, L.; Frutos, D. de; Liana, L.; Miguel, C.; Quemada, J. e Rabay, G.: Belgian-Spanish Proposal for a Time Extended LOTOS. In J. Quemada, editor "Working Draft on Enhancements to LOTOS", ISI/IEC JTC1/SC21/WG1. October, 1994.
Quemada, J.; Fernandez, A.: Introduction of Quantitative Relative Time into LOTOS. In Protocol Specification, Testing and Verification VIL, p. 105-121, 1987
Azcorra, A. S.; Formal Modeling of Synchronous Systems. Ph.D. Thesis, Dpto. de Ingeniería de Sistemas Telemáticos, Universidad Politécnica de Madrid, Madrid, Espanha, 1990,
Regan, T; Multimidia in Temporal LOTOS. In IFIP - Protocol Specification, Testing and Verification, XIII (C-16), Dantine, A.; Leduc, G.; Wolper, P. (editors), Elsevier Science Publishers B. V. (North-Holland), p. 127-143, 1993.
Leduc, G.; Léonard, L.; A Formal Definition of Time in LOTOS. Research Report, Université de Liège, Institut d'Electricité Montefiori, Bélgica, 1994
Camargo, M. S. de; Tornando a Linguagem LOTOS Apta para Especificar Sistemas Dependentes do Tempo. Tese de Doutorado LCMI/UFSC, Florianópolis, 1995,
Working Draft on Enhancement to LOTOS, ISO/IEC JTC1/SC21/WG7, Project WI 1.21.20.2.3, January, 1997, Juan Quemada Ed.
Martins, R. F: Verificação de Sistemas Dependentes de Tempo a partir de Especificações escritas em RT-LOTOS. Dissertação de Mestrado LCMI/UFSC, Florianópolis, 1996.
Alur, R.; Henzinger, T. A.: Logics and Models for Real Time: A Survey. Proceedings of the REX Workshop, Mook, The Netherlands, June, 1991, Lecture Notes in Computer Science No.600, Springer-Verlag, 1992
Olivero, A.; Yovine, S.: KRONOS: A Tool for Verifying Real-Time Systems - User's Guide and and Reference Manual, Montbonnot Soint Martin, França, agosto 1993.
Plotkin, G. D: A Structural Approach to Operational Semantics, Report DAIMI-FN19, Computer Science Dept., Århus University, Dinamarca, 1981
Scheffel, R. M.: Um Simulador para Validação de Sistemas Dependentes de Tempo Descritos em RT-LOTOS. Dissertação de Mestrado CPGCC/UFSC, Florianópolis, 1997
Kirkwood, C. E: Verification of LOTOS Specifications using Term Rewriting Techniques Submitted for the Degree of Doctor of Philosophy. Department of Computing Science, University of Glasgow, June, 1994
Boullier, P.; Deschamp, P: Le Système SYNTAX: Manuel d'Utilisation et de Mise en Oeuvre sous UNIX. Project Languages et Traducteurs, INRIA, Setembro, 1988.
Boullier, P.; Deschamp, P.: SYNTAX: User Commands and C Library Functions. Project Languages et Traducteurs, INRIA, Junho, 1989.
Leduc, G.; Léonard, L.; Danthine, A.: The Tick-Tock case study for the assessment of timed FDTs. In the ISO95 transport service with multimidia support on HSLAN's and B-ISDN, 1994
Daws, C; Olivero, A; Yovine, S.: Verifing ET-LOTOS programs with KRONOS. In Proceedings of the FORTE'94, Berne, Switzerland, October, 1994
Courtiat, J. P.; Oliveira, R. D. de: On RT-LOTOS and its application to the formal design of multimedia protocols. In Annals of Telecommunications, vol 50, no. 1-1, p. 888-906, 1995
Courtiat, J.P. and de Camargo, M.S. and Saidouni, D.E: RT_LOTOS: LOTOS Temporisé pour la Spécification de Systèmes Temps Réel, CFIP'93 - Ingénierie des Protocoles, Dssouli, R. e Bochmann, G. von (Editeurs), HERMES, Paris, 1993
Camargo, M.S. de; Farines, J.-M.: Tornando LOTOS Apta para Especificar Sistemas Tempo-Real, Anais do 12 Simpósio Brasileiro de Redes de Computadores, Curitiba, maio, 1994.
Camargo, M.S. de; Farines, J.-M.: Uma abordagem para especificação e verificação de sistemas dependentes do tempo, Anais do IX Simpósio Brasileiro de Engenharia de Software, Recife, Outubro de 1995.
Martins, R.F.; Camargo, M.S. de; Farines, J-M.: Uma ferramenta para auxílio no processo de verificação de especificações em RT-LOTOS, Anais do X Simpósio Brasileiro de Engenharia de Software, São Carlos, Outubro de 1996
Pavón, S.; Larrabeiti, D.; Rabay, G: Lotos Laboratory - User Manual (version 3R6), LOLA/N5/V10. Departamento de Ingenieria Telematica, Universidad Politécnica de Madrid. Madrid - Espanha, 1995.
Leduc, G.; Leonard, L.; Frutos, D. de; Liana, L.; Miguel, C.; Quemada, J. e Rabay, G.: Belgian-Spanish Proposal for a Time Extended LOTOS. In J. Quemada, editor "Working Draft on Enhancements to LOTOS", ISI/IEC JTC1/SC21/WG1. October, 1994.
Publicado
15/10/1997
Como Citar
SCHEFFEL, Roberto Milton; CAMARGO, Murilo Silva de.
Validação de Especificações Formais de Sistemas Dependentes de Tempo Através de Simulação. In: SIMPÓSIO BRASILEIRO DE ENGENHARIA DE SOFTWARE (SBES), 11. , 1997, Recife/PE.
Anais [...].
Porto Alegre: Sociedade Brasileira de Computação,
1997
.
p. 215-230.
DOI: https://doi.org/10.5753/sbes.1997.24050.
