Repositório Digital

A- A A+

Formal specification and verification of real-time systems usinggraph grammars

.

Formal specification and verification of real-time systems usinggraph grammars

Mostrar registro completo

Estatísticas

Título Formal specification and verification of real-time systems usinggraph grammars
Autor Michelon, Leonardo
Costa, Simone Andre da
Ribeiro, Leila
Abstract The importance of real-time systems has enormously increased in the last decade. Application areas that typically need real-time models include railroad systems, intelligent vehicle highway systems, avionics, multimedia and telephony. To assure that such systems are correct, additionally to prove that they provide the required functionality, time constraints must be satisfied. There are already formal specification methods for real-time systems, but most of them are difficult to use by software developers, that are usually not very familiar with mathematical notation but rather specify systems using the objectoriented paradigm. In this paper we propose a formal approach to specify and analyze real-time systems that has an object-oriented flavor. This approach is based on Object-Based Graph Grammars (OBGGs), a formal description technique suitable for the specification of asynchronous distributed systems, and intuitive even for nontheoreticians. We extend OBGGs to enable explicit modeling of time constraints, and define the semantics of the specifications via transition systems. Finally, we translate timed OBGGs to Timed Automata, a formal notation that is wide spread in the area of real-time systems modeling and allows the automatic verification of properties.
Contido em Journal of the Brazilian Computer Society. Vol. 13, no. 4 (Dec. 2007), p. 51-68
Assunto Gramatica : Grafos
sistemas : tempo real
[en] Formal specification and verification
[en] Graph grammars
[en] Real-time computing
[en] Timed automata
Origem Nacional
Tipo Artigo de periódico
URI http://hdl.handle.net/10183/72572
Arquivos Descrição Formato
000629169.pdf (404.8Kb) Texto completo (inglês) Adobe PDF Visualizar/abrir

Este item está licenciado na Creative Commons License

Este item aparece na(s) seguinte(s) coleção(ões)


Mostrar registro completo

Percorrer



  • O autor é titular dos direitos autorais dos documentos disponíveis neste repositório e é vedada, nos termos da lei, a comercialização de qualquer espécie sem sua autorização prévia.
    Projeto gráfico elaborado pelo Caixola - Clube de Criação Fabico/UFRGS Powered by DSpace software, Version 1.8.1.