Time extensions of Petri nets for modelling and verification of hard real-time systems

• Autorzy: Samolej S. , Szmuc T.

Warianty tytułu

PL

Rozszerzenia czasowe sieci Petriego do modelowania i weryfikacji systemów czasu rzeczywistego o twardych wymaganiach czasowych

• Języki publikacji: EN

Abstrakty

EN

The main aim of the paper is a presentation of time extensions of Petri nets appropriate for modelling and analysis of hard real-time systems. It is assumed, that the extensions must provide a model of time flow, an ability to force a transition to fire within a stated timing constraint (the so-called the strong firing rule), and timing constraints represented by intervaIs. The presented survey includes extensions of classical Place/Transition Petri nets, as welI as the ones applied to high-level Petri nets. An expressiveness of each time extension is illustrated using simple hard real-time system. The paper includes also a brief description of analysis and verification methods related to the extensions, and a survey of software tooIs supporting modelling and analysis of the considered Petri nets.

PL

Głównym celem pracy jest prezentacja rozszerzeń czasowych sieci Petriego pod kątem przydatności do modelowania i analizy systemów czasu rzeczywistego o twardych wymaganiach losowych. Zakłada się, że rozważane rozszerzenia winny spełniać następujące warunki: modelowania upływu czasu, forsowania odpalenia przejścia w określonych warunkach czasowych (tzw. silna reguła odpalania), przedziałowej reprezentacji ograniczeń czasowych. Przegląd dotyczy zarówno klasycznych sieci miejsc i przejść, jak również sieci Petriego wyższego poziomu. Siła ekspresji poszczególnych rozszerzeń jest ilustrowana na wspólnym przykładzie systemu o twardych wymaganiach czasowych. Artykuł zawiera również krótki opis metod analizy i weryfikacji ograniczeń czasowych oraz przegląd systemów wspomagających modelowanie i analizę rozważanych sieci Petriego.

Słowa kluczowe

EN

hard real-time systems; timed Petri nets; high-level Petri nets

PL

systemy czasu rzeczywistego; twarde wymagania czasowe; czasowe sieci Petriego wyższego poziomu

• Wydawca: Wydawnictwa AGH
• Czasopismo: Computer Science
• Rocznik: 2002
• Tom: Vol. 4
• Strony: 55--76
• Opis fizyczny: Bibliogr. 34 poz., rys., tab.

Twórcy

autor

Samolej S.

• Computer and Control Engineering Chair, Rzeszów University of Technology, Rzeszów

autor

Szmuc T.

• Institute of Automatics, University of Mining and Metallurgy, Cracow

Bibliografia

• [1] van der Aalst W.M.P.: Interval Timed Coloured Petri Nets and their Analysis. Application and Theory of Petri Nets 1993, Proc. of the 14th International Petri Net Conference, Chicago 1993, Lecture Notes in Computer Science, vol. 691, Springer-Verlag 1993, 452-427
• [2] Berhtomieu B., Diaz M.: Modeling and Verification of Time Dependent Systems Using Time Petri Nets. IEEE Transactions on Software Engineering, vol. 17, No. 3, March 1991, 259-273
• [3] Bowden F.D.J.: Modelling Time in Petri Nets. Proc. of the Second Australia-Japan Workshop on Stochastic Models in Engineering, Technology and Management, Gold Coast, Australia, July 1996
• [4] Bowden F.D.J.: A Brief Survey and Synthesis of the Roles of Time in Petri Nets. Mathematical and Computer Modelling, 1999
• [5] Burkhard H.D.: Ordered Firing in Petri Nets. Journal of Information Proc. and Cybernetics EIK, 17, 1981, 71-86
• [6] Cerone A.: A Net-Based Approach for Specifying Real-Time Systems. Dipartamento di Informatica, Universita di Pisa 1993 (Ph.D., Thesis, TD-16/93)
• [7] Cerone A., Maggiolo-Shettini A.: Time-Based Expressivity of Time Petri Nets for System Specification. Theoretical Computer Science, vol. 216, 1999, 1-53
• [8] Coolahan J.E. Jr., Roussopoulos N.: Timing Requirements for Time-Driven Systems Using Augmented Petri Nets. IEEE Transactions on Software Engineering, vol. SE-9, No. 5, September 1983, 603-616
• [9] Felder M., Ghezzi C., Pezze M.: Formal Specyfication and Timing Analysis of High-Integrity Real-Time Systems. Real Time Computing, NATO ASI Series, vol. 127, 1992, 187-211
• [10] de Frutos-Escrig D., Ruiz V.V., Alonso O.M.: Decidability of Properties of Timed-Arc Petri Nets. Application and Theory of Petri Nets 2000,21 st International Conference, IC ATPN 2000, Aarhus, Denmark, June 26-30, 2000, 187-206
• [11] Ghezzi C., Mandrioli D., Morasca S., Pezze M.: A Unified High-Level Petri Net Formalism for Time-Critical Systems. IEEE Transactions on Software Engineering, vol. 17, No. 2, February 1991, 160-172
• [12] Hanisch H.M.: Analysis of Place/Transition Nets with Timed Arcs and its Application to Batch process Control. Application and Theory of Petri Nets 1993, Proc. of the 14th International Petri Net Conference, Chicago 1993, Lecture Notes in Computer Science, vol. 691, Springer- -Verlag 1993, 282-299
• [13] Hanisch H.M., Thieme J., Lautenbach K., Simon C.: Timestamp nets in technical applications. Proc. IEEE Int. Conf. on Systems, Man, and Cybernetics (SMC’98), San Diego, CA, 11-14 October 1998, 119-124
• [14] Halang W.A., Sacha K.M.: Real-Time Systems. London, World Scientific Publishing Co. 1992
• [15] Holliday M.A., Vernon M.K.: A Generalized Timed Petri Net Model for Performance Analysis. IEEE Transactions on Software Engineering, vol. SE-13, No. 12, December 1987, 1297-1310
• [16] Jensen K.: Coloured Petri Nets. Basic Concepts, Analysis Methods and Practical Use. vol. 1-3. Berlin, Springer-Verlag 1995/96
• [17] Leveson N.G., Stolzy J.L.: Safety Analysis Using Petri Nets. IEEE Transactions on Software Engineering, vol. SE-13, No. 3, March 1987, 386-397
• [18] Merlin P.M., Farber D.J.: Recoverability of Communication Protocols - Implications of a Theoretical Study. IEEE Transactions on Communications, September 1976, 1036-1043
• [19] Meta Software Corporation: Design/CPN Tutorial for X-Windows. Meta Software 1993
• [20] Meta Software Corporation: Design/CPN Reference Manual for X-Windows. Meta Software 1993
• [21] Murata T: Petri Nets: Properties, Analysis and Applications. Proc. of the IEEE, vol. 77, No. 4, 1989, 541-580
• [22] Peterson J.L.: Petri Net Theory and The Modelling of Systems. Englewood Cliffs, Prentice- -Hall, 1981
• [23] Ramamoorthy C.V., Ho G.S.: Performance Evaluation of Asynchronous Concurrent Systems Using Petri Nets. IEEE Transactions on Software Engineering, vol. SE-6, No. 5, September 1980, 440-449
• [24] Ramchandani C.: Analisys of Asynchronous Concurrent Systems by Petri Nets. Project MAC, MAC-TR 120, MIT 1974 (Ph.D. Thesis)
• [25] Roch S., Starke H.P.: IN A Integrated Net Analyzer, Version 2.2, Manual. Berlin, Humboldt- -Universitat zu Berlin, Institut fur Informatik, Lehrstuhl fur Automaten und Systemtheorie 1999
• [26] Sacha K.: Projektowanie oprogramowania systemów wbudowanych. Warszawa, Politechnika Warszawska 1996 Prace Naukowe Elektronika, z. 115,
• [27] Sifakis J.: Performance Evaluation of Systems Using Nets. Net Theory and Applications, Proc. of the Advanced Course on General Net Theory of Processes and Systems, Hamburg, October 1979, Lecture Notes in Computer Science, vol. 84, Springer 1980, 307-319
• [28] Starke P.H.: Some Properties of Timed Nets under the Earliest Firing Rule. Lecture Notes in Computer Science, vol. 424, Advances in Petri Nets 1989, Germany, Springer-Verlag 1990, 418-432
• [29] Starke P.H.: A Memo on Time Constraints in Petri Nets. Informatik-Bericht, Nr 46
• [30] Storrle H.: An Ealuation of High-End Tools for Petri-Nets. Ludwig-Maximilians-Universitat Miinchen, Institut fur Informatik, June 1998
• [31] Szmuc T: Zaawansowane metody tworzenia oprogramowania systemów czasu rzeczywistego. Kraków, Cracow Centre for Advanced Training in Information Engineering, vol. 15, 1998
• [32] Walter B.: Timed Petri Nets for Modelling and Analysis Protocols with Real-Time Characteristics. Proc. 3rd IFIP Workshop on Protocol Specification, Testing, and Verification, North- -Holland, Amsterdam 1983, 149-159
• [33] http://www.daimi.au.dk/PetriNets/classification/tools/cabemet.html
• [34] http://www.daimi.au.dk/PetriNets/classification/tools/merlot.html