Real-time synchronisation of multiaxis high-speed machines, from SFC specification to Petri net verification

Access Full Text

Real-time synchronisation of multiaxis high-speed machines, from SFC specification to Petri net verification

For access to this article, please select a purchase option:

Buy article PDF
£12.50
(plus tax if applicable)
Add to cart
Buy Knowledge Pack
10 articles for £75.00
(plus taxes if applicable)
Add to cart

IET members benefit from discounts to all IET publications and free access to E&T Magazine. If you are an IET member, log in to your account and the discounts will automatically be applied.

Learn more about IET membership 

Recommend Title Publication to library

You must fill out fields marked with: *

Librarian details
Name:*
Email:*
Your details
Name:*
Email:*
Department:*
Why are you recommending this title?
Select reason:
 
 
 
 
 
IEE Proceedings - Control Theory and Applications — Recommend this title to your library

Thank you

Your recommendation has been sent to your librarian.

© IEE
Published

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.

Inspec keywords: synchronisation; real-time systems; machine tools; formal verification; packaging; Petri nets; discrete event systems; standards; formal logic

Other keywords: formal verification; synchronisation logic; specification; multiaxis high-speed machines; industry standard IEC 1131; packaging machine; Petri net model; discrete event systems; hybrid control; real-time systems; sequential function charts

Subjects: Control applications to materials handling; Discrete control systems; Production management; Materials handling and distribution; Systems theory applications in industry; Combinatorial mathematics; Combinatorial mathematics; Systems theory applications; Formal logic; Packaging

References

    1. 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. 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. 3)
      • C.A.R. Hoare . (1985) Communicating sequential processes.
    4. 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. 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. 6)
      • T. Murata . Petri nets: Properties, analysis and applications. Proc. IEEE , 4 , 541 - 580
    7. 7)
      • IEC 1131, International Electrotechnical Commission:‘Internationalstandardfor programmable controllers, programming languages’, March 1993.
    8. 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. 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. 10)
      • P.M. Merlin , D.J. Farber . Recoverability of communication protocols, implications of a theoreticalstudy. IEEE Trans. , 1036 - 1043
    11. 11)
      • N.G. Levenson , J.L. Stolzy . Safety analysis using Petri nets. IEEE Trans. Softw. Eng. , 3 , 386 - 397
    12. 12)
      • A.A. Desrochers , R.Y. Al-Jaar . (1995) Applications of Petri nets in manufacturing systems.
    13. 13)
      • R. Zurawski , M.C. Zhou . Petri nets and industrial applications: A tutorial. IEEE Trans. Indust.Electron. , 6 , 567 - 585
    14. 14)
      • J.L. Peterson . (1981) Petri net theory and the modelling of systems.
    15. 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. 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. 17)
      • W. Reisig . (1985) Petri nets: an introduction.
    18. 18)
      • H. Langmaack , W.-P. de Roever , S. Vytopil . (1994) Formal techniques in real-time and fault-tolerant systems.
    19. 19)
      • D. Skeen , M. Stonebraker . A formal model of crash recovery in a distributed system. IEEE Trans. Softw. Eng. , 3 , 213 - 228
    20. 20)
      • P.J. Antsaklis , W. Kohn , A. Nerode , S. Sastry . (1998) Hybrid systems.
    21. 21)
      • N.G. Levenson . (1995) Safeware – system safety and computers.
    22. 22)
      • L. Lamport . Proving the correctness of multiprocess programs. IEEE Trans. Softw. Eng. , 2 , 125 - 143
    23. 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
Loading

Related content

content/journals/10.1049/ip-cta_19960266
pub_keyword,iet_inspecKeyword,pub_concept
6
6
Loading