This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
An Algorithm for Exact Bounds on the Time Separation of Events in Concurrent Systems
November 1995 (vol. 44 no. 11)
pp. 1306-1317

Abstract—Determining the time separation of events is a fundamental problem in the analysis, synthesis, and optimization of concurrent systems. Applications range from logic optimization of asynchronous digital circuits to evaluation of execution times of programs for real-time systems. We present an efficient algorithm to find exact (tight) bounds on the separation time of events in an arbitrary process graph without conditional behavior. This result is more general than the methods presented in several previously published papers as it handles cyclic graphs and yields the tightest possible bounds on event separations. The algorithm is based on a functional decomposition technique that permits the implicit evaluation of an infinitely unfolded process graph. Examples are presented that demonstrate the utility and efficiency of the solution. The algorithm will form a basis for exploration of timing-constrained synthesis techniques.

[1] C.A.R. Hoare, Communicating Sequential Processes, Prentice Hall, Englewood Cliffs, N.J., 1985.
[2] H. Hulgaard,S.M. Burns,T. Amon,, and G. Borriello,“Practical applications of an efficient time separation of events algorithm,” Proc. Int’l Conf. Computer-Aided Design (ICCAD), pp. 146-151, Nov. 1993.
[3] H. Hulgaard,T. Amon,S. M. Burns,, and G. Borriello,“Timing analysis of timed event graphs with bounded delays using algebraic techniques,” IEEE Conf. Decision and Control, Dec. 1994.
[4] 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.
[5] F. Jahanian and D.A. Stuart,“A method for verifying properties of modechart specifications,” Proc. Ninth IEEE Real-Time Systems Symp., pp. 12-21, Dec. 1988.
[6] A.R. Martello and S.P. Levitan,“Temporal analysis of time bounded digital systems,” Correct Hardware Design and Verification Methods: IFIP WG10.2 Advanced Research Working Conf., CHARME’93, May 1993.
[7] X. Nicollin, J. Sifakis, and S. Yovine, “Compiling Real-Time Specifications into Extended Automata,” IEEE Trans. Software Eng., vol. 18, no. 9, pp. 794-804, Sept. 1992.
[8] T.G. Rokicki,“Representing and modeling digital circuits,” PhD thesis, Stanford Univ., 1993.
[9] S.V. Campos and E.M. Clarke,“Real-time symbolic model checking for discrete time models,” AMAST Series in Computing: Theories and Experiences for Real-Time System Development. World Scientific Publishing Co., 1994.
[10] 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.
[11] L.Y. Liu and R.K. Shyamasundar, "Static Analysis of Real-Time Distributed Systems," IEEE Trans. Software Eng., vol. 16, no. 4, Apr. 1990.
[12] R. Alur and D.L. Dill,“The theory of timed automata,” Real-Time: Theory in Practice, J.W. de Bakker, C. Huizing, W.P. de Roever, and G. Rosenberg, eds., Lecture Notes in Computer Science #600, pp. 28-73. Springer-Verlag, 1991.
[13] J.S. Ostroff,“Verification of safety critical systems using TTM/RTTL,” Real-Time: Theory in Practice, J.W. de Bakker, C. Huizing, W.P. de Roever, and G. Rosenberg, eds., Lecture Notes in Computer Science #600, pp. 573-602. Springer-Verlag, 1991.
[14] A. Zwarico and I. Lee,“Proving a network of real-time processes correct,” Proc. IEEE Real-Time Systems Symp., pp. 178-188, 1985.
[15] F. Jahanian and A. K.-L. Mok,“Safety analysis of timing properties in real-time systems,”IEEE Trans. Software Eng., vol. SE-12, pp. 890–904, Sept. 1986.
[16] C.J. Myers and T.H.-Y. Meng,“Synthesis of timed asynchronous circuits,” IEEE Trans. Very Large Scale Integration (VLSI) Systems, vol. 1, no. 2, pp. 106-119, June 1993.
[17] K. McMillan and D. Dill, "Algorithms for Interface Timing Verification," Proc. IEEE Int'l Conf. Computer Design, 1992.
[18] P. Vanbekbergen,G. Goossens,, and H. De Man,“Specification and analysis of timing constraints in signal transition graphs,” European Design Automation Conf., Mar. 1992.
[19] F. Baccelli,G. Cohen,G.J. Olsder,, and J.-P. Quadrat,Synchronization and Linearity, Wiley Series in Probability and Mathematical Statistics. New York: John Wiley&Sons, 1992.
[20] S.M. Burns,“Performance analysis and optimization of asynchronous circuits,” PhD thesis, CS-TR-91-1, California Inst. of Tech., 1991.
[21] T. Amon and G. Borriello,“An approach to symbolic timing verification,” 29th ACM/IEEE Design Automation Conf., June 1992.
[22] G. Borriello,“A new interface specification methodology and its application to transducer synthesis,” PhD thesis, Univ. of California, Berkeley, 1988.
[23] A.R. Martello,S. P. Levitan,, and D.M. Chiarulli,“Timing verification using HDTV,” 27th ACM/IEEE Design Automation Conf., pp. 118-123, 1990.
[24] H. Hulgaard and S.M. Burns,“Bounded delay timing analysis of a class of CSP programs with choice,” Int’l Symp. Advanced Research in Asynchronous Circuits and Systems, Nov. 1994.
[25] A.A. Desrochers,“Performance analysis using Petri nets,” J. Intelligent and Robotic Systems, vol. 6, pp. 65-79, 1992.
[26] J.-Y. Lin and D. Ionescu,“Asymptotic behavior of output feedback for a class of nondeterministic discrete event systems,” Int’l J. Control, vol. 54, no. 4, pp. 903-920, 1991.
[27] G.J. Olsder,J.A.C. Resing,R.E. De Vries,M.S. Keane,, and G. Hooghiemstra,“Discrete event systems with stochastic processing times,” IEEE Trans. Automatic Control, vol. 35, no. 3, pp. 299-302, Mar. 1990.
[28] J.A.C. Resing,R.E. de Vries,G. Hooghiemstra,M.S. Keane,, and G.J. Olsder,“Asymptotic behavior of random discrete event systems,” Stochastic Processes and their Applications, vol. 36, pp. 195-216, 1990.
[29] E.D. Lazowska, J. Zahorjan, G.S. Graham, and K.C. Sevcik, Quantitative System Performance, Prentice Hall, pp 64-66, 1984.
[30] H. Hulgaard,S.M. Burns,T. Amon,, and G. Borriello,“An algorithm for exact bounds on the time separation of events in concurrent systems,” Technical Report TR #94-02-02, Univ. of Washington, Dept. of Computer Science and Eng., Feb. 1994, (available via anonymous ftp: cs.washington.edu:tr/1994/02/UW-CSE-94-02-02.PS.Z).
[31] T. Amon, H. Hulgaard, S.M. Burns, and G. Borriello, "An Algorithm for Exact Bounds on the Time Separation of Events in Concurrent Systems," Proc. IEEE Int'l Conf. Computer Design, 1993.
[32] R.A. Cuninghame-Green,Minimax Algebra, no. 166in Lecture Notes in Economics and Mathematical Systems. Springer-Verlag, 1979.
[33] I.N. Herstein,Topics in Algebra. Blaisdell Publishing Company, 1964.
[34] E.L. Lawler,Combinatorial Optimization: Networks and Matroids.New York: Holt, Rinehart, and Winston, 1976.
[35] A.V. Aho,J.E. Hopcroft, and J.D. Ullman,The Design and Analysis of Computer Algorithms.Reading, Mass.: Addison-Wesley, 1974.
[36] M.R. Greenstreet,“STARI: A technique for high-bandwidth communication,” PhD thesis, Princeton Univ., Jan. 1993.

Index Terms:
Abstract algebra, asynchronous systems, concurrent systems, discrete event systems, time separation of events, timing verification.
Citation:
Steven M. Burns, Henrik Hulgaard, Tod Amon, Gaetano Borriello, "An Algorithm for Exact Bounds on the Time Separation of Events in Concurrent Systems," IEEE Transactions on Computers, vol. 44, no. 11, pp. 1306-1317, Nov. 1995, doi:10.1109/12.475126
Usage of this product signifies your acceptance of the Terms of Use.