directional valve 3/2 way normally closed with 
spring return (H). 
The second security requirement, related with 
the stop the filling operation, was performed through 
the turn OFF of the filling directional valve 2/2 way 
normally closed with spring return (D). 
The figure 9 shows the total controller SFC 
specification based on the GEMMA implementation 
with the single SFC method (see section 2.2). 
 
Figure 9: Total SFC controller specification with 
emergence sequence. 
All the controller specification, presented on the 
previous figure, was simulated on Automation Studio 
Software. The obtained results leaded to the conclusions 
that all the requirements defined on the Emergency Stop 
Standards, were accomplished. 
Further, the specification was translated to Ladder 
Diagrams according to the SFC algebraic formalization 
and implemented on a Programmable Logic Controller 
(PLC) adopted as the controller physical device. This part 
of the developed work is not detailed on this publication. 
5  CONCLUSIONS 
It was presented, on a systematic way, the adopted 
techniques for the emergency stop behavior 
specification of automation systems. 
The ways to translate the GEMMA graphical chart 
to the low level specification was also presented and 
discussed. 
The standards (EN418, EN60204-1) related with the 
stop emergency specifications were considered and 
all the requirements were accomplished. 
The obtained results, by simulation with Automation 
Studio software, show that the adopted approach is 
adequate. 
Further work will be devoted, in one hand, to the 
application of formal methods to verify some 
important system’s behavior (taking into account the 
discrete behavior of the system) and, in other hand, 
the application of modeling techniques for hybrid 
systems and respective tools for simulation and 
formal verification. 
REFERENCES 
ADEPA, 1992. GEMMA (2nd Edition) – Guide d`Étude 
des Modes de Marches et d`Arrêts. 
Automation Studio, 2004. Famic Technologies inc., 
Automation Studio 5.0, 
http://www.automationstudio.com. 
Baresi L., Mauri M., Pezzè M., 2002. PLCTools: Graph 
Transformation Meets PLC Design. Electronic Notes 
in Theoretical Computer Science, Vol. 72, No. 2. 
Elmqvist E., Mattson S., 1997. An Introduction to the 
Physical Modelling Language Modelica. ESS'97. 
Passau, Germany. 
EN 418, 1992. Safety of machinery. Emergency stop 
equipment, functional aspects. Principles for design. 
European Standard. 
EN 60204-1, 1997. Safety of Machinery - Electrical 
Equipment of Machines - Part 1: General 
Requirements-IEC 60204-1. European Standard. 
Frey G., Litz L., 2000. Formal methods in PLC 
programming. IEEE Conference on Systems, Man and 
Cybernetics, SMC 2000, Nashville, October 8-11. 
IEC 60848, 1998. Specification language GRAFCET for 
sequential function chart. ed. 2. 
Klein S., 2005. Fault detection of discrete event systems 
using an identification approach. PhD Thesis, 
University of Kaiserslautern. 
Machado, J., Seabra, E. A. R., 2008. Real-Time Systems 
Safety Control considering Human-Machine Interface. 
ICINCO’2008, May 10-14, Funchal, Madeira, 
Portugal,. 6p. 
Machado, J., Seabra, E. A. R., Campos, J., Soares, F. O., 
Leão, C. P., Silva, J. C. L., 2008. Simulation and 
Formal Verification of Industrial Systems Controllers. 
Symp. Series in Mech.; Vol. 3, pp.461-470. 
Otter M., Årzén K., Dressler I., 2005. TaskGraph - A 
Modelica Library for Hierarchical Task Machines. 
Modelica 2005 Proceedings. 
Seabra, E. A. R., Machado, J., Silva, J. C. L., Soares, F. 
O., Leão, C. P., 2007. Simulation and Formal 
Verification of Real Time Systems: A Case Study. 
ICINCO’2007, Angers, France; May 9-12, 6p. 
Ramadge P. J. and Wonham W. M., 1987. Supervisory 
control of a class of discrete event processes. SIAM J. 
Control Optimization, 25(1), pp. 206-230. 
Rossi O., 2004. Validation formelle de programmes 
Ladder Diagram pour Automates Programmables 
industriels. PhD Thesis, École Normale Supérieure de 
Cachan. 
SAFE CONTROLLERS DESIGN FOR HIBRID PLANTS - The Emergency Stop
177