This Article 
 Bibliographic References 
 Add to: 
Analyzing Partially-Implemented Real-Time Systems
August 1998 (vol. 24 no. 8)
pp. 602-614

Abstract—Most analysis methods for real-time systems assume that all the components of the system are at roughly the same stage of development and can be expressed in a single notation, such as a specification or programming language. There are, however, many situations in which developers would benefit from tools that could analyze partially-implemented systems, those for which some components are given only as high-level specifications while others are fully implemented in a programming language. In this paper, we propose a method for analyzing such partially-implemented real-time systems. Here we consider real-time concurrent systems for which some components are implemented in Ada and some are partially specified using regular expressions and Graphical Interval Logic (GIL), a real-time temporal logic. We show how to construct models of the partially-implemented systems that account for such properties as run-time overhead and scheduling of processes, yet support tractable analysis of nontrivial programs. The approach can be fully automated, and we illustrate it by analyzing a small example.

[1] 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.
[2] 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.
[3] L. Sha and J.B. Goodenough, "Real-Time Scheduling Theory and Ada," Computer, vol. 24, no. 4, pp. 53-62, Apr. 1990.
[4] L.K. Dillon, G. Kutty, L.E. Moser, P.M. Melliar-Smith, and Y.S. Ramakrishna, “A Graphical Interval Logic for Specifying Concurrent Systems,” ACM Trans. Software Eng. Methods, vol. 3, no. 2, pp. 131-165, Apr. 1994.
[5] L.K. Dillon and Q. Yu, “Oracles for Checking Temporal Properties of Concurrent Systems,” Proc. Symp. Foundations of Software Eng., pp. 140–153, Dec. 1994.
[6] L.K. Dillon and Y.S. Ramakrishna, “Generating Oracles from Your Fravorite Temporal Logic Specificaitons,” Proc. Symp. Foundations of Software Eng., Oct. 1996.
[7] J.C. Corbett, “Timing Analysis of Ada Tasking Programs,” IEEE Trans. Software Eng., vol. 22, no. 7, pp. 461-483, July 1996.
[8] Y.S. Ramakrishna, P.M. Melliar-Smith, L.E. Moser, L.K. Dillon, and G. Kutty, "Interval Logics and Their Decision Procedures, Part II: A Real-Time Interval Logic," Theoretical Computer Science, vol. 170, nos. 1/2, pp. 1-46, Dec. 1996.
[9] J.C. Corbett, "Modeling and Analysis of Real-Time Ada Tasking Programs," K. Ramamritham, ed., Proc. Real-Time Systems Symp., IEEE CS Press, pp. 132-141, Dec. 1994.
[10] J.C. Corbett, "Constructing Abstract Models of Concurrent Real-Time Software," S. Ziel, ed., Proc. 1996 Int'l Symp. Software Testing and Analysis (ISSTA). ACM Press, Jan. 1996.
[11] E.M. Clarke, D.E. Long, and K.L. McMillan, “Compositional Model Checking,” Proc. Fourth Ann. Symp. Logic in Computer Science, June 1989.
[12] W.J. Yeh and M. Young, "Compositional Reachability Analysis Using Process Algebra," Proc. ACM SIGSOFT Symp. Testing, Analysis and Verification, pp. 49-59, Oct. 1991.
[13] S.C. Cheung and J. Kramer, "Enhancing Compositional Reachability Analysis Using Context Constraints," Proc. First ACM SIGSOFT Symp. Foundations of Software Engineering, pp. 115-125, Dec. 1993.
[14] P. Zave and M. Jackson, "Conjunction as Composition," ACM Trans. Software Engineering and Methodology, vol. 2, no. 4, pp. 379-411, Oct. 1993.
[15] M. Pezzè and M. Young, "Generation of Multi-formalism State-Space Analysis Tools," Zeil [26], pp. 172-179.
[16] M. Pezzè and M. Young, "Constructing Multi-Formalism State-Space Analysis Tools: Using Rules to Specify Dynamic Semantics of Models," Proc. 19th Int'l Conf. Software Eng.,Boston, pp. 239-249, May 1997.
[17] M. Pezzè, "A Formal Approach to the Development of High Integrity Programmable Electronic Systems," High Integrity Systems, vol. 1, no. 6, pp. 531-540, 1996.
[18] R.L. Bagrodia and C.-C. Shen, "MIDAS: Integrated Design and Simulation of Distributed Systems," IEEE Trans. Software Eng., vol. 17, no. 10, pp. 1,042-1,058, Oct. 1991.
[19] C.-C. Shen and R.L. Bagrodia, "Parallel Hybrid Models in System Design," Proc. Winter Simulation Conf.—WSC '93, G.W. Evens, M. Mollaghasemi, E.C. Russell, and W.E. Biles, eds., pp. 589-594, Dec. 1993.
[20] R. Alur, C. Courcoubetis, N. Halbwachs, T. Henzinger, P. Ho, X. Nicollin, A. Olivero, J. Sifakis, and S. Yovine, "The Algorithmic Analysis of Hybrid Systems," Theoretical Computer Science, vol. 138, pp. 3-34, 1995.
[21] 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.
[22] T.A. Henzinger, P.-H. Ho, and H. Wong-Toi, "HyTech: The Next Generation," Proc. Real-Time Systems Symp., IEEE CS Press, 1995.
[23] C.Y. Park and A.C. Shaw, "Experiments With a Program Timing Tool Based on Source-Level Timing Schema," Computer, pp. 48-57, May 1991.
[24] Z. Manna and A. Pnueli, Temporal Verification of Reactive Systems: Safety.New York: Springer-Verlag, 1995.
[25] P. Wolper, "The Tableau Method for Temporal Logic: An Overview," Logique et Analyse, vols. 110-111, pp. 119-136, June-Sept. 1985.
[26] Proc. 1996 Int'l Symp. Software Testing and Analysis (ISSTA), S.J. Zeil, ed., San Diego: ACM Press, Jan. 1996.

Index Terms:
Real-time, concurrency, static analysis, Ada, temporal logic, hybrid systems, Graphical Interval Logic.
George S. Avrunin, James C. Corbett, Laura K. Dillon, "Analyzing Partially-Implemented Real-Time Systems," IEEE Transactions on Software Engineering, vol. 24, no. 8, pp. 602-614, Aug. 1998, doi:10.1109/32.707696
Usage of this product signifies your acceptance of the Terms of Use.