» Download Article

Authors
Ruel, Silvain; de Smet, Olivier; Faure, Jean-Marc

Identifier
10.3182/20080706-5-KR-1001.00860

Index Terms
Verification; Control over communication; Discrete event systems modeling and control

Abstract
Networked automation architectures with Ethernet-based fieldbuses instead of traditional fieldbuses are more and more often used in industry, even for critical systems such as chemical or nuclear power plants. The strong safety requirements of these processes impose to evaluate the time performances of these complex architectures. Formal verification techniques are promising solutions to reach this objective. Hence, this paper focuses on the applicability of formal verification techniques to check time performances. On the basis of a case study, it is shown how formal models of networked automation architectures which are simple enough to be checked by existing timed model-checkers while yielding meaningful results can be developed.

References

R. Alur and D. L. Dill. A theory of timed automata. 126:
183�235, 1994.

C. G. Cassandras and S. Lafortune. Introduction to
Dioscrete Event Systems. Kluwer Academic Publishers,
1999.

E. M. Clarke and E. A. Emerson. Design and synthesis
of synchronization skeletons using branching time temporal
logic. In Logics of Programs Workshop, Yorktown
Heights, New-York, 1981.

B. Denis, S. Ruel, J.-M. Faure, G. Marsal, and G. Frey.
Measuring the impact of vertical integration on response
times in Ethernet fieldbuses. In Proc. of ETFA�07, 2007.

J.-P. Georges, E. Rondeau, and T. Divoux. How to be
sure that Ethernet networks will satisfy the real-time
requirements? In Proc. of IEEE Int. Symposium on
Industrial Electronics, July 2002.

J. Greifeneider and G. Frey. Probabilistic timed automata
for modeling networked automation systems. In proc.
1st IFAC DCDS, Cachan, pages 143 � 148, 2007.

M.-H. Hung, J. Tsai, F.-T. Cheng, and H.-C. Yang.
Development of an Ethernet-based equipment integration
framework for factory automation. Robotics and
Computer-Integrated Manufacturing, 20:369�383, 2004.

K. G. Larsen, P. Pettersson, and W. Yi. Uppaal in
a nutshell. Journal of Software Tools for Technology
Transfer, 1(1-2):134�152, 1997.

K. C. Lee and S. Lee. Performance evaluation of switched
Ethernet for real-time industrial communications. Computer
standards & interfaces, (24):411�423, 2002.

G. Marsal. Evaluation of time performances of Ethernetbased
automation systems by simulation of high-level
Petri nets. PhD thesis, ENS Cachan (France) and
Kaiserslautern University (Germany), December 2006.

N. Pereira, E. Tovar, and L. M. Pinho. Timeliness in
COTS factory-floor distributed systems: what role for
simulation? In Proc. of 9th IEEE Int. Conf. on Emerging
Technologies and Factory Automation, September
2004.

R. Viegas, R.A.M. Valentim, D.G. Texeira, and L.A.
Guedes. Analysis of protocols to Ethernet automation
networks. In Proc. of International Joint Conference
SICE-ICASE, pages 4981�4985, 2006.

D.Witsch, B. Vogel-Heuser, J.M. Faure, and G. Poulard-
Marsal. Performance analysis of industrial Ethernet
networks by means of timed model-checking. In Proc.
of 12th IFAC Symposium on Information Control Problems
in Manufacturing (INCOM 2006), pages 101�106,
2006.

D. A. Zaitsev. Switched LAN simulation by colored Petri
nets. Mathematics and Computers in Simulation, 65(3):
245�249, 2004.