
This Article  
 
Share  
Bibliographic References  
Add to:  
Digg Furl Spurl Blink Simpy Del.icio.us Y!MyWeb  
Search  
 
ASCII Text  x  
Jia Xu, "On Inspection and Verification of Software with Timing Requirements," IEEE Transactions on Software Engineering, vol. 29, no. 8, pp. 705720, August, 2003.  
BibTex  x  
@article{ 10.1109/TSE.2003.1223645, author = {Jia Xu}, title = {On Inspection and Verification of Software with Timing Requirements}, journal ={IEEE Transactions on Software Engineering}, volume = {29}, number = {8}, issn = {00985589}, year = {2003}, pages = {705720}, doi = {http://doi.ieeecomputersociety.org/10.1109/TSE.2003.1223645}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }  
RefWorks Procite/RefMan/Endnote  x  
TY  JOUR JO  IEEE Transactions on Software Engineering TI  On Inspection and Verification of Software with Timing Requirements IS  8 SN  00985589 SP705 EP720 EPD  705720 A1  Jia Xu, PY  2003 KW  Realtime KW  software KW  code KW  inspection KW  verification KW  timing requirements KW  current practices KW  complexity KW  restrictions KW  software structures KW  preruntime scheduling KW  predictability. VL  29 JA  IEEE Transactions on Software Engineering ER   
Abstract—Software with hard timing requirements should be designed using a systematic approach to make its timing properties easier to inspect and verify; otherwise, it may be practically impossible to determine whether the software satisfies the timing requirements. Preruntime scheduling provides such an approach by placing restrictions on software structures to reduce complexity. A major benefit of using a preruntime scheduling approach is that it makes it easier to systematically inspect and verify the timing properties of the actual software code, not just various highlevel abstractions of the code.
[1] R. Alur, C. Courcoubetis, T.A. Henzinger, and P.H. Ho, Hybrid Automata: An Algorithmic Approach to the Specification and Verification of Hybrid Systems Hybrid Systems, R.L. Grossman, A. Nerode, A. Ravn, and H. Rischel, eds., 1993.
[2] R. Alur and D. Dill, “A Theory of Timed Automata,” Theoretical Computer Science, vol. 126, pp. 183235, 1994.
[3] R. Alur and T.A. Henzinger, RealTime Logics: Complexity and Expressiveness Proc. Fifth Ann. IEEE Symp. Logic in Computer Science, pp. 390401, 1990.
[4] R. Alur and T. Henzinger, "Logics and Models of RealTime: A Survey," RealTime: Theory in Practice, Lecture Notes in Computer Science 600, pp. 74106.
[5] S.R. Ball, Debugging Embedded Microprocessor Systems. Newnes, 1998.
[6] S.R. Ball, Embedded Microprocessor Systems: Real World Design, second ed. Newnes, 2000.
[7] P. Bellini, R. Mattolini, and P. Nesi, Temporal Logics for RealTime System Specification ACM Computing Surveys, vol. 32, no. 1, pp. 1242, 2000.
[8] A. Burns, K. Tindell, and A. Wellings, “Effective Analysis for Engineering RealTime Fixed Priority Schedulers,” IEEE Trans. Software Eng., vol. 21, no. 5, pp. 475480, May 1995.
[9] S.V. Campos and E.M. Clarke, The Verus Language: Representing Time Efficiently with BDDs Theoretical Computer Science, 1999.
[10] G.D. Carlow, Architecture of the Space Shuttle Primary Avionics Software System Comm. ACM, vol. 27, pp. 926936, Sept. 1984.
[11] E.M. Clarke, E.A. Emerson, and A.P. Sistla, "Automatic verification of finitestate concurrent systems using temporal logic specifications," ACM Trans. Programming Languages and Systems, vol. 8, no. 2, pp. 244263, 1986.
[12] E.M. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith, Progress on the State Explosion Problem in Model Checking Informatics. 10 Years Back. 10 Years Ahead, R. Wilhelm, ed., 2001.
[13] E.M. Clarke and J.M. Wing, "Formal Methods: State of the Art and Future Directions," ACM Computing Surveys, vol. 28, no. 4, pp. 626643, 1996.
[14] E. Closse, M. Poize, J. Pulou, J. Sifakis, P. Venter, D. Weil, and S. Yovine, TAXYS: A Tool for the Development and Verification of RealTime Embedded Systems Proc. 13th Int'l Conf. Computer Aided Verification (CAV), pp. 391395, 2001.
[15] D. Cofer and M. Rangarajan, Formal Modeling and Analysis of Advanced Scheduling Features in an Avionics RTOS Proc. Int'l Workshop Embedded Software (EMSOFT 2002), A. SangiovanniVincentelli and J. Sifikis, eds., 2002.
[16] P. Chou and G. Borriello, "Modal Processes: Towards Enhanced Retargetability Through Control Composition of Distributed Embedded Systems," Proc. Design Automation Conf., June 1998.
[17] P. Cousot and R. Cousot, Verification of Embedded Software: Problems and Perspectives Proc. Int'l Workshop Embedded Software (EMSOFT 2001), 2001.
[18] 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.
[19] E.W. Dijkstra, Cooperating Sequential Processes Programming Languages, F. Genuys, ed., pp. 43112, 1968.
[20] D. Dill and J. Rushby, Acceptance of Formal Methods: Lessons from Hardware Design Computer, vol. 29, pp. 2324, 1996.
[21] B. Dutertre, Formal Analysis of the Priority Ceiling Protocol Proc. IEEE RealTime Systems Symp., pp. 151160, Nov. 2000.
[22] E.A. Emerson and E.M. Clarke, Using Branching Time Temporal Logic to Synthesize Synchronization Skeletons Science of Computer Programming, vol. 2, pp. 241266, 1982.
[23] E.A. Emerson, A.K. Mok, A.P. Sistla, and J. Srinivasan, Quantitative Temporal Reasoning Proc. Second Workshop ComputerAided Verification, pp. 136145, 1989.
[24] S.R. Faulk and D.L. Parnas, On Synchronization in HardRealTime Systems Comm. ACM, vol. 31, pp. 274287, Mar. 1988.
[25] J.G. Ganssle, The Art of Designing Embedded Systems. Newnes, 2000.
[26] C. Ghezzi, D. Mandrioli, S. Morasca, and M. Pezze, “A Unified HighLevel Petri Net Formalism for TimeCritical Systems,” IEEE Trans. Software Eng., vol. 17, no. 2, pp. 160–171, Feb. 1991.
[27] C. Heitmeyer, "On the Need for Practical Formal Methods," Proc. Formal Techniques in RealTime and FaultTolerant Systems (FTRTFT'98),Lyngby, Denmark, Sept. 1998.
[28] K. Heninger, J. Kallander, D.L. Parnas, and J. Shore, Software Requirements for the A7E Aircraft NRL Report No. 3876, Nov. 1978.
[29] T.A. Henzinger, Z. Manna, and A. Pnueli, "Temporal Proof Methodologies for RealTime Systems," Proc. 18th Ann. ACM Symp. Principles of Programming Languages, pp. 353366, 1990.
[30] T.A. Henzinger and J.F. Raskin, Robust Undecidability of Timed and Hybrid Systems Proc. Third Int'l Workshop Hybrid Systems: Computation and Control, 2000.
[31] Software Fundamentals: Collected Papers by David L. Parnas. D.M. Hoffman and D.M. Weiss, eds., AddisonWesley, 2001.
[32] G.J. Holzmann, “The Model Checker SPIN,” IEEE Trans. Software Eng., vol. 23, May 1997.
[33] F. Jahanian and A. K.L. Mok,“Safety analysis of timing properties in realtime systems,”IEEE Trans. Software Eng., vol. SE12, pp. 890–904, Sept. 1986.
[34] M. H. Klein, T. Ralya, B. Pollak, R. Obenza, and M. G. Harobur,A Practitioner's Handbook for RealTime Analysis: Guide to Rate Monotonic Analysis for RealTime Systems. New York: Kluwer–Academic, 1993.
[35] H. Kopetz, RealTime Systems Design Principles for Distributed Embedded Applications, Kluwer Academic, Boston, 1997.
[36] 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.
[37] K.L. McMillan, Symbolic Model Checking. Kluwer Academic, 1993.
[38] M.P. MelliarSmith and R. L. Schwartz, Formal Specification and Mechanical Verification of SIFT: A FaultTolerant Flight Control System IEEE Trans. Computers, vol. 31, no. 7, pp. 616629, July 1982.
[39] A.K. Mok, Fundamental Design Problems of Distributed Systems for the HardRealTime Environment PhD thesis, Dept. of Electrical Eng. and Computer Science, Massachusetts Inst. of Technology, Cambridge, Mass., May 1983.
[40] A.K. Mok, The Design of RealTime Programming Systems Based on Process Models Proc. IEEE RealTime Systems Symp., pp. 517, Dec. 1984.
[41] J. Ostroff, Temporal Logic for RealTime Systems. John Wiley and Sons, 1989.
[42] D.L. Parnas, Inspection of SafetyCritical Software Using ProgramFunction Tables Proc. IFIP World Congress 1994, vol. 3, Aug. 1994.
[43] J. Penix, W. Visser, E. Engstrom, A. Larson, and N. Weininger, Verification of Time Partitioning in the DEOS Scheduler Kernel Proc. Int'l Conf. Software Eng., pp. 488497, 2000.
[44] J.P. Queille and J. Sifakis, "Specification and Verification of Concurrent Systems in CESAR," Int'l Symp. Programming, pp. 337351, Lecture Notes in Computer Science 137, SpringerVerlag, Apr. 1982.
[45] L. Sha, R. Rajkuma, and J.P. Lehoczky, "Priority Inheritance Protocols: An Approach to RealTime Synchronization," IEEE Trans. Computers, vol. 39, no. 9, pp. 1,1751,185, Sept. 1990.
[46] T. Shepard and M. Gagne, A Model of the F18 Mission Computer Software for Preruntime Scheduling Proc. 10th Int'l Conf. Distributed Computing Systems, pp. 6269, 1990.
[47] T. Shepard and M. Gagne, “A PreRunTime Scheduling Algorithm for Hard RealTime Systems,” IEEE Trans. Software Eng., vol. 17, no. 7, pp. 669677, July 1991.
[48] W. Soukoreff, A Comparison of Two Preruntime ScheduleDispatchers for RTAI COSC6390 Project Report, Dept. of Computer Science, York Univ., Dec. 2001.
[49] Hard RealTime Systems IEEE Computer Society Tutorial, J. Stankovic and K. Ramamrithan, eds., 1988.
[50] J.A. Stankovic, M. Spuri, M. Di Natale, and G. Buttazzo, “Implications of Classical Scheduling Results for RealTime Systems,” IEEE Computer, vol. 28, no. 6, June 1995.
[51] J. Xu, “Multiprocessor Scheduling of Processes with Release Times, Deadlines, Precedence, and Exclusion Relations,” IEEE Trans. Software Eng., vol. 19, no. 2, pp. 139154, Feb. 1993.
[52] J. Xu, Making Timing Properties of Software Easier to Inspect and Verify IEEE Software, July/Aug. 2003.
[53] J. Xu and K.y. Lam, Integrating Runtime Scheduling and Preruntime Scheduling of RealTime Processes Proc. 23rd IFAC/IFIP Workshop RealTime Programming, June 1998.
[54] 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. 360369, Mar. 1990.
[55] J. Xu and D.L. Parnas, Preruntime Scheduling of Processes with Exclusion Relations on Nested or Overlapping Critical Sections Proc. 11th Ann. IEEE Int'l Phoenix Conf. Computers and Comm. (IPCCC92), Apr. 1992.
[56] J. Xu and D.L. Parnas, "On Satisfying Timing Constraints in Hard RealTime Systems," IEEE Trans. Software Eng., Vol. 19, No. 1, Jan. 1993, pp. 7084.
[57] J. Xu and D.L. Parnas, Fixed Priority Scheduling versus PreRunTime Scheduling RealTime Systems, vol. 18, pp. 723, Jan. 2000.