The association ends at the basis of a formal validation

Author

Bouabana-Tebibel, Thouraya ; Belmesk, Mounira

Author_Institution

Nat. Inst. of Comput. Sci., Alger

fYear

2006

fDate

21-23 June 2006

Firstpage

959

Lastpage

964

Abstract

The object constraint language OCL is an extension of the UML notation for the expression of restrictions over the static and dynamic diagrams. We propose to take advantage of its formal capabilities for validating whether the UML model matches with the system properties. For this purpose, we develop an approach based on Petri nets and temporal logics. This approach allows the non trivial integration of the temporal logic properties translated from the OCL invariants with the Petri nets obtained from the UML modeling. A case study is given throughout the paper to illustrate the approach

Keywords

Petri nets; Unified Modeling Language; formal verification; object-oriented languages; temporal logic; OCL invariant; Petri nets; UML model notation; dynamic diagram; formal validation; object constraint language; static diagram; temporal logic; Abstracts; Automatic logic units; Computer science; Costs; Formal verification; Petri nets; Unified modeling language; OCL; Petri nets; UML; temporal logics; verification;

fLanguage

English

Publisher

ieee

Conference_Titel

Service Operations and Logistics, and Informatics, 2006. SOLI '06. IEEE International Conference on

Conference_Location

Shanghai

Print_ISBN

1-4244-0317-0

Electronic_ISBN

1-4244-0318-9

Type

conf

DOI

10.1109/SOLI.2006.328880

Filename

4125715