
This Article  
 
Share  
Bibliographic References  
Add to:  
Digg Furl Spurl Blink Simpy Del.icio.us Y!MyWeb  
Search  
 
ASCII Text  x  
George S. Avrunin, James C. Corbett, Laura K. Dillon, "Analyzing PartiallyImplemented RealTime Systems," IEEE Transactions on Software Engineering, vol. 24, no. 8, pp. 602614, August, 1998.  
BibTex  x  
@article{ 10.1109/32.707696, author = {George S. Avrunin and James C. Corbett and Laura K. Dillon}, title = {Analyzing PartiallyImplemented RealTime Systems}, journal ={IEEE Transactions on Software Engineering}, volume = {24}, number = {8}, issn = {00985589}, year = {1998}, pages = {602614}, doi = {http://doi.ieeecomputersociety.org/10.1109/32.707696}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }  
RefWorks Procite/RefMan/Endnote  x  
TY  JOUR JO  IEEE Transactions on Software Engineering TI  Analyzing PartiallyImplemented RealTime Systems IS  8 SN  00985589 SP602 EP614 EPD  602614 A1  George S. Avrunin, A1  James C. Corbett, A1  Laura K. Dillon, PY  1998 KW  Realtime KW  concurrency KW  static analysis KW  Ada KW  temporal logic KW  hybrid systems KW  Graphical Interval Logic. VL  24 JA  IEEE Transactions on Software Engineering ER   
Abstract—Most analysis methods for realtime 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 partiallyimplemented systems, those for which some components are given only as highlevel specifications while others are fully implemented in a programming language. In this paper, we propose a method for analyzing such partiallyimplemented realtime systems. Here we consider realtime concurrent systems for which some components are implemented in Ada and some are partially specified using regular expressions and Graphical Interval Logic (GIL), a realtime temporal logic. We show how to construct models of the partiallyimplemented systems that account for such properties as runtime 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 RealTime Environment,” J. ACM, vol. 20, no. 1, pp. 4061, 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. 1328, Jan. 1994.
[3] L. Sha and J.B. Goodenough, "RealTime Scheduling Theory and Ada," Computer, vol. 24, no. 4, pp. 5362, Apr. 1990.
[4] L.K. Dillon, G. Kutty, L.E. Moser, P.M. MelliarSmith, and Y.S. Ramakrishna, “A Graphical Interval Logic for Specifying Concurrent Systems,” ACM Trans. Software Eng. Methods, vol. 3, no. 2, pp. 131165, 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. 461483, July 1996.
[8] Y.S. Ramakrishna, P.M. MelliarSmith, L.E. Moser, L.K. Dillon, and G. Kutty, "Interval Logics and Their Decision Procedures, Part II: A RealTime Interval Logic," Theoretical Computer Science, vol. 170, nos. 1/2, pp. 146, Dec. 1996.
[9] J.C. Corbett, "Modeling and Analysis of RealTime Ada Tasking Programs," K. Ramamritham, ed., Proc. RealTime Systems Symp., IEEE CS Press, pp. 132141, Dec. 1994.
[10] J.C. Corbett, "Constructing Abstract Models of Concurrent RealTime 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. 4959, 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. 115125, Dec. 1993.
[14] P. Zave and M. Jackson, "Conjunction as Composition," ACM Trans. Software Engineering and Methodology, vol. 2, no. 4, pp. 379411, Oct. 1993.
[15] M. Pezzè and M. Young, "Generation of Multiformalism StateSpace Analysis Tools," Zeil [26], pp. 172179.
[16] M. Pezzè and M. Young, "Constructing MultiFormalism StateSpace Analysis Tools: Using Rules to Specify Dynamic Semantics of Models," Proc. 19th Int'l Conf. Software Eng.,Boston, pp. 239249, 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. 531540, 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,0421,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. 589594, 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. 334, 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. WongToi, "HyTech: The Next Generation," Proc. RealTime Systems Symp., IEEE CS Press, 1995.
[23] C.Y. Park and A.C. Shaw, "Experiments With a Program Timing Tool Based on SourceLevel Timing Schema," Computer, pp. 4857, May 1991.
[24] Z. Manna and A. Pnueli, Temporal Verification of Reactive Systems: Safety.New York: SpringerVerlag, 1995.
[25] P. Wolper, "The Tableau Method for Temporal Logic: An Overview," Logique et Analyse, vols. 110111, pp. 119136, JuneSept. 1985.
[26] Proc. 1996 Int'l Symp. Software Testing and Analysis (ISSTA), S.J. Zeil, ed., San Diego: ACM Press, Jan. 1996.