Uma ferramenta para auxílio no processo de verificação de especificações em RT-LOTOS
Resumo
In this paper, we present a methodology and tools for verifying specifications of real-time systems, written in RT-LOTOS, a timed extension of the LOTOS specification language. From the model in RT-LOTOS, it is generated the related Timed Automata, over which the verification can be done, by using formulas written in the TCTL Real-Time Temporal Logic. The translator of RT-LOTOS specifications into Timed Automata that was built is described in this work. His integration with existing tools that allow the verification is also shown. Finally, case-studies allow to analyze the use of this method and the tools presented.
Palavras-chave:
LOTOS, Real-Time Systems, Symbolic Model Checking
Referências
R. Alur, C. Courcoubetis and D. Dill. Model Checking for Real-Time Systems. In Procs. of the 5th IEEE Symposium on Logic in Computer Science, 1990.
R. Alur and D. Dill. The theory of Timed Automata. Proccedings of the REX Workshop, Lecture Notes in Computer Science No. 600, Mook, The Netherlands, June, 1991.
R. Alur and T. A. Henzinger. Logics and Models for Real Time: A Survey. In Procs. of the REX Workshop, Mook, The Netherlands, June, 1991, Lecture Notes in Computer Science No. 600, Springer-Verlag, 1992.
T. Bolognesi, F. Lucidi and S. Trigila. Converging Towards a Timed-LOTOS Standard. Reserarch CNUCE/C.R.N., Pisa, Itália, 1993.
P. Boullier et P. Deschamp. Le Système SYNTAX: Manuel d'Utilisation et de Mise en Oeuvre sous UNIX. Project Langages et Traducteurs, INRIA, setembro, 1988.
M. S. de Camargo. Tornando a Linguagem LOTOS Apta para Especificar Sistemas Dependentes do Tempo. Tese de Doutorado LCMI/UFSC, Florianópolis, 1995.
M.S. de Camargo e J. -M. Farines. Uma abordagem para especificação e verificação de sistemas dependentes do tempo. IX SBES, 1995.
E. M. Clarke, E. A. Emerson and A. P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems, 8(2):244-263, 1986.
J.-P. Courtiat and R. C. Oliveira. About time nondeterminism and exception handling in a temporal extension of LOTOS. In Protocol Specification, Testing and Verification XIV, pages 37-52, Canada, 1994.
J. -P. Courtiat and R. C. Oliveira. RT-LOTOS and its application to multimedia protocol specification and validation. MnNet'95 - International Conference on Multimedia and Networking, Aizu, Japan, September, 1995.
C. Daws, A. Olivero and S. Yovine. Verifying ET-LOTOS programs with KRONOS. In Proceedings of the FORTE94, Berne, Switzerland, Outubro, 1994.
H. Garavel. Compilation et Vérification of LOTOS Programs. Thèse de Docteur de lUniversité Joseph Fourier - Grenoble I, França, Novembro, 1989.
C. Heitmeyer and N. Lynch. The Generalized RailRoad Crossing: A case study in formal verification of real-time systems. Laboratory for Computer Science - MIT, Cambridge, Massachusetts, November, 1994.
T. A. Henzinger and P. -H. Ho. HyTech: The Cornell HYbrid TECHnology Tool. In Hybrid Systems II, Lecture Notes in Computer Science 999, Springer-Verlag, 1995, pp. 265-294.
T. A. Henzinger, X. Nicollin, J. Sifakis and S. Yovine. Symbolic model-checking for real-time systems. In Procs. of 7th LICS, IEEE Computer Society Press, 1992.
L. Lamport. A fast mutual exclusion algorithm. ACM Transactions on Computer Systems, 5(1):1-11, fevereiro, 1987.
G. Leduc and L. Léonard. A Formal Definition of Time in LOTOS. Research Report, Université de Liège, Institut d'Electricité Montefiori, Bélgica, 1994.
V. Luchangco, E. Söylemez, S. Garland and N. Lynch. Verifying Timing Properties of Concurrent Algorithms. In Proc. FORTE'94, Berne, Swtzerland, outubro, 1994.
R.F. Martins. Verificação de sistemas dependentes do tempo a partir de especificações escritas em RT-LOTOS. Dissertação de Mestrado LCMI/UFSC, Florianópolis, Junho, 1996.
B. Meyer. Introduction to the Theory of Programming Languages. International Series in Computer Science, Prentice-Hall, 1990.
X. Nicollin. ATP: une algèbre pour la spécification et l'analyse des systèmes temps reel. Thèse, Institut National Polytechnique de Grenoble, France, maio, 1992.
A. Olivero and S. Yovine. KRONOS: A Tool for Verifying Real-Time Systems, User's Guide and Reference Manual. Montbonnot Soint Martin, França, agosto, 1993.
T. Regan. Multimidia in Temporal LOTOS. In IFIP - Protocol Specification, Testing and Verification, XII (C-16), Dantine, A.; Leduc, G.; Wolper, P. (Editors), Elsevier Science Publishers B.V. (North-Holland), pp. 127-143, 1998.
J. -B. Stefani, L. Hazard and F. Horn. Computational model for distributed multimedia applications based on a aynchronous programming language. Computer Communications, 15(2):114-128, March, 1992.
S. Yovine. Méthodes et Outils pour la Vérification Symbolique de Systèmes Temporisés. Thèse de Docteur de l'Institut National Polytechnique de Grenoble - Grenoble, França, Maio, 1993.
R. Alur and D. Dill. The theory of Timed Automata. Proccedings of the REX Workshop, Lecture Notes in Computer Science No. 600, Mook, The Netherlands, June, 1991.
R. Alur and T. A. Henzinger. Logics and Models for Real Time: A Survey. In Procs. of the REX Workshop, Mook, The Netherlands, June, 1991, Lecture Notes in Computer Science No. 600, Springer-Verlag, 1992.
T. Bolognesi, F. Lucidi and S. Trigila. Converging Towards a Timed-LOTOS Standard. Reserarch CNUCE/C.R.N., Pisa, Itália, 1993.
P. Boullier et P. Deschamp. Le Système SYNTAX: Manuel d'Utilisation et de Mise en Oeuvre sous UNIX. Project Langages et Traducteurs, INRIA, setembro, 1988.
M. S. de Camargo. Tornando a Linguagem LOTOS Apta para Especificar Sistemas Dependentes do Tempo. Tese de Doutorado LCMI/UFSC, Florianópolis, 1995.
M.S. de Camargo e J. -M. Farines. Uma abordagem para especificação e verificação de sistemas dependentes do tempo. IX SBES, 1995.
E. M. Clarke, E. A. Emerson and A. P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems, 8(2):244-263, 1986.
J.-P. Courtiat and R. C. Oliveira. About time nondeterminism and exception handling in a temporal extension of LOTOS. In Protocol Specification, Testing and Verification XIV, pages 37-52, Canada, 1994.
J. -P. Courtiat and R. C. Oliveira. RT-LOTOS and its application to multimedia protocol specification and validation. MnNet'95 - International Conference on Multimedia and Networking, Aizu, Japan, September, 1995.
C. Daws, A. Olivero and S. Yovine. Verifying ET-LOTOS programs with KRONOS. In Proceedings of the FORTE94, Berne, Switzerland, Outubro, 1994.
H. Garavel. Compilation et Vérification of LOTOS Programs. Thèse de Docteur de lUniversité Joseph Fourier - Grenoble I, França, Novembro, 1989.
C. Heitmeyer and N. Lynch. The Generalized RailRoad Crossing: A case study in formal verification of real-time systems. Laboratory for Computer Science - MIT, Cambridge, Massachusetts, November, 1994.
T. A. Henzinger and P. -H. Ho. HyTech: The Cornell HYbrid TECHnology Tool. In Hybrid Systems II, Lecture Notes in Computer Science 999, Springer-Verlag, 1995, pp. 265-294.
T. A. Henzinger, X. Nicollin, J. Sifakis and S. Yovine. Symbolic model-checking for real-time systems. In Procs. of 7th LICS, IEEE Computer Society Press, 1992.
L. Lamport. A fast mutual exclusion algorithm. ACM Transactions on Computer Systems, 5(1):1-11, fevereiro, 1987.
G. Leduc and L. Léonard. A Formal Definition of Time in LOTOS. Research Report, Université de Liège, Institut d'Electricité Montefiori, Bélgica, 1994.
V. Luchangco, E. Söylemez, S. Garland and N. Lynch. Verifying Timing Properties of Concurrent Algorithms. In Proc. FORTE'94, Berne, Swtzerland, outubro, 1994.
R.F. Martins. Verificação de sistemas dependentes do tempo a partir de especificações escritas em RT-LOTOS. Dissertação de Mestrado LCMI/UFSC, Florianópolis, Junho, 1996.
B. Meyer. Introduction to the Theory of Programming Languages. International Series in Computer Science, Prentice-Hall, 1990.
X. Nicollin. ATP: une algèbre pour la spécification et l'analyse des systèmes temps reel. Thèse, Institut National Polytechnique de Grenoble, France, maio, 1992.
A. Olivero and S. Yovine. KRONOS: A Tool for Verifying Real-Time Systems, User's Guide and Reference Manual. Montbonnot Soint Martin, França, agosto, 1993.
T. Regan. Multimidia in Temporal LOTOS. In IFIP - Protocol Specification, Testing and Verification, XII (C-16), Dantine, A.; Leduc, G.; Wolper, P. (Editors), Elsevier Science Publishers B.V. (North-Holland), pp. 127-143, 1998.
J. -B. Stefani, L. Hazard and F. Horn. Computational model for distributed multimedia applications based on a aynchronous programming language. Computer Communications, 15(2):114-128, March, 1992.
S. Yovine. Méthodes et Outils pour la Vérification Symbolique de Systèmes Temporisés. Thèse de Docteur de l'Institut National Polytechnique de Grenoble - Grenoble, França, Maio, 1993.
Publicado
14/10/1996
Como Citar
MARTINS, Ricardo Ferreira; CAMARGO, Murilo Silva de; FARINES, Jean-Marie.
Uma ferramenta para auxílio no processo de verificação de especificações em RT-LOTOS. In: SIMPÓSIO BRASILEIRO DE ENGENHARIA DE SOFTWARE (SBES), 10. , 1996, São Carlos/SP.
Anais [...].
Porto Alegre: Sociedade Brasileira de Computação,
1996
.
p. 259-274.
DOI: https://doi.org/10.5753/sbes.1996.24447.
