BDBComp
Parceria:
SBC
Petri net and UML for the V&V of ITASAT Satellite Prototype

Eduardo CorreiaPaulo VerasOsamu SaotomeEmilia Villani

This paper approaches the process of validating and verifying the embedded control system of a satellite prototype. The focus of this approach is on the integration of UML and Petri nets, aiming at the formal verification of the system requirements. The approach is composed of: (1) simulation of the UML model in a CASE tool; (2) simulation of the Petri net model in a Petri net simulator; and (3) formal verification of the Petri net model. The Petri net model is obtained from the UML statecharts by applying a set of rules. The formal verification is done by associating the system requirements to Petri net properties that are proved using Petri net analysis methods.

http://www.lbd.dcc.ufmg.br/colecoes/wtr/2008/016.pdf

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: bdbcomp@lbd.dcc.ufmg.br
     Mantida por:
LBD