This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Automated Derivation of Time Bounds in Uniprocessor Concurrent Systems
September 1994 (vol. 20 no. 9)
pp. 708-719
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. 708-719, 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 = {0098-5589},
year = {1994},
pages = {708-719},
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 - 0098-5589
SP708
EP719
EPD - 708-719
A1 - G.S. Avrunin,
A1 - J.C. Corbett,
A1 - L.K. Dillon,
A1 - J.C. Wileden,
PY - 1994
KW - integer programming; real-time systems; scheduling; systems analysis; concurrency control; time bound derivation; uniprocessor concurrent systems; complex real-time 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 real-time 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. 36-46, Apr. 1985.
[2] A. I. Ali, J. Kennington, and B. Shetty, "The equal flow problem,"European J. Oper. Res., vol. 36, pp. 107-115, 1988.
[3] J. M. Atlee and J. Gannon, "State-based model checking of event-driven system requirements,"IEEE Trans. Software Eng., vol. 19, no. 1, pp. 24-40, 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. 1204-1222, Nov. 1991.
[5] J. C. Corbett, "Automated Formal Analysis Methods for Concurrent and Real-Time 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 real-time 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. 110-116.
[7] C. Courcoubetis and M. Yannakakis, "Minimum and maximum delay problems in real-time 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. 399-409). New York: Springer-Verlag.
[8] B. Dasarathy, "Timing constraints of real-time systems: Constructs for expressing them, methods of validating them,"IEEE Trans. Software Eng., vol. 11, no. 1, pp. 80-86, 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. 374-402, July 1988.
[10] H. Garcia-Molina and D. Barbara, "How to assign votes in a distributed systems,"J. ACM, vol. 32, no. 4, pp. 841-860, Oct. 1985.
[11] R. Gerber and I. Lee, "A Layered approach to automating the verification of real-time systems,"IEEE Trans. Software Eng., vol. 18, no. 9, pp. 768-784, Sept. 1992.
[12] C. Ghezzi, D. Mandrioli, and A. Morzenti, "TRIO: A logic language for executable specifications of real-time systems,"J. Systems Software, vol. 12, pp. 107-123, 1990.
[13] V. H. Haase, "Real-time behavior of programs,"IEEE Trans. Software Eng., vol. 7, no. 5, pp. 494-501, 1981.
[14] N. Halbwachs, P. Caspi, P. Raymond, and D. Pilaud, "The synchronous dataflow programming language LUSTRE,"Proc. IEEE, vol. 79, pp. 1305-1320, Sept. 1991.
[15] D. Helmbold and D. Luckham, "Debugging Ada tasking programs,"IEEE Software, vol. 2, no. 2, pp. 47-57, Mar. 1985.
[16] 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.
[17] F. Jahanian and D. Stuart, "A method for verifying properties of modechart specifications," inProc. Real-Time Syst. Symp., 1988, pp. 12-21.
[18] C. L. Liu and J. W. Layland, "Scheduling algorithms for multiprogramming in a hard real-time environment,"J. ACM, vol. 20, no. 1, pp. 46-61, 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. 170-183, 1990.
[21] J. Reif and S. Smolka, "The complexity of reachability in distributed communicating processes,"Acta Informatica, vol. 25, no. 3, pp. 333-354, 1988.
[22] L. Sha and J. B. Goodenough, "Real-time scheduling theory and Ada,"IEEE Comput., vol. 23, pp. 53-62, Apr. 1990.
[23] L. Sha, R. Rajkumar, and J. P. Lehoczky, "Priority inheritance protocols: An approach to real-time synchronization,"IEEE Trans. Comput., vol. 39, no. 9, pp. 1175-1185, 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 Real-Time Computing: Formal Specifications and Methods. Boston: Kluwer Academic Publishers, 1991, ch. 9, pp. 217-249.
[25] J.A. Stankovic and K. Ramamritham,Hard Real-Time 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. 57-84, 1983.

Index Terms:
integer programming; real-time systems; scheduling; systems analysis; concurrency control; time bound derivation; uniprocessor concurrent systems; complex real-time 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
Citation:
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. 708-719, Sept. 1994, doi:10.1109/32.317429
Usage of this product signifies your acceptance of the Terms of Use.