
This Article  
 
Share  
Bibliographic References  
Add to:  
Digg Furl Spurl Blink Simpy Del.icio.us Y!MyWeb  
Search  
 
ASCII Text  x  
J.S. Ostroff, "Deciding Properties of Timed Transition Models," IEEE Transactions on Parallel and Distributed Systems, vol. 1, no. 2, pp. 170183, April, 1990.  
BibTex  x  
@article{ 10.1109/71.80145, author = {J.S. Ostroff}, title = {Deciding Properties of Timed Transition Models}, journal ={IEEE Transactions on Parallel and Distributed Systems}, volume = {1}, number = {2}, issn = {10459219}, year = {1990}, pages = {170183}, doi = {http://doi.ieeecomputersociety.org/10.1109/71.80145}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }  
RefWorks Procite/RefMan/Endnote  x  
TY  JOUR JO  IEEE Transactions on Parallel and Distributed Systems TI  Deciding Properties of Timed Transition Models IS  2 SN  10459219 SP170 EP183 EPD  170183 A1  J.S. Ostroff, PY  1990 KW  Index Termspetri nets; parallel program design; timed transition models; finitestate TTM; decision procedures; realtime temporal logic; system reachability graph; invariance; precedence; eventuality; realtime response specifications; decidability; formal logic; formal specification; parallel programming; programming theory; realtime systems VL  1 JA  IEEE Transactions on Parallel and Distributed Systems ER   
Realtime distributed systems are modeled by a times transition model (TTM). For any finitestate TTM, decision procedures are provided for checking a small but important class of properties (specified in realtime temporal logic). The procedures are linear in the size of the system reachability graph. The class of properties includes invariance, precedence, eventuality and realtime response specifications.
[1] K. M. Chandy and J. Misra,Parallel Program Design: A Foundation. Reading, MA: AddisonWesley, 1988.
[2] E. M. Clarke, E. A. Emerson, and A. P. Sistla, "Automatic verification of finitestate concurrent systems using temporal logic,"ACM Trans. Program. Lang. Syst., vol. 8, no. 2, pp. 244263, 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. 8496.
[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. 151178, Jan. 1986.
[5] F. Jahanian and A. K. Mok, "Safety analysis of timing properties in realtime systems,"IEEE Trans. Software Eng., vol. SE12, no. 9, pp. 890904, Sept. 1986.
[6] F. Jahanian and A. K. Mok, "A graphtheoretic approach for timing analysis and its implementation,"IEEE Trans. Comput., vol. 36, pp. 961975, Aug. 1987.
[7] F. Jahanian and D. Stuart, "A method for verifying properties of modechart specification," inProc. 9th RealTime Syst. Symp., IEEE Comput. Soc, Huntsville, AL, Dec. 1988, pp. 1221.
[8] N.G. Leveson and J.L. Stolzy, "Safety analysis using Petri nets,"IEEE Trans. Software Eng., vol. SE13, no. 3, pp. 386397, 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. 141154.
[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. 163225, 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. 6893, Jan. 1984.
[14] Z. Manna and A. Pnueli, "Proving precedence properties: the temporal way," Tech. Rep. STANCS83964, Dep. Comput. Sci., Stanford Univ., Stanford, CA, Apr. 1983.
[15] K. Mehlhorn,Graph Algorithms and NPCompleteness. New York: SpringerVerlag, 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. 162169.
[17] P. Merlin and D.J. Faber, "Recoverability of communication protocols,"IEEE Trans. Commun, vol. COM24, no. 9, Sept. 1976.
[18] R. BaezaYates, "The expected behavior of B+trees,"Acta Inform., vol. 26, pp. 439471, 1989.
[19] J. Ostroff,Temporal Logic of RealTime Systems. Research Studies Press, 1990.
[20] A. Krasniewski and S. Pilarski, "Circular SelfTest Path: A LowCost BIST Technique,"Proc. Design Automation Conf., July 1987, pp. 407415.
[21] J. S. Ostroff and W. M. Wonham, "Modeling, specifying, and verifying realtime embedded computer systems," inProc. 8th IEEE RealTime Syst. Symp., San Jose, CA, Dec. 1987, pp. 124132.
[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. 681686.
[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, SpringerVerlag, N.Y., 1986, pp. 510584.
[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 68, 1980, pp. 8896.