This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Static Analysis and Dynamic Steering of Time-Dependent Systems
August 2001 (vol. 27 no. 8)
pp. 728-748

Abstract—An enumerative technique is presented which supports reachability and timeliness analysis of time-dependent models. The technique assumes a dense model of time and uses equivalence classes to enable discrete and compact enumeration of the state space. Properties of timed reachability among states are recovered through the analysis of timing constraints embedded within equivalence classes. In particular, algorithms are given to evaluate a tight profile for the set of feasible timings of any untimed run. Runtime refinement of static profiles supports a mixed static/dynamic strategy in the development of a failure avoidance mechanism for dynamic acceptance and a guarantee of hard real-time processes.

[1] R.K. Ahuja, T.L. Magnanti, and J.B. Orlin, Network Flows. Prentice Hall, 1993.
[2] R. Alur and D.L. Dill, “Automata for Modeling Real-Time Systems,” Proc. 17th Int'l Colloquium on Automata, Languages, and Programming, 1990.
[3] R. Alur, C. Courcoubetis, and D. Dill, “Model-Checking for Real-Time Systems,” Proc. Fifth Symp. Logic in Computer Science, June 1990.
[4] R. Alur, T.A. Henzinger, and P.-H. Ho, “Automatic Symbolic Verification of Embedded Systems,” IEEE Trans. Software Eng., vol. 22, no. 3, Mar. 1996.
[5] G. Beccari, S. Caselli, M. Reggiani, and F. Zanichelli, “A Real-Time Library for the Design of Hybrid Robot Control Architectures,” IEEE/RSJ Int'l Conf. Intelligent Robots and Systems, IROS '98, Oct. 1998.
[6] J. Bengtsson, K.G. Larsen, F. Larsson, P. Pettersson, and W. Yi, “UPPAAL: A Tool-Suite for Automatic Verification of Real-Time Systems,” Hybrid Systems III, R. Alur, T.A. Henzinger, and E.D. Sontag, eds., 1996.
[7] J.A. Stankovic, M. Spuri, M. Di Natale, and G. Buttazzo, “Implications of Classical Scheduling Results for Real-Time Systems,” IEEE Computer, vol. 28, no. 6, June 1995.
[8] 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.
[9] B. Berthomieu and M. Menasche, “An Enumerative Approach for Analyzing Time Petri Nets,” Proc. Int'l Federation for Information Processing Congress, Sept. 1983.
[10] G. Bucci and E. Vicario, “Compositional Validation of Time-Critical Systems Using Communicating Time Petri Nets,” IEEE Trans. Software Eng., vol. 21, no. 12, pp. 969–992, Dec. 1995.
[11] S. Christensen and L. Petrucci, “Modular State Space Analysis of Coloured Petri Nets,” Proc. 16th Int'l Conf. Application and Theory of Petri Nets, June 1995.
[12] 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.
[13] J.C. Corbett, “Timing Analysis of Ada Tasking Programs,” IEEE Trans. Software Eng., vol. 22, no. 7, pp. 461-483, July 1996.
[14] C. Corcoubetis, D. Dill, M. Chatzaki, and P. Tzounakis, “Verification with Real-Time COSPAN,” Proc. Int'l Workshop on Computer Aided Verification, 1992.
[15] C. Corcoubetis and M. Yannakakis, “Minimum and Maximum Delay Problems in Real-Time Systems,” Proc. Int'l Workshop Computer Aided Verification, 1991.
[16] B. Dasarathy, “Timing Constraints of Real-Time Systems: Constructs for Expressing Them, Methods for Validating Them,” IEEE Trans. Software Eng., vol. 11, no. 1, Jan. 1985.
[17] C. Daws, A. Olivero, S. Tripakis, and S. Yovine, “The Tool KRONOS,” Hybrid Systems III, R. Alur, T.A. Henzinger, and E.D. Sontag, eds., 1996.
[18] D. Dill, “Timing Assumptions and Verification of Finite-State Concurrent Systems,” Proc. Workshop Computer Aided Verification Methods for Finite State Systems, 1989.
[19] E.A. Emerson, A.K. Mok, A.P. Sistla, and J. Srinivasan, “Quantitative Temporal Reasoning,” Proc. Workshop Automatic Verification Methods for Finite State Systems, 1989.
[20] A. Fehnker, “Scheduling a Steel Plant with Timed Automata,” Proc. Sixth Int'l Conf. Real-Time Computing Systems and Applications, Dec. 1999.
[21] N. Gehani and K. Ramamrithan, “Real-Time Concurrent C: A Language for Programming Dynamic Real-Time Systems,” J. Real Time Systems, no. 3, 1991.
[22] B. Hamidzadeh and Y. Atif, “Dynamic Scheduling of Real Time Tasks, by Sssignment,” IEEE Concurrency, pp. 14-25, Oct.-Dec. 1998.
[23] M.G. Harbour, M.H. Klein, and J.P. Lehoczky, “Timing Analysis for Fixed Priority Scheduling of Hard Real Time Systems,” IEEE Trans. Software Eng., vol. 20, no. 1, pp. 13-28, Jan. 1994.
[24] M. Humphrey and J.A. Stankovic, “Predictable Threads for Dynamic Hard Real Time Environments,” IEEE Trans. Software Eng., vol. 23, no. 12, pp. 745-758, Dec. 1997.
[25] N. Leveson, “Safety Analysis Using Petri Nets,” IEEE Trans. Software Eng., vol. 13, no. 3, Mar. 1987.
[26] C.L. Liu and J.W. Layland, “Scheduling Algorithms for Multiprogramming in a Hard Real-Time Environment,” J. ACM, vol. 20, no. 1, pp. 40-61, 1973.
[27] M. Lusini and E. Vicario, “Static Analysis and Dynamic Steering of Time-Dependent Systems Using Time Petri Nets,” Technical Report 28.98, Dip. Sistemi e Informatica, Univ. of Florence, 1998.
[28] P. Merlin and D.J. Farber, “Recoverability of Communication Protocols,” IEEE Trans. Comm., vol. 24, no. 9, Sept. 1976.
[29] T. Murata, “Petri Nets: Properties, Analysis and Application,” Proc. IEEE, vol. 77, no. 4, 1989.
[30] X. Nicollin, J. Sifakis, and S. Yovine, “Compiling Real-Time Specifications into Extended Automata,” IEEE Trans. Software Eng., vol. 18, no. 9, Sept. 1992.
[31] C. Norstrom, A. Wall, and W. Yi, “Timed Automata as Task Models for Event Driven Systems,” Proc. Sixth Int'l Conf. Real-Time Computing Systems and Applications, Dec. 1999.
[32] M. Notomi and T. Murata, “Hierarchical Reachability Graph of Bounded Petri Nets for Concurrent Software Analysis,” IEEE Trans. Software Eng., vol. 19, no. 1, Jan. 1993.
[33] J.S. Ostroff, “Deciding properties of Timed Transition Models,” IEEE Trans. Paralel and Distributed Systems, vol. 1, no. 2, Apr. 1990.
[34] Y.A. Papelis and T.L. Casavant, “Specification of Parallel/Distributed Software and Systems by Petri Nets with Transition Enabling Functions,” IEEE Trans. Software Eng., vol. 18, no. 3, Mar. 1992.
[35] D.-T. Peng, K.G. Shin, and T.F. Abdelzaher, “Assignment and Scheduling Communicating Periodic tasks in Distributed Real Time Systems,” IEEE Trans. Software Eng., vol. 23, no. 12, pp. 745-758, Dec. 1997.
[36] J. Xu and D.L. Parnas, "On Satisfying Timing Constraints in Hard Real-Time Systems," IEEE Trans. Software Eng., Vol. 19, No. 1, Jan. 1993, pp. 70-84.
[37] J.L. Peterson, “Petri Nets,” ACM Computing Surveys, vol. 9, no. 3, Sept. 1977.
[38] K. Ramamritham and J.A. Stankovic, “Scheduling Algorithms and Operating System Support for Real Time Systems,” Proc. IEEE, vol. 82, no. 1, Jan. 1994.
[39] K. Ramamritham, “Allocation and Scheduling of Precedence-Related Periodic Tasks,” IEEE Trans. Parallel and Distributed Systems, vol. 6, no. 4, pp. 412-420, Apr. 1995.
[40] K. Ramamritham, J.A. Stankovic, and W. Zhao, “Distributed Scheduling of Tasks with Deadlines and Resource Requirements,” Trans. Computers, vol. 38, no. 8, Aug. 1989.
[41] L. Sha, R. Rajkuma, and J.P. Lehoczky, "Priority Inheritance Protocols: An Approach to Real-Time Synchronization," IEEE Trans. Computers, vol. 39, no. 9, pp. 1,175-1,185, Sept. 1990.
[42] L. Sha, R. Rajkumar, and S.S. Sathaye, “Generalized Rate Monotonic Scheduling Theory: A Framework for Developing Real Time Systems,” Proc. IEEE, vol. 82, no. 1, Jan. 1994.
[43] J.A. Stankovic and K. Ramamritham, “The Spring Kernel: A New Paradigm for Real-Time Systems,” IEEE Software, pp. 62-72, May 1991.
[44] J.A. Stankovic and K. Ramamritham, “What is Predictability for Real Time Systems,” J. Real Time Systems, vol. 2, Dec. 1990.
[45] J.A. Stankovic, “Misconceptions About Real Time Computing,” IEEE Computer, vol. 21, no. 10, Oct. 1988.
[46] J. Sun, M.K. Gardner, and J.W.S. Liu, “Bounding Completion Times of Jobs with Arbitrary Release Times, Variable Execution Times, and Resource Sharing,” IEEE Trans. Software Eng., vol. 23, no. 10, Oct. 1997.
[47] W. Zhao, K. Ramamritham, and J.A. Stankovic, “Scheduling Tasks with Resource Requirements in Hard Real Time Systems,” IEEE Trans. Software Eng., vol. 13, no. 5, pp. 564-577, May 1987.
[48] J. Xu and D.L. Parnas, “Scheduling Processes with Release Times, Deadlines, Precedence and Exclusion Relations,” IEEE Trans. Software Eng., vol. 16, no. 3, pp. 360-369, Mar. 1990.

Index Terms:
Time-dependent systems, hard real-time systems, timeliness predictability, enumerative static analysis, dynamic task guarantee, quantitative timing estimation, Time Petri Nets.
Citation:
Enrico Vicario, "Static Analysis and Dynamic Steering of Time-Dependent Systems," IEEE Transactions on Software Engineering, vol. 27, no. 8, pp. 728-748, Aug. 2001, doi:10.1109/32.940727
Usage of this product signifies your acceptance of the Terms of Use.