This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Deciding Properties of Timed Transition Models
April 1990 (vol. 1 no. 2)
pp. 170-183

Real-time distributed systems are modeled by a times transition model (TTM). For any finite-state TTM, decision procedures are provided for checking a small but important class of properties (specified in real-time temporal logic). The procedures are linear in the size of the system reachability graph. The class of properties includes invariance, precedence, eventuality and real-time response specifications.

[1] K. M. Chandy and J. Misra,Parallel Program Design: A Foundation. Reading, MA: Addison-Wesley, 1988.
[2] E. M. Clarke, E. A. Emerson, and A. P. Sistla, "Automatic verification of finite-state concurrent systems using temporal logic,"ACM Trans. Program. Lang. Syst., vol. 8, no. 2, pp. 244-263, Apr. 1986.
[3] E. A. Emerson and C. Lei, "Modalities for model checking: Branching time strikes back," inConf. Record 12th ACM Symp. Principles Programm. Lang., New Orleans, LA, Jan. 1985, pp. 84-96.
[4] E. A. Emerson and J. Y. Halpern, "'Sometimes' and 'not never' revisited: On branching versus linear time temporal logic,"J. ACM, vol. 33, no. 1, pp. 151-178, Jan. 1986.
[5] F. Jahanian and A. K. Mok, "Safety analysis of timing properties in real-time systems,"IEEE Trans. Software Eng., vol. SE-12, no. 9, pp. 890-904, Sept. 1986.
[6] F. Jahanian and A. K. Mok, "A graph-theoretic approach for timing analysis and its implementation,"IEEE Trans. Comput., vol. 36, pp. 961-975, Aug. 1987.
[7] F. Jahanian and D. Stuart, "A method for verifying properties of modechart specification," inProc. 9th Real-Time Syst. Symp., IEEE Comput. Soc, Huntsville, AL, Dec. 1988, pp. 12-21.
[8] N.G. Leveson and J.L. Stolzy, "Safety analysis using Petri nets,"IEEE Trans. Software Eng., vol. SE-13, no. 3, pp. 386-397, Mar. 1987.
[9] O. Lichtenstein and A. Pnueli, "Checking that finite state concurrent programs satisfy their linear specification," Tech. Rep., Dep. Appl. Math., Weizmann Institute of Science, Tel Aviv, Israel, Dec. 1984.
[10] Z. Manna and A. Pnueli, "How to cook a temporal proof system for your pet language," inProc. Symp. Principles Programm. Languag., Austin, TX, Jan. 1983, pp. 141-154.
[11] Z. Manna and A. Pnueli, "The anchored version of the temporal framework," inModels of Concurrency: Linear, Branching, and Partial Orders, J. W. de Bakker, W. P. de Roever, and G. Rozenburg, Eds. Berlin: Springer, 1986.
[12] Z. Manna and A. Pnueli, "Verification of concurrent programs: A temporal proof system, " Tech. Rep. Dep. Comput. Sci., Stanford Univ., June 1983; see also Foundations of Computer Science IV, Amsterdam, Mathematical Center Tracts, pp. 163-225, 1983.
[13] Z. Manna and P. Wolper, "Synthesis of communicating processes from temporal logic specifications,"ACM Trans. Programm. Languag. Syst., vol. 6, no. 1, pp. 68-93, Jan. 1984.
[14] Z. Manna and A. Pnueli, "Proving precedence properties: the temporal way," Tech. Rep. STAN-CS-83-964, Dep. Comput. Sci., Stanford Univ., Stanford, CA, Apr. 1983.
[15] K. Mehlhorn,Graph Algorithms and NP-Completeness. New York: Springer-Verlag, 1984.
[16] M. Menasche, "PAREDE: An automated tool for the analysis of time(d) Petri nets," inInternational Workshop on Timed Petri Nets. IEEE Comput. Soc., June 1985, pp. 162-169.
[17] P. Merlin and D.J. Faber, "Recoverability of communication protocols,"IEEE Trans. Commun, vol. COM-24, no. 9, Sept. 1976.
[18] R. Baeza-Yates, "The expected behavior of B+-trees,"Acta Inform., vol. 26, pp. 439-471, 1989.
[19] J. Ostroff,Temporal Logic of Real-Time Systems. Research Studies Press, 1990.
[20] A. Krasniewski and S. Pilarski, "Circular Self-Test Path: A Low-Cost BIST Technique,"Proc. Design Automation Conf., July 1987, pp. 407-415.
[21] J. S. Ostroff and W. M. Wonham, "Modeling, specifying, and verifying real-time embedded computer systems," inProc. 8th IEEE Real-Time Syst. Symp., San Jose, CA, Dec. 1987, pp. 124-132.
[22] J. S. Ostroff and W. M. Wonham, "State machines, temporal logic and control: A framework for discrete event systems," inProc. 26th IEEE Conf. Decision Control, Los Angeles, CA, pp. 681-686.
[23] A. Pnueli, "Applications of Temporal Logic to the Specification and Verification of Reactive Systems: A Survey of CurrentTrends," inCurrent Trends in Concurrency: Overviews and Tutorials. W.-P. de Roever and G. Rozenberg, eds., Lecture Notes in Computer Science 224, Springer-Verlag, N.Y., 1986, pp. 510-584.
[24] C. Ramchandani, "Analysis of asynchronous concurrent systems by timed Petri nets," Massachusetts Inst. Technol., Project MAC, Tech. Rep. 120, Feb. 1974.
[25] R. R. Razouk and C. V. Phelps, "Performance analysis of timed Petri nets," inProc. 4th Int. Workshop Protocol Verification and Testing, June 1984.
[26] W. M. Zuberek, "Timed Petri nets and preliminary performance evaluation," inProc. 7th Annu. Symp. Computer Architecture, May 6-8, 1980, pp. 88-96.

Index Terms:
Index Termspetri nets; parallel program design; timed transition models; finite-state TTM; decision procedures; real-time temporal logic; system reachability graph; invariance; precedence; eventuality; real-time response specifications; decidability; formal logic; formal specification; parallel programming; programming theory; real-time systems
Citation:
J.S. Ostroff, "Deciding Properties of Timed Transition Models," IEEE Transactions on Parallel and Distributed Systems, vol. 1, no. 2, pp. 170-183, April 1990, doi:10.1109/71.80145
Usage of this product signifies your acceptance of the Terms of Use.