Model checking in object-oriented Petri nets

Author

Rodrigues, Cássio L. ; Guerrero, Dalton D S ; De Figueiredo, Jorge C A

Author_Institution

Fed. Univ. of Campina Grande, Brazil

Volume

5

fYear

2004

fDate

10-13 Oct. 2004

Firstpage

4977

Abstract

We present model checking techniques for verifying an object oriented Petri net modeling language (RPOO). Our intention is turn the application of model checking on model-based software development more feasible. In order that we provide means of specifying objects properties regardless Petri nets details. We use Petri nets semantics just to construct the models state space. We present our algorithms to evaluate properties expressed in branching-time temporal logic CTL. We deal with explicit representation of state space emphasizing its OO features. Besides, we remark the results of some applications of our model checker.

Keywords

Petri nets; object-oriented languages; program verification; software engineering; specification languages; branching-time temporal logic CTL; model checking; model-based software development; object-oriented Petri net modeling language; Application software; Concurrent computing; Lead; Logic; Object oriented modeling; Parallel processing; Petri nets; Programming; Software systems; State-space methods;

fLanguage

English

Publisher

ieee

Conference_Titel

Systems, Man and Cybernetics, 2004 IEEE International Conference on

ISSN

1062-922X

Print_ISBN

0-7803-8566-7

Type

conf

DOI

10.1109/ICSMC.2004.1401320

Filename

1401320