Differential predicate transition Petri nets and objects, an aid for proving properties in hybrid systems

E. Villani*, J.C. Pascal**, P.E. Miyagi*, R. Valette**
*Dep. Mecatrônica, EPUSP, São Paulo, Brasil
**LAAS-CNRS, F-31077 Toulouse Cedex 4, France

Presented at:
ADHS 2003, IFAC Conference on Analysis and Design of Hybrid Systems, Saint-Malo, France, June 16-18, 2003, p.117-122

Abstract

This paper introduces a new approach for the verification of behaviour properties in hybrid systems. By using Petri nets and object oriented concepts the proof of a system property 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 case of proving safety properties. Copyright © 2002 IFAC

Keywords

Petri nets, object modelling techniques, differential equations