This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Reduction Methods for Real-Time Systems Using Delay Time Petri Nets
May 2001 (vol. 27 no. 5)
pp. 422-448

Abstract—This paper presents a new net-reduction methodology to facilitate the analysis of real-time systems using Delay Time Petri Nets (DTPNs). Net reduction is one of the most important techniques for reducing the state-explosion problem of Petri nets. However, the application of net reduction to current timed-extensions of Petri nets (such as Merlin's Time PNs) is very limited due to the difficulty faced in the preservation of timing constraints. To overcome this problem, this paper introduces DTPNs which are inspired by Merlin's Time PNs, Sénac's Hierarchical Time Stream PNs, and Little's Timed PNs. We show that DTPNs are much more suitable for net reduction. Then, this paper presents a new set of DTPN reduction rules for the analysis of schedule and deadlock analysis. Our work is distinct from the others since our goal is to analyze real-time systems and the reduction methods we propose preserve both timing properties (schedule) and deadlock. To evaluate our framework, we have implemented an automated analysis tool whose main functions include net reduction and class-graph generation. The experimental results show that our net-reduction methodology leads to a significant contribution to the efficient analysis of real-time systems.

[1] R. Alur and D. Dill, “A Theory of Timed Automata,” Theoretical Computer Science, vol. 126, pp. 183-235, 1994.
[2] G. Berthelot, "Checking Properties of Nets Using Transformations," Advances in Petri Nets, vol. 222, Lecture Notes in Computer Science, pp. 19-40. Springer-Verlag, 1987.
[3] B. Berthomieu and M. Diaz, “Modeling and Verification of Time Dependent Systems Using Time Petri Nets,” IEEE Trans. Software Eng., vol. 17, no. 3, Mar. 1991.
[4] G. Bucci and E. Vicario, “Compositional Validation of Time-Critical Systems Using Communicating Time Petri Nets,” IEEE Trans. Software Eng., vol. 21, no. 12, pp. 969–992, Dec. 1995.
[5] M. D'Anna and S. Trigila, ”Concurrent System Analysis Using Petri Nets: An Optimized Algorithm for Finding Net Invariants,” Computer Comm., vol. 11, no. 4, pp. 215-220, Aug. 1988.
[6] P. Godefroid and P. Wolper, "Using Partial Orders for the Efficient Verification of Deadlock Freedom and Safety Properties," Formal Methods in System Design, pp. 149-164, Apr. 1993.
[7] S. Haddad, “A Reduction Theory for Coloured Petri Nets,” Proc. Advances in Petri Nets, pp. 209-235, 1990.
[8] R. Johnsonbaugh and T. Murata, “Additional Methods for Reduction and Expansion of Marked Graphs,” IEEE Trans. Circuits and Systems, vol. 28, no. 10, pp. 1009-1024, Oct. 1981.
[9] E. Juan, J.J.P. Tsai, and T. Murata, "Compositional Verification of Concurrent Systems Using Petri-Net-Based Condensation Rules," ACM Trans. Programming Languages and Systems, vol. 20, no. 5, Sept. 1998.
[10] E. Juan and J.J.P. Tsai, Compositional Verification of High-Assurance Systems. Boston: Kluwer Academic, 2000.
[11] A.A. Khan, G.S. Hura, H. Singh, and N.K. Nanda, ”On the Determination of the Solution of a Class of Murata's State Equation of Petri Nets,” Proc. IEEE, vol. 69, no. 4, pp. 466-467, Apr. 1981.
[12] H. Lee-Kwang and J. Favrel, “Hierarchical Reduction Methods for Analysis and Decomposition of Petri Nets,” IEEE Trans. Systems, Man, and Cybernetics, vol. 15, pp. 272-280, Mar. 1985.
[13] H. Lee-Kwang, J. Favrel, and P. Baptiste, “Generalized Petri Net Reduction Method,” IEEE Trans. Systems, Man, and Cybernetics, vol. 17, no. 2, pp. 297-303, Apr. 1987.
[14] N. Leveson, “Safety Analysis Using Petri Nets,” IEEE Trans. Software Eng., vol. 13, no. 3, Mar. 1987.
[15] T.D.C. Little and A. Ghafoor, “Spatio-Temporal Composition of Distributed Multimedia Objects for Value Added Networks,” Computer, vol. 24, no. 10, pp. 42-50, Oct. 1991.
[16] P. Merlin and D. Faber, “Recoverability of Communication Protocols—Implications of a Theoretical Study,” IEEE Trans. Comm., vol. 24, no. 9, pp. 381-404, Sept. 1976.
[17] M. Merritt, F. Modugno, and M.R. Tuttle, ”Time-Constrained Automata,” Lecture Notes in Computer Science, vol. 527, pp. 408-423, 1991.
[18] T. Murata and J.Y. Koh, “Reduction and Expansion of Live and Safe Marked Graphs,” IEEE Trans. Circuits and Systems, vol. 27, no. 1, pp. 68-70, Jan. 1980.
[19] T. Murata, “Petri Nets: Properties, Analysis and Application,” Proc. IEEE, vol. 77, no. 4, 1989.
[20] M. Notomi and T. Murata, "Hierarchical Reachability Graph of Bounded Petri Nets for Concurrent-Software Analysis," IEEE Trans. Software Eng., vol. 20, no. 5, May 1994.
[21] L. Pomello, ”Some Equivalence Notions for Concurrent Systems,” Advances in Petri Nets 1985, G. Rozenberg, ed., pp. 381-400, 1986.
[22] C. Ramchandani,“Analysis of asynchronous concurrent systems by Petri nets.”Cambridge, MA: MIT, Project MAC, TR-120, Feb. 1974.
[23] C.V. Ramamoorthy and G.S. Ho, ”Performance Evaluation of Asynchronous Concurrent Systems Using Petri Nets,” IEEE Trans. Software Eng., vol. 6, pp. 440-449, Sept. 1980.
[24] J.L. Roux, “Modélisation et Analyse des Systèmes Distribués Parles Réseaux de Petri Temporels,” thèse de Docteur-Ingénieur INSA, Dec. 1985.
[25] P. Sénac, M. Diaz, A. Léger, and P.D. Saqui-Sannes, “Toward a Formal Specification of Multimedia Synchronization,” Annals of Telecomm., May/June 1994.
[26] P. Sénac, M. Diaz, A. Léger, and P.D. Saqui-Sannes, “Modeling Logical and Temporal Synchronization in Hypermedia Systems,” IEEE J. Selected Areas in Comm., vol. 14, no. 1, pp. 84-103, Jan. 1996.
[27] S.M. Shatz, S. Tu, T. Murata, and S. Duri, "An Application of Petri Net Reduction for Ada Tasking Deadlock Analysis," IEEE Trans. Parallel and Distributed Systems, pp. 1,307-1,322, vol. 7, no. 12, Dec. 1996.
[28] R.H. Sloan and U. Buy, “Reduction Rules for Time Petri Nets,” Acta Informatica, vol. 33, pp. 687-706, Oct. 1996.
[29] Monitoring and Debugging Distributed Real-Time Systems, J.J.P. Tsai and S. Yang eds. Washington, D.C.: IEEE Computer Society Press, Nov. 1994.
[30] J.J.P. Tsai, S.J.H. Yang, and Y.H. Chang, ”Timing Constraint Petri Nets and their Application to Schedulability Analysis of Real-Time System Specification,” IEEE Trans. Software Eng., vol. 21, no. 1, pp. 32-49, Jan. 1995.
[31] J.J.P. Tsai, Y. Bi, S.J.H. Yang, and R.A.W. Smith, Distributed Real-Time Systems: Monitoring, Debugging, and Visualization. John Wiley and Sons, 1996.
[32] J.J.P. Tsai and X. Kuang, ”An Empirical Evaluation of Deadlock Detection in Software Architecture Specifications,” Annals of Software Eng., vol. 7, pp. 95-126, 1999.
[33] R. Valette, ”Analysis of Petri Nets by Stepwise Refinements,” J. Computer and System Sciences, vol. 18, pp. 35-46, 1979.
[34] M. Zhou, K. McDermott, and P.A. Patel, "Petri Net Synthesis and Analysis of a Flexible Manufacturing System Cell," IEEE Trans. Systems, Man, and Cybernetics, pp. 523-531, vol. 23, no. 2, Mar. 1993.

Index Terms:
Real-time systems, state explosion, Petri nets, net reduction, schedule, deadlock, reachability.
Citation:
Eric Y.T. Juan, Jeffrey J.P. Tsai, Tadao Murata, Yi Zhou, "Reduction Methods for Real-Time Systems Using Delay Time Petri Nets," IEEE Transactions on Software Engineering, vol. 27, no. 5, pp. 422-448, May 2001, doi:10.1109/32.922714
Usage of this product signifies your acceptance of the Terms of Use.