This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Compositional Validation of Time-Critical Systems Using Communicating Time Petri Nets
December 1995 (vol. 21 no. 12)
pp. 969-992
An extended Petri Net model which considers modular partitioning along with timing restrictions and environment models is presented. Module constructs permit the specification of a complex system as a set of message passing modules with the timing semantics of Time Petri Nets. The state space of each individual module can be separately enumerated and assessed under the assumption of a partial specification of the intended module operation environment. State spaces of individual modules can be recursively integrated, to permit the assessment of module clusters and of the overall model, and to check the satisfaction of the assumptions made in the separate analysis of elementary component modules. In the intermediate stages between subsequent integration steps, the state spaces of module and module clusters can be projected onto reduced representations concealing local events that are not essential to the purposes of the analysis. The joint use of incremental enumeration and intermediate concealment of local events allows for a flexible management of state explosion, and permits a scalable approach to the validation of complex systems.

[1] T. Agerwala,“Putting Petri nets to work,” IEEE Computer, vol. 12, no. 12, pp. 85-94, Dec. 1979.
[2] R. Alur and D. Dill, "Automata for Modeling Real-Time Systems," Proc. 17th Int'l Colloq. Aut. Lang. Prog., 1990.
[3] R. Alur, C. Courcoubetis, and D. Dill, “Model-Checking for Real-Time Systems,” Proc. Fifth Symp. Logic in Computer Science, June 1990.
[4] R. Alur and T. Henzinger, "Logics and Models of Real-Time: A Survey," Real-Time: Theory in Practice, Lecture Notes in Computer Science 600, pp. 74-106.
[5] M. Ben-Ari,A. Pnueli,, and Z. Manna,“The temporal logic of branching time,” Acta Informatica, vol. 20, pp. 207-226, 1983.
[6] K. Bartlett, R. Scantlebury, and P. Wilkinson, "A Note on Reliable Full-Duplex Transmission over Half-Duplex Links," Comm. ACM, vol. 12, no. 5, pp. 260-261, May 1969.
[7] M. Baldassarri and G. Bruno,“Protob: An object oriented methodology for developing discrete dynamicsystems,” Computer Languages, vol. 16, no. 1, 1991.
[8] B. Berthomieu and M. Menasche,“An enumerative approach for analyzing time Petri nets,” Proc. IFIP Congress, Sept. 1983.
[9] 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.
[10] A. Cerone,“A net-based approach for specifying real-time systems,” PhD thesis, Univ. of Pisa, Italy, TD-16/93, Mar. 1993.
[11] S. Christensen and L. Petrucci, “Modular State Space Analysis of Coloured Petri Nets,” Proc. 16th Int'l Conf. Application and Theory of Petri Nets, June 1995.
[12] E.M. Clarke, E.A. Emerson, and A.P. Sistla, "Automatic verification of finite-state concurrent systems using temporal logic specifications," ACM Trans. Programming Languages and Systems, vol. 8, no. 2, pp. 244-263, 1986.
[13] A.A.S. Danthine,“Protocol representation with finite state models,” IEEE Trans. on Communications, vol. 28, no. 4, Apr. 1984.
[14] R. Dasarathy,“Timing constraints of real-time systems: Constructs forexpressing them, methods for validating them,” IEEE Transactions on Software Engineering, vol. 11, no. 1, Jan. 1985.
[15] D. Dill,“Timing assumptions and verification of finite-state concurrent systems,” Proc. of the Workshop on Computer Aided Verification Methods for FiniteState Systems,Grenoble, France, 1989.
[16] E.A. Emerson,A.K. Mok,A.P. Sistla,, and J. Srinivasan,“Quantitative temporal reasoning,” Proc. of the Workshop on Computer Aided VerificationMethods for Finite State Systems,Grenoble, France, 1989.
[17] D.J. Hatley and I.A. Pirbhai,Strategies for Real-Time System Specification, Dorset House, 1987.
[18] T.A. Henzinger,Z. Manna,, and A. Pnueli,“Timed transition systems,” Tech. Rep. 92-1263, Dept. of Computer Science, Cornell Univ., Ithaca, N.Y., Jan. 1992.
[19] T.A. Henzinger,X. Nicollin,J. Sifakis,, and S. Yovine,“Symbolic model checking for real-time systems,” Proc. Seventh Symp. on Logics in Computer Science (LICS), 1992.
[20] C.A.R. Hoare, Communicating Sequential Processes, Prentice Hall, Englewood Cliffs, N.J., 1985.
[21] P. Huber, K. Jensen, and R.M. Shapiro, “Hierarchies in Coloured Petri Nets,” Advances in Petri Nets 1990, G. Rozenberg, ed., pp. 313–341, 1990.
[22] A. Kay and J.N. Reed, "A Rely and Guarantee Method for Timed CSP: A Specification and Design of a Telephone Exchange," IEEE Trans. Software Engineering, vol. 19, no. 6, pp. 625-639, June 1993.
[23] R.M. Keller,“Formal verification of parallel programs,” Comm. ACM, vol. 19, no. 7, July 1976.
[24] H. Krumm,“Projections of the reachability graph and environment models,” G. Rozenberg, ed., Advances on Petri Nets’92.New York: Springer Verlag, 1993.
[25] S.S. Lam and A.U. Shankar,“Protocol verification via projections,” IEEE Transactions on Software Engineering, vol. 10, no. 4, July 1984.
[26] L. Lamport,“Using time instead of timeout for fault-tolerant distributedsystems,” ACM Trans. on Programming Languages and Systems, vol. 6, no. 2, Apr. 1984.
[27] N. Leveson, “Safety Analysis Using Petri Nets,” IEEE Trans. Software Eng., vol. 13, no. 3, Mar. 1987.
[28] P. Merlin,“A methodology for the design and the implementation of communicationprotocols,” IEEE Trans. on Communications, vol. 24, no. 6, June 1976.
[29] P. Merlin and D.J. Farber,“Recoverability of communication protocols,” IEEE Trans. on Communications, vol. 24, no. 9, Sept. 1976.
[30] T. Murata,“Petri nets: Properties, analysis and applications,” Proc. IEEE, vol. 77, no. 4, Apr. 1989.
[31] 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.
[32] J. Xu and D.L. Parnas, "On Satisfying Timing Constraints in Hard Real-Time Systems," IEEE Trans. Software Eng., Vol. 19, No. 1, Jan. 1993, pp. 70-84.
[33] J.A. Stankovic and K. Ramamritham, “What is Predictability for Real Time Systems,” J. Real Time Systems, vol. 2, Dec. 1990.
[34] N.V. Stenning,“A data transfer protocol,” Computer Networks, vol. 1, Sept. 1976.
[35] I. Suzuki,“Formal analysis of the alternating bit protocol by temporal Petrinets,” IEEE Transactions on Software Engineering, vol. 16, no. 11, Nov. 1990.
[36] E. Vicario,“Validazione di sistemi di tempo reale mediante modelli di Petri estesi(Real time system validation through extended Petri net models),” PhD diss., Dip.Sistemi e Informatica, Univ. of Florence, Italy, Mar. 1994.
[37] S.S. Yau and M.U. Caglayan,“Distributed software system design representation using modified Petrinets,” IEEE Transactions on Software Engineering, vol. 9, no. 6, Nov. 1983.

Index Terms:
Time-critical systems, finite state models, time Petri Nets, model partitioning, incremental state space enumeration, state space projection, compositional validation.
Citation:
Giacomo Bucci, Enrico Vicario, "Compositional Validation of Time-Critical Systems Using Communicating Time Petri Nets," IEEE Transactions on Software Engineering, vol. 21, no. 12, pp. 969-992, Dec. 1995, doi:10.1109/32.489073
Usage of this product signifies your acceptance of the Terms of Use.