» Download Article
A Contribution to the Validation to of Operating Mode Switching: Application to Satellite
World Congress, Volume # 17 | Part# 1
Authors
Gonzalez Berlanga, Saul Israel; Niel, Eric; Zouari, Belhassen; Blanquart, Jean-Paul
Identifier
10.3182/20080706-5-KR-1001.01107
Index Terms
Discrete event systems modeling and control; Switched discrete and hybrid systems; Verification
Abstract
We propose a methodology for modeling systems with different operating modes using Nested Petri Nets (NPNs) based on Valks approach, where each token can be also considered as one Petri Net. NPNs provide a powerful tool for concurrent modeling and introduce interesting properties such as synchronization at a hierarchical level. In order to manage operating modes of critical and complex systems these properties are used to define and link component behaviors to the global system, through synchronized transitions. In order to formally verify these properties, CTL formulae will be used, translated from a logical table of technical specifications. The formulae allow a formal validation of the model and an examination of its coherency when the system switches to a new operating mode, under the influence of exceptional events. This verification is possible namely by using logic programming tools for the simulation and model checking. It is illustrated through a case study concerning a satellites control unit.
References
REFERENCES E. Asarin and O. Bournez, and T. Dang and O. Maler and A. Pnueli. Effective Synthesis of Switching Controllers for Linear System, Proceedings of IEEE, vol. 88, pp. 1011-1025. B. Berard. Model-checking temporisé, Ecole d’été temps réel, ERT 2007, Nantes, pp.97-109, 2007. N. Hamani, and N. Dangoumau, and Craye, E. (2004) "A formal approach for reactive mode handling", IEEE, SMC04, pp. 4306-4311, The Hague, Netherlands. O. Kammach, and L. Pietrac, and E. Niel. Multi-Model approach to Discrete Events Systems: Application to operating mode management, Mathematics and Computers in Simulation, vol. 70, n°5-6, p. 394-407, 2005. M. Leuschel and B. Farwer.(2004) Model Checking Object Petri Nets in Prolog, PPDP’04, August 24–26, 2004, Verona, Italy. I. A. Lomazova. Nested Petri nets — a formalism for specification of multi-agent distributed systems. Concurrency Specification and Programming (CSP’99), Proceedings, pages 127–140. M. Nourelfath, and E. Niel, Modular supervisory control of an experimental automated manufacturing system, Control Engineering Practice, vol. 12, n°2, pp. 205-216, 2004. R. Valk. Petri nets as token objects. An introduction to elementary object nets. Applications and Theory of Petri Nets 1998. Proceedings, volume 1420, pages 1–25. Springer-Verlag, 1998. M. Zefran, and J. Burdick. Design of switching controllers for systems with changing dynamics, 37th CDC, pp. 2113-2118, Phoenix, Arizona, USA. B. Zouari and R. Frefrita and E. Niel. A colored Petri net approach for the management of operating modes in discrete event systems, IFAC MCPL, Sibiu, Romania September 27-30-2007.