Formal specification and verification of real-time systems usinggraph grammars
dc.contributor.author | Michelon, Leonardo | pt_BR |
dc.contributor.author | Costa, Simone Andre da | pt_BR |
dc.contributor.author | Ribeiro, Leila | pt_BR |
dc.date.accessioned | 2013-06-19T01:43:49Z | pt_BR |
dc.date.issued | 2007 | pt_BR |
dc.identifier.issn | 0104-6500 | pt_BR |
dc.identifier.uri | http://hdl.handle.net/10183/72572 | pt_BR |
dc.description.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. | en |
dc.format.mimetype | application/pdf | |
dc.language.iso | eng | pt_BR |
dc.relation.ispartof | Journal of the Brazilian Computer Society. Vol. 13, no. 4 (Dec. 2007), p. 51-68 | pt_BR |
dc.rights | Open Access | en |
dc.subject | Gramatica : Grafos | pt_BR |
dc.subject | Real-time computing | en |
dc.subject | Formal specification and verification | en |
dc.subject | sistemas : tempo real | pt_BR |
dc.subject | Graph grammars | en |
dc.subject | Timed automata | en |
dc.title | Formal specification and verification of real-time systems usinggraph grammars | pt_BR |
dc.type | Artigo de periódico | pt_BR |
dc.identifier.nrb | 000629169 | pt_BR |
dc.type.origin | Nacional | pt_BR |
Este item está licenciado na Creative Commons License
-
Artigos de Periódicos (39150)Ciências Exatas e da Terra (5955)