The paper considers the co-ordination and control of flexible, independently driven, multiaxis, high-speed machinery in which mechanical complexity has been exchanged for sophistication in control. The control of such machines is a hybrid control problem and the paper addresses the specification and design of the discrete event part of the controller. It focuses on the design of synchronisation logic for the event-driven real-time co-ordination and synchronisation of the machine. For such time-critical and system-critical applications, it is imperative that system behaviour is fully understood and unambiguous. The paper proposes a method for inferring system behaviour and performing formal verification of machine systems specified using a subset of the industry standard IEC 1131 sequential function charts (SFC). It shows how an SFC-based design can be translated to an equivalent Petri net model, thereby allowing Petri net theory and analysis techniques to probe its behaviour and verify its functionality. The approach is demonstrated by considering the design of synchronisation logic for a prototype six-axis high-speed packaging machine which incorporates both time-critical and system-critical functions.
References
-
-
1)
-
Mallaband, S.: `Specification of real time control systems by means of sequential functioncharts', International conference on Software engineering for real-timesystems, 16–18 September 1991, p. 57–61.
-
2)
-
J.S. Sagoo ,
D.J. Holding
.
A comparison of temporal Petri net based techniques in the specificationand design of hard real-time systems.
Microprocess. Microprogr.
,
111 -
118
-
3)
-
C.A.R. Hoare
.
(1985)
Communicating sequential processes.
-
4)
-
David, R.: `Modelling of dynamic systems by Petri nets', ECC 91 European Control conference, 2–5 July 1991, Laboratoire d'Automatique de GrenobleGrenoble, France, p. 136–147.
-
5)
-
D.J. Holding ,
J.S. Sagoo ,
G.W. Irwin ,
P.J. Fleming
.
(1992)
A formal approach to the software control of high-speed machinery, Transputers in real-time control.
-
6)
-
T. Murata
.
Petri nets: Properties, analysis and applications.
Proc. IEEE
,
4 ,
541 -
580
-
7)
-
IEC 1131, International Electrotechnical Commission:‘Internationalstandardfor programmable controllers, programming languages’, March 1993.
-
8)
-
X. He ,
J.A.N. Lee
.
Integrating predicate transition nets with first order temporal logicin thespecification and analysis of concurrent systems.
Form. Asp. Comput.
,
226 -
246
-
9)
-
L.E. Holloway ,
B.H. Krogh
.
Synthesis of feedback control logic for a class of controlled Petri nets.
IEEE Trans. Autom. Control
,
5 ,
514 -
523
-
10)
-
P.M. Merlin ,
D.J. Farber
.
Recoverability of communication protocols, implications of a theoreticalstudy.
IEEE Trans.
,
1036 -
1043
-
11)
-
N.G. Levenson ,
J.L. Stolzy
.
Safety analysis using Petri nets.
IEEE Trans. Softw. Eng.
,
3 ,
386 -
397
-
12)
-
A.A. Desrochers ,
R.Y. Al-Jaar
.
(1995)
Applications of Petri nets in manufacturing systems.
-
13)
-
R. Zurawski ,
M.C. Zhou
.
Petri nets and industrial applications: A tutorial.
IEEE Trans. Indust.Electron.
,
6 ,
567 -
585
-
14)
-
J.L. Peterson
.
(1981)
Petri net theory and the modelling of systems.
-
15)
-
I. Suzuki ,
H. Lu
.
Temporal Petri nets and their application to modelling and analysis ofa handshake daisy chain arbiter.
IEEE Trans. Comput.
,
5 ,
641 -
704
-
16)
-
Jiang, J., Holding, D.J.: `The formalisation and analysis of sequential function charts using aPetri net approach', 13th IFAC world congress, IFAC'96, 1996, San Francisco, in press.
-
17)
-
W. Reisig
.
(1985)
Petri nets: an introduction.
-
18)
-
H. Langmaack ,
W.-P. de Roever ,
S. Vytopil
.
(1994)
Formal techniques in real-time and fault-tolerant systems.
-
19)
-
D. Skeen ,
M. Stonebraker
.
A formal model of crash recovery in a distributed system.
IEEE Trans. Softw. Eng.
,
3 ,
213 -
228
-
20)
-
P.J. Antsaklis ,
W. Kohn ,
A. Nerode ,
S. Sastry
.
(1998)
Hybrid systems.
-
21)
-
N.G. Levenson
.
(1995)
Safeware – system safety and computers.
-
22)
-
L. Lamport
.
Proving the correctness of multiprocess programs.
IEEE Trans. Softw. Eng.
,
2 ,
125 -
143
-
23)
-
R. David ,
H. Alla
.
(1992)
Petri nets and Grafcet: Tools for modelling discrete event systems.
http://iet.metastore.ingenta.com/content/journals/10.1049/ip-cta_19960266
Related content
content/journals/10.1049/ip-cta_19960266
pub_keyword,iet_inspecKeyword,pub_concept
6
6