Formal Specification and Verification of Real-Time Systems using Graph Grammars

Leonardo MichelonSimone André da CostaLeila Ribeiro

The importance of real-time systems has enormouslyincreased in the last decade. Application areas that typicallyneed real-time models include railroad systems, intelligentvehicle highway systems, avionics, multimediaand telephony. To assure that such systems are correct,additionally to prove that they provide the required functionality,time constraints must be satisfied. There are alreadyformal specification methods for real-time systems,but most of them are difficult to use by software developers,that are usually not very familiar with mathematicalnotation but rather specify systems using the objectorientedparadigm. In this paper we propose a formalapproach to specify and analyze real-time systems thathas an object-oriented flavor. This approach is based onObject-Based Graph Grammars (OBGGs), a formal descriptiontechnique suitable for the specification of asynchronousdistributed systems, and intuitive even for nontheoreticians.We extend OBGGs to enable explicit modelingof time constraints, and define the semantics of thespecifications via transition systems. Finally, we translatetimed OBGGs to Timed Automata, a formal notation thatis wide spread in the area of real-time systems modelingand allows the automatic verification of properties.

Caso o link acima esteja inválido, faça uma busca pelo texto completo na Web: Buscar na Web

Biblioteca Digital Brasileira de Computação - Contato:
     Mantida por: