
This Article  
 
Share  
Bibliographic References  
Add to:  
Digg Furl Spurl Blink Simpy Del.icio.us Y!MyWeb  
Search  
 
ASCII Text  x  
G.S. Avrunin, J.C. Corbett, L.K. Dillon, J.C. Wileden, "Automated Derivation of Time Bounds in Uniprocessor Concurrent Systems," IEEE Transactions on Software Engineering, vol. 20, no. 9, pp. 708719, September, 1994.  
BibTex  x  
@article{ 10.1109/32.317429, author = {G.S. Avrunin and J.C. Corbett and L.K. Dillon and J.C. Wileden}, title = {Automated Derivation of Time Bounds in Uniprocessor Concurrent Systems}, journal ={IEEE Transactions on Software Engineering}, volume = {20}, number = {9}, issn = {00985589}, year = {1994}, pages = {708719}, doi = {http://doi.ieeecomputersociety.org/10.1109/32.317429}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }  
RefWorks Procite/RefMan/Endnote  x  
TY  JOUR JO  IEEE Transactions on Software Engineering TI  Automated Derivation of Time Bounds in Uniprocessor Concurrent Systems IS  9 SN  00985589 SP708 EP719 EPD  708719 A1  G.S. Avrunin, A1  J.C. Corbett, A1  L.K. Dillon, A1  J.C. Wileden, PY  1994 KW  integer programming; realtime systems; scheduling; systems analysis; concurrency control; time bound derivation; uniprocessor concurrent systems; complex realtime systems; timing properties; lower bounds; upper bounds; concurrent software system; single processor; arbitrary scheduling; linear inequalities; integer programming methods; constrained expression toolset; very large state spaces; concurrent systems; timing analysis; finite state systems VL  20 JA  IEEE Transactions on Software Engineering ER   
The successful development of complex realtime systems depends on analysis techniques that can accurately assess the timing properties of those systems. This paper describes a technique for deriving upper and lower bounds on the time that can elapse between two given events in an execution of a concurrent software system running on a single processor under arbitrary scheduling. The technique involves generating linear inequalities expressing conditions that must be satisfied by all executions of such a system and using integer programming methods to find appropriate solutions to the inequalities. The technique does not require construction of the state space of the system and its feasibility has been demonstrated by using an extended version of the constrained expression toolset to analyze the timing properties of some concurrent systems with very large state spaces.
[1] M. W. Alford, "SREM at the age of eight; The distributed computing design system,"Computer, vol. 18, pp. 3646, Apr. 1985.
[2] A. I. Ali, J. Kennington, and B. Shetty, "The equal flow problem,"European J. Oper. Res., vol. 36, pp. 107115, 1988.
[3] J. M. Atlee and J. Gannon, "Statebased model checking of eventdriven system requirements,"IEEE Trans. Software Eng., vol. 19, no. 1, pp. 2440, Jan. 1993.
[4] G. S. Avrunin, U. A. Buy, J. C. Corbett, L. K. Dillon, and J. C. Wileden, "Automated analysis of concurrent systems with the constrained expression toolset,"IEEE Trans. Software Eng., vol. 17, no. 11, pp. 12041222, Nov. 1991.
[5] J. C. Corbett, "Automated Formal Analysis Methods for Concurrent and RealTime Software," Ph.D. thesis, Univ. of Massachusetts at Amherst, 1992.
[6] J. C. Corbett and G. S. Avrunin, "A practical method for bounding the time between events in concurrent realtime systems," inProceedings of the 1993 International Symposium on Software Testing and Analysis (ISSTA), T. Ostrand and E. Weyuker, Eds. New York: ACM Press, June, 1993, pp. 110116.
[7] C. Courcoubetis and M. Yannakakis, "Minimum and maximum delay problems in realtime system," inComputer Aided Verification, 3rd International Workshop Proceedings, vol. 575 ofLecture Notes in Computer Science, K. G. Larsen and A. Skou, Eds., (Aalborg, Denmark, July, 1991, pp. 399409). New York: SpringerVerlag.
[8] B. Dasarathy, "Timing constraints of realtime systems: Constructs for expressing them, methods of validating them,"IEEE Trans. Software Eng., vol. 11, no. 1, pp. 8086, 1985.
[9] L. K. Dillon, G. S. Avrunin, and J. C. Wileden, "Constrained expressions toward broad applicability of analysis methods for distributed software systems,"ACM Trans. Program. Languages and Syst., vol. 10, pp. 374402, July 1988.
[10] H. GarciaMolina and D. Barbara, "How to assign votes in a distributed systems,"J. ACM, vol. 32, no. 4, pp. 841860, Oct. 1985.
[11] R. Gerber and I. Lee, "A Layered approach to automating the verification of realtime systems,"IEEE Trans. Software Eng., vol. 18, no. 9, pp. 768784, Sept. 1992.
[12] C. Ghezzi, D. Mandrioli, and A. Morzenti, "TRIO: A logic language for executable specifications of realtime systems,"J. Systems Software, vol. 12, pp. 107123, 1990.
[13] V. H. Haase, "Realtime behavior of programs,"IEEE Trans. Software Eng., vol. 7, no. 5, pp. 494501, 1981.
[14] N. Halbwachs, P. Caspi, P. Raymond, and D. Pilaud, "The synchronous dataflow programming language LUSTRE,"Proc. IEEE, vol. 79, pp. 13051320, Sept. 1991.
[15] D. Helmbold and D. Luckham, "Debugging Ada tasking programs,"IEEE Software, vol. 2, no. 2, pp. 4757, Mar. 1985.
[16] 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.
[17] F. Jahanian and D. Stuart, "A method for verifying properties of modechart specifications," inProc. RealTime Syst. Symp., 1988, pp. 1221.
[18] C. L. Liu and J. W. Layland, "Scheduling algorithms for multiprogramming in a hard realtime environment,"J. ACM, vol. 20, no. 1, pp. 4661, Jan. 1973.
[19] A. J. Mok, "Fundamental Design Problems of Distributed Systems for the Hard Real Time Environment," Ph.D. thesis, Massachusetts Inst. Technology, 1983.
[20] J. S. Ostroff, "Deciding propertics of timed transition models,"IEEE Trans. Parallel Distrib. Syst., vol. 1, no. 2, pp. 170183, 1990.
[21] J. Reif and S. Smolka, "The complexity of reachability in distributed communicating processes,"Acta Informatica, vol. 25, no. 3, pp. 333354, 1988.
[22] L. Sha and J. B. Goodenough, "Realtime scheduling theory and Ada,"IEEE Comput., vol. 23, pp. 5362, Apr. 1990.
[23] L. Sha, R. Rajkumar, and J. P. Lehoczky, "Priority inheritance protocols: An approach to realtime synchronization,"IEEE Trans. Comput., vol. 39, no. 9, pp. 11751185, Sept. 1990.
[24] A. C. Shaw, "Towards a timing semantics for programming languages," in A. M. van Tilborg and G. M. Koob, Eds.,Foundations of RealTime Computing: Formal Specifications and Methods. Boston: Kluwer Academic Publishers, 1991, ch. 9, pp. 217249.
[25] J.A. Stankovic and K. Ramamritham,Hard RealTime Systems, CS Press, Los Alamitos, Calif., 1984.
[26] R. N. Taylor, "Complexity of analyzing the synchronization structure of concurrent programs,"Acta Informatica, vol. 19, pp. 5784, 1983.