E. Villani*, F. Junqueira*, P.E. Miyagi*, R. Valette**
*Dep. Mecatrônica, EPUSP, São Paulo, Brasil
**LAAS-CNRS,
F-31077 Toulouse Cedex 4, France
Presented at:
COBEM 2003, 17th International Congress of Mechanical Engineering,
November 10-14, 2003, São Paulo, Brazil,
p. 0348.
This work considers the combined used of Petri nets and object-oriented concepts for the modelling and analysis of control systems. The object modularity is explored in order to deal with the system complexity in both modelling and analysis. According to the proposed approach, the verification of behaviour properties is reduced from a complex proof involving the overall model to a set of simpler proofs involving the model of one or a few objects. Each local proof is made considering a set of hypotheses that should then be proven. Particularly, this paper considers the landing system of the military aircraft Rafale (Dassault Aviation) as a case-study. The aim is to test the proposed approach for real systems with a high level of complexity.
Verification, object-orientation, Petri nets, hybrid systems.