基于实时规约的测试预言自动生成技术的研究
摘要
实时系统目前已广泛应用于工业、军事和民用高科技的各个领域，其中，航空航天、医疗监控、军事指挥和武器装备控制等领域对实时系统的安全性和实时性要求非常高。一旦软件控制出现问题，后果往往不堪设想。为此，实时软件在正式投入使用之前，必须保证其正确性。实时系统的显著特性是对系统的时序性要求严格。由于实时逻辑语义精确、对实时系统时序性质描述能力强大、测试和验证算法便捷，因此日益受到软件工程领域研究人员和系统工程师们的重视。
鉴于人们对高质量软件的迫切需求，以软件测试为中心的质量保障技术在软件生产实践中得到了迅速发展和广泛应用，已成为发现软件缺陷、保证软件质量的关键技术之一。测试预言(test oracle)是检验待测系统在特定执行下是否正确运行的方法，也是软件测试过程中的重要环节。本文提出了基于受限度量区间时序逻辑(Metric Interval Temporal Logic，MITL)的测试预言自动生成技术。首先针对MITL_([0，b])的语法和语义，使用模型检验中的tableau思想，通过使用重写规则，将一条线性因果的MITL_([0，b])逻辑公式自动转换为带接收状态的时间自动机(Timed Automata with Accepting States，TAAS)，由时间自动机充当测试预言。然后，在此基础上对实时规约的表达能力进行扩充，针对MITL_([a，6])的语法和语义，提出相应的测试预言自动生成算法。
由于生成的时间自动机是非确定的，因此，充当测试预言的自动机的状态空间对于检验实时系统的效率起着决定作用，状态空间越大、迁移越多，运行时的系统开销越大。为此，本文提出对时间自动机进行优化的方法，尽可能地减少冗余状态、去除不可达状态。此外，本文还对带时标的状态序列的精化过程提出优化方法，在一定程度上缩减了由精化产生的额外状态-区间对。
测试预言以实时系统的轨迹作为输入。获取轨迹的方法有两种，要么在系统外部进行监测，要么在系统内部插入断言并输出。两种方法各有利弊，外部监测不会打扰系统运行但可观测的内容受限，而断言的插入则会打扰实时系统的实际运行，进而可能改变系统的时间特性。本文提出一种折衷的方法，根据规约的内容选择获取轨迹的方法，该方法是上述两种方法的综合，力图吸取上述两种方法的长处，而回避两者的不足。使用最差情况执行时间(Worst Case Execution Time，WCET)分析技术，对插入的断言开销进行了分析，进而对由于断言的插入而导致对系统时间的影响提出补偿方法。
我们设计并实现了一个Windows环境下的测试预言自动生成工具AutoTO，能够将以MITL书写的实时系统规约自动地转换为可执行的测试预言。
Real-time systems have been widely used in many safety-critical areas such as aviation, spacecraft, medical treatment monitors, military command and weapon equipment control systems. In these fields, the requirements for the safety and timing constraints of real-time systems are very strict. Once some control-related errors occur at run-time, the consequence may be disastrous. So the correctness of real-time software must be guaranteed before their release. Real-time logic have obtained more and more attentions of software engineering researchers and system engineers, because their accurate syntax and semantic are able to quantitatively characterize the timing constraints of real-time systems.
Due to the urgent needs for high quality software, the testing-centric quality guarantee techniques have been widely applied. Test oracle is a method for verifying whether a system under test is running as desired on a particular execution, and also an indispensable stage of software testing. However it has not been thoroughly investigated in software testing research. . This thesis proposes an approach to automatic generation of test oracle from restricted MITL (Metric Interval Temporal Logic). Firstly, a linear-causal MITL_[0, b] formula is automatically translated into a TAAS (Timed Automata with Accepting States) which acts as the test oracle using the tableau idea in model checking. Secondly, MITL_[0, b] is extended to MITL_[a, b]. The thesis proposes a method for automatic generation of test oracle based on the syntax and semantic of MITL_[a,b].
The size of the state space of TAAS determines the efficiency of the run-time verification of the systems under test. The larger the state space and the transition set are, the larger the overhead of testing will be. This thesis proposes some optimized technologies for TAAS to reduce redundant and unreachable states. Moreover, an optimized refinement method is proposed for timed state sequence to reduce the extra state-interval tuples produced by the refinement.
The inputs of test oracles are the traces of real-time systems. Two methods can be used to acquire the traces: one is to monitor the systems from outside, and the other is to insert assertions into the systems and observe their outputs. Each method has its advantage and weakness. The former method will not disturb the running of the systems, but it cannot acquire all the system events. The latter method does the opposite. In order to reduce or even remove the timing impact of the inserted assertions during testing, the thesis advances a new monitoring schema which has less time intrusiveness than software motoring and can test the tested system completely.
鉴于人们对高质量软件的迫切需求，以软件测试为中心的质量保障技术在软件生产实践中得到了迅速发展和广泛应用，已成为发现软件缺陷、保证软件质量的关键技术之一。测试预言(test oracle)是检验待测系统在特定执行下是否正确运行的方法，也是软件测试过程中的重要环节。本文提出了基于受限度量区间时序逻辑(Metric Interval Temporal Logic，MITL)的测试预言自动生成技术。首先针对MITL_([0，b])的语法和语义，使用模型检验中的tableau思想，通过使用重写规则，将一条线性因果的MITL_([0，b])逻辑公式自动转换为带接收状态的时间自动机(Timed Automata with Accepting States，TAAS)，由时间自动机充当测试预言。然后，在此基础上对实时规约的表达能力进行扩充，针对MITL_([a，6])的语法和语义，提出相应的测试预言自动生成算法。
由于生成的时间自动机是非确定的，因此，充当测试预言的自动机的状态空间对于检验实时系统的效率起着决定作用，状态空间越大、迁移越多，运行时的系统开销越大。为此，本文提出对时间自动机进行优化的方法，尽可能地减少冗余状态、去除不可达状态。此外，本文还对带时标的状态序列的精化过程提出优化方法，在一定程度上缩减了由精化产生的额外状态-区间对。
测试预言以实时系统的轨迹作为输入。获取轨迹的方法有两种，要么在系统外部进行监测，要么在系统内部插入断言并输出。两种方法各有利弊，外部监测不会打扰系统运行但可观测的内容受限，而断言的插入则会打扰实时系统的实际运行，进而可能改变系统的时间特性。本文提出一种折衷的方法，根据规约的内容选择获取轨迹的方法，该方法是上述两种方法的综合，力图吸取上述两种方法的长处，而回避两者的不足。使用最差情况执行时间(Worst Case Execution Time，WCET)分析技术，对插入的断言开销进行了分析，进而对由于断言的插入而导致对系统时间的影响提出补偿方法。
我们设计并实现了一个Windows环境下的测试预言自动生成工具AutoTO，能够将以MITL书写的实时系统规约自动地转换为可执行的测试预言。
Real-time systems have been widely used in many safety-critical areas such as aviation, spacecraft, medical treatment monitors, military command and weapon equipment control systems. In these fields, the requirements for the safety and timing constraints of real-time systems are very strict. Once some control-related errors occur at run-time, the consequence may be disastrous. So the correctness of real-time software must be guaranteed before their release. Real-time logic have obtained more and more attentions of software engineering researchers and system engineers, because their accurate syntax and semantic are able to quantitatively characterize the timing constraints of real-time systems.
Due to the urgent needs for high quality software, the testing-centric quality guarantee techniques have been widely applied. Test oracle is a method for verifying whether a system under test is running as desired on a particular execution, and also an indispensable stage of software testing. However it has not been thoroughly investigated in software testing research. . This thesis proposes an approach to automatic generation of test oracle from restricted MITL (Metric Interval Temporal Logic). Firstly, a linear-causal MITL_[0, b] formula is automatically translated into a TAAS (Timed Automata with Accepting States) which acts as the test oracle using the tableau idea in model checking. Secondly, MITL_[0, b] is extended to MITL_[a, b]. The thesis proposes a method for automatic generation of test oracle based on the syntax and semantic of MITL_[a,b].
The size of the state space of TAAS determines the efficiency of the run-time verification of the systems under test. The larger the state space and the transition set are, the larger the overhead of testing will be. This thesis proposes some optimized technologies for TAAS to reduce redundant and unreachable states. Moreover, an optimized refinement method is proposed for timed state sequence to reduce the extra state-interval tuples produced by the refinement.
The inputs of test oracles are the traces of real-time systems. Two methods can be used to acquire the traces: one is to monitor the systems from outside, and the other is to insert assertions into the systems and observe their outputs. Each method has its advantage and weakness. The former method will not disturb the running of the systems, but it cannot acquire all the system events. The latter method does the opposite. In order to reduce or even remove the timing impact of the inserted assertions during testing, the thesis advances a new monitoring schema which has less time intrusiveness than software motoring and can test the tested system completely.
引文
[1] The Committee on Information and Communications R&D (CIC) of the National Science, Technology Council (NSTC). America in the Age of Information: A Forum on Federal Information and Communications R&D. Bethesda, Maryland. July 6-7, 1995.
[2] Committee on Computing, Information, and Communications, National Science and Technology Council Research Challenges in High Confidence Systems: Proceedings of the Committee on Computing, Information, and Communications Workshop, August 6-7, 1997, http://www.nitrd.gov/pubs/hcs-Aug97/
[3] High Confidence Systems Working Group, Committee on Computing, Information, and Communications Research and Development, National Science and Technology Council. SETTING AN INTERAGENCY HIGH CONFIDENCE SYSTEMS (HCS) RESEARCH AGENDA: Proceedings of the Interagency High Confidence Systems Workshop. Hosted by the National Coordination Office for Computing, Information, and Communications. Arlington, Virginia. 25 March 1998
[4] High Confidence Software and Systems Coordinating Group, Interagency Working Group on Information Technology Research and Development. HIGH CONFIDENCE SOFTWARE AND SYSTEMS RESEARCH NEEDS, 10, January 2001, http://www.nitrd.gov/pubs/hcss-research.pdf
[5] Ministry of Defence: "INT DEF STAN 00-55: The Procurement of Safety Critical Software in Defence Equipment - Issue 1", MoD, April 1991.
[6] Department of Defense. MIL-STD-882B System Safety Program Requirements, July 1, 1987 NOTICE 1. http://sparc.airtime.co.uk/users/wysywig/882b.htm
[7] Laplante, P.: Real-Time Systems Design and Analysis: An Engineer' s Handbook. Ieee Press, New York (1992)
[8] J.A.Stankovic: Misconceptions about real-time computing a serious problem for next generation systems. IEEE Computer 21(10) (1998) 10-19
[9] P. J. Pulli, P. Marko, and Heikkinen, Concurrent engineering for real-time systems. IEEE Software, November/December 1993,10(6): p. 33-38
[10] A. Pnueli. Applications of temporal logic to the specification and verification of reactive systems: a survey of current trends, In Current Trends in Concurrency. Overviews and Tutorials, New York, Springer Lecture Notes in Computer Science, Springer-Verlag, 1986
[11] M. Falla, Advances in Safety Critical Systems: Results and Achievements from the DTI/EPSRC R&D Programe in Safety Critical Systems, Mike Falla, 1997. http://www.comp.lancs.ac.uk/computing/resources/scs/
[12] Richard N Taylor, Structural testing of concurrent programs. IEEE transaction on Software Engineering, March, 18 1992
[13] S. V. Campos, A Quantitative Approach to the Formal Verification of Real-time System, PhD thesis, Carnegie Mellon University, 1996[14] 郑人杰，计算机软件测试技术，清华大学出版社，1992
[15] ANSI/IEEE Std 829-1983, IEEE Standard for Software Test Documentation
[16] 朱鸿，金凌紫，软件质量保障与测试，科学出版社，1997
[17] L. Baresi and M. Young, Test Oracles, Technical Report, CIS-TR01-02, Dept. of Computer and Information Science, Univ. of Oregon, Aug. 2001. http://www.cs.uoregon.edu/-michal/pubs/oracles.html
[18] W. E. Howden and P. Eichhorst, Proving properties of programs from program traces, in Tutorial: Software Testing and Validation, ed by E. Miller and W. E. Howden in IEEE Computer Society: New York. p. 46-56, 1978
[19] L. J. White and E. I. Cohe, A domain strategy for computer program testing. IEEE Transaction on Software Engineering, SE-6: p. 247-257, 1990
[20] R. Alur and T. A. Henzinger. A really temporal logic, In Proceedings of the 30th IEEE Conference on Foundatiions of Computer Science, Los Alamitos, CA, IEEE Computer Society Press, 1989
[21] P. Bellini, R. Mattolini, and P. Nesi, Temporal logics for real-time system specification. ACM Computing Surveys, 32(1): p. 12-42, March 2000
[22] Alur, R.: Techniques of Automatic Verification of Real-Time Systems. PhD thesis, PhD thesis, Stanford University (1991)
[23] R. Alur, T. Feder, and T. Henzinger. The benefits of relaxing punctuality. Journal of the ACM, 43(1): 116{146, January 1996
[24] 《冯友兰学术精华录》，北京师范学院出版社，鲍霁主编，1988年，第119至125页
[25] 明，王夫之，《船山全书》第七册，岳麓出版社，第110页
[26] D. J. Panzl, Automatic Software Test Drivers. Computer, April 1978, 11(4): p. 44-50
[27] Richard G. Hamlet, Testing Programs with the Aid of a Compiler. IEEE Transactions on Software Engineering, July 1977, 3(4): p. 279-290
[28] D. Chapman, A Program Testing Assistant. Communications of the ACM, September 1982
[29] Elaine J. Weyuker, On testing non-testable programs. Computer Journal, 25, 1982: p. 465-470
[30] J. D. Day and J. D. Gannon. A test oracle based on formal specifications. In Proc. SoftFair, A Second Conf. on Software Development Tools, Techniques, and Alternatives, ACM Press, San Francisco, Dec 1985, pages 126-130
[31] Richard N. Taylor, An integrated verification and testing environment. Software-Practice and Experience, 1983, 13: p. 697-713
[32] D.C. Luckham and F.W. von Henke, Overview of Anna, a Specification Language for Ada. IEEE Software, March 1985, 2(2): p. 9-22
[33] D. C. Luckham, F. W. von Henke, B. Krieg-Bruckner, and O. Owe, Anna-A Language for Annotating Ada Programs. Lecture Notes in Computer Science, Springer-Verlag, 1987
[34] S. Sankar, D. Rosenblum, and R. Neff. An Implementation of Anna, In Proceedings of the Ada International Conference on Ada in Use, ACM, Cambridge University Press, May 1985[35] David Luckham, Programming with Specifications: An Introduction to ANNA, A Language for Specifying Ada Programs. Springer-Verlag, 1990
[36] David S. Rosenblum. Towards a Method of Programming with Assertions, In Proceedings of the 14th International Conference on Software Engineering, May 1992
[37] David S. Rosenblum, A Practical Approach to Programming With Assertions. IEEE Transactions on Software Engineering, 21(1): p. 19-31, January 1995
[38] R. Kramer. iContract - The Java Design by Contract Tool, In Proceedings of TOOLS26: Technology of Object-Oriented Languages and Systems, IEEE Computer Society, 1998.
[39] P.J. Maker, GNU Nana - User's Guide (version 2.4), Technical report, School of Information Technology - Northern Territory University, July 1998
[40] Jones, C.B., Systematic Software using VDM, 2nd ed., Prentice Hall, 1990.
[41] Bertrand Meyer, Eiffel: The Language. Object-Oriented Series, Prentice Hall, New York, 1992
[42] Bertrand Meyer, Object-Oriented Software Construction. Second Edition, The Object-Oriented Series, Prentice-Hall, 1997
[43] S. Sankar and R. Hayes, ADL: An Interface Definition Language for Specifying and Testing Software. ACM SIGPLAN Notices, August 1994, 29(8): p. 13-21
[44] Sun Microsystems, ADL language reference manual, 1993
[45] ADL Project, Ad1 2, http://adl.opengroup.org/exgr/
[46] S. R. Viswanadha and S. Sankar. Preliminary Design of ADL/C++ - A Specification Langauge for C++, In Proceedings of the 2nd Conference on Object-Oriented Technologies and Systems (COOTS), Toronto, Canada, June 1996
[47] M. Obayashi, H. Kubota, S.P. McCarron, and L. Mallet, The Assertion Based Testing Tool for OOP: ADL2. May 1998
[48] Dennis K. Peters and David L. Parnas, Using Test Oracles Generated from Program Documentation. IEEE Transactions on Software Engineering, 1998, 24(3): p. 161-173
[49] D.L. Parnas, J. Madey, and M. Iglewski, Precise Documentation of Well-Structured Programs. IEEE Transactions on Software Engineering, December 1994, 20(12): p. 948-976
[50] John D. Gannon, Paul McMullin, and Richard G Hamlet, Data-Abstraction mplementation, Specification, and Testing. ACM Transactions on Programming Languages and Systems, July 1981, 3(3): p. 211-223
[51] Victor R. Basili. The Design and Implementation of a Family of Application-Oriented Languages. In Proceedings of the 5th Texas Conference on Computing Systems, October 1976, pages 6-12
[52] Sergio Antoy and Richard G. Hamlet, Automatically Checking an Implementation against Its Formal Specification. IEEE Transactions on Software Engineering, January 2000, 26(1): p. 55-69
[53] S. Fujiwara, G. v. Bochmann, F. Khendek, M. Amalou, and A. Ghedamsi, Test Selection Based on Finite State Models. IEEE Transactions on Software Engineering, June 1991, 17(6): p. 591-603[54] Atif M. Memon, Martha E. Pollack, and Mary Lou Soffa. Automated test oracles for GUIs. In Proceedings of the ACM SIGSOFT 8th International Symposium on the Foundations of Software Engineering (FSE-00), volume 25, 6 of ACM Software Engineering Notes. ACM Press, November 2000, pages 30-39
[55] James H. Andrews. Testing using log file analysis: Tools, methods, and issues, In Proceedings of the 13 th IEEE International Conference on Advanced Software Engineering, Honolulu, Hawaii, October 1998
[56] James H. Andrews and Yingjun Zhang. Broad-spectrum studies of log file analysis, In Proceedings of the 22nd International Conference on Software Engineering (ICSE 2000), Limerick, Ireland, ACM Press, June 2000
[57] Martin S. Feather, Rapid application of lightweight formal methods for consistency analysis. IEEE Transactions on Software Engineering, November 1998, 24(11): p. 949-959
[58] Martin S. Feather and Ben Smith, Automatic generation of test oracles - from pilot studies to application. Automated Software Engineering Journal, 2001, 8(1): p. 31-62
[59] John M. Spivey. The Z Notation: A Reference Manual. Prentice-Hall, 1989
[60] D. Carrington, D. Duke, R. Duke, P. King, G. Rose, and G Smith. Object-Z: An object-oriented extension to Z. In Formal Description Techniques (FORTE '89), North-Holland Publishing Co., December 1989 , pages 281-296
[61] E. Mikk. Compilation of Z Specifications into C for Automatic Test Result Evaluation. In Proceedings of the 9th International Conference of Z Users, volume 967 of Lecture Notes in Computer Science, Springer-Verlag, 1995., pages 167-180
[62] J. McDonald, L. Murray, and P. Strooper. Translating Object-Z specifications to object-oriented test oracles. In Proceedings: 4th Asia-Pacific Software Engineering and International Computer Science Conference, IEEE Computer Society Press, 1997, pages 414-426
[63] J. McDonald and P. Strooper. Translating Object-Z specifications to passive test oracles. In Proceedings of the 2nd International Conference on Formal Engineering Methods (ICFEM98), IEEE Computer Society Press, 1998, pages 165-174
[64] Paul Stocks and David Carrington. A Framework for Specification-Based Testing. IEEE Transactions on Software Engineering, 1996, 22(11):777-793
[65] L.K. Dillon and Qing Yu. Oracles for Checking Temporal Properties of Concurrent Systems, In Proceedings of the ACM SIGSOFT '94 Symposium on the Foundations of Software Engineering, December 1994
[66] L.K. Dillon and Y.S. Ramakrishna. Generating Oracles from Your Favorite Temporal Logic Specifications, In Proceedings of the Fourth ACM SIGSOFT Symposium on the Foundations of Software Engineering, 21 ACM Press, October 1996
[67] Doron Drusinsky. The Temporal Rover and the ATG Rover, In SPIN Model Checking and Software Verification, Proc, 7th SPIN Workshop, Stanford, California, 1885 of Springer-Verlag Lecture Notes in Computer Science, Springer Verlag, 2000
[68] John Hakansson, Automated generation of test scripts from temporal logic specification, Master's thesis, Uppsala University, 2000[69] A. Pnueli. The temporal logic of programs, In Proceedings of the 18th Annual Symposium on Foundations of Computer Science, Los Alamitos, CA IEEE Computer Society Press, 1977
[70] A. Pnueli, The temporal semantics of concurrent programs. Theor. Comput. Sci, 13, 1981
[71] A. Pnueli. Applications of temporal logic to the specification and verification of reactive systems: a survey of current trends, In Current Trends in Concurrency. Overviews and Tutorials, New York, Springer Lecture Notes in Computer Science, Springer-Verlag, 1986
[72] L.K. Dillon, G. Kutty, L. E. Moser, P. M. Melliar-Smith, and Y. S. Ramakrishna. Graphical specification for concurrent software systems, In Proc. 14th IEEE Inter. Conf. Software Engineering, Melbourne, May 1992
[73] 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 Engineering and Methodology, 1994
[74] Pierre Wolper, The tableau method for temporal logic: An overview. Logique et Analyse, 1985,110-111: p. 119-136
[75] Moshe Vardy and Pierre Wolper, Reasoning about infinite computations. Information and Computation, 115(1-37), 1994
[76] Rob Gerth, Doron Peled, Moshe Vardi, and Pierre Wolper. Simple on-the-fly automatic verification of linear temporal logic, In Protocol Specification Testing and Verification, Warsaw, Poland, Chapman & Hall, 1995
[77] Y. Kesten, Z. Manna, H. McGuire, and A. Pnueli, A decision algorithm for full prepositional temporal logic. In C. Courooubetis, ed., Proc. 1993 International Conference of Computer-Aided Verification, vol 697 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, 1993, pp. 97-109
[78] H. McGuire, Two Mehtods for Checking Formulas of Temporal Logic, PhD thesis, Dept. of Computer Science, Stanford University, Stanford, California, 1995
[79] Geilen, M.: On the construction of monitors for temporal logic properties. In: K. Havelund and G Rosu, editors, Proceedings of RV'01 - First Workshop on Run-time Verification. Satellite Workshop of CAV'01, Electronic Notes in Theoretical Computer Science 55(2), Amsterdam, 2001. Elsevier Science, Paris, France (2001)
[80] Kupferman, O. and M. Y. Vardi, Model checking of safety properties, in: N. Halbwachs and D. Peled, editors, Computer Aided Verification: 11th International Conference Proceedings, CAV'99(LNCS 1633), Trento, Italy, July 6-10, 1999, pp. 172-183
[81] R. Koymans, Specifying real-time properties with metric temporal logic. Real-Time Systems, November 1990, 2(4): p. 255-299
[82] C. Ghezzi, D. Mandrioli, and A. Morzenti, TRIO: A logic language for executable specifications of real-time systems. Journal of Systems and software, 12(2): p. 107-123, May 1990
[83] M. Felder and A. Morzenti, Validating real-time systems by history-checking TRIO specifications. ACM Transaction on Software Engineering Methodology, 3(4): p. 308-339, October 1994[84] M.C.W.Geilen, Formal Techniques for Verification of Complex Real-Time Systems, PhD Thesis, Eindhoven University of Technology, Netherlands, 2002, pp. 159-205
[85] Marius Mikucionis, Brian Nielsen and Kim G. Larsen, Real-time System Testing On-the-fly, The 15th Nordic Workshop on Programming Theory, Turku, Finland, October 29-31,2003
[86] Wang Yi, Paul Pettersson and Mats Daniels, Automatic Verification of Real-Time Communicating Systems by Constraint Solving, In Proceedings of the 7th International Conference on Formal Description Techniques, North-Holland, 1994, pp. 223-238
[87] K. L. Heninger, J. Kallander, D. L. Parnas, and J. E. Shore, Software Requirements for the A-7E Aircraft, NRL Memorandum Report 3876, United States Naval Research Laboratory, November 1978
[88] Angelo Gargantini and Connie Heitmeyer. Using Model Checking to Generate Tests from Requirements Specifications. In Proceedings of the 7th European Engineering Conference and the 7th ACM SIGSOFT Symposium on the Foundations of Software Engeneering, volume 24.6 of Software Engineering Notes (SEN), ACM Press, September 6-10 1999, pages 146-162
[89] Jin-Cherng Lin and Ian Ho, Generating timed test cases with oracles for real-time software. Advances in Engineering Software, 2001, 32(9): p. 705-715
[90] J. L. Peterson. Petri Nets Theory and the Modelling of Systems. Prentice-Hall, 1981
[91] Pamela Zave and Michael Jackson. Where Do Operations Come From? A Multiparadigm Specification Technique. IEEE Transactions on Software Engineering, 1996, 22(7):508-528
[92] Debra J. Richardson, Stephanie Leif-Aha, and T. Owen OMalley. Specificationbased Test Oracles for Reactive Systems. In Proceedings of the 14th International Conference on Software Engineering, May 1992, pages 105-118
[93] Comp.realtime: Frequently Asked Questions (FAQs). (version 3.5) http://www.faqs.org/faqs/realtime-computing/faq/index.html
[94] Xin Wang, Ji Wang and Zhi-chang Qi, Automatic Generation of Run-Time Test Oracles for Distributed Real-Time Systems, 24th IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems FORTE 2004, Madrid, Spain, LNCS 3235, Springer-Verlag, September, 2004, pp. 199-212
[95] 姬孟洛,李军,王馨等,实时系统,高等教育出版社,2003,第22页至27页
[96] Languages and methods for specifying real-time systems, Jan Carlson, MRTC report, Malardalen Real-Time Research Centre, Malardalen University, August, 2002
[97] Hans van Vliet. Software Engineering: Principles and Practice.John Wiley & Sons, Chichester, 1993
[98] B. Randell, The Origin of Digital Computer, Springer-Verlag, 1973
[99] R. Floyd, Assigning Meanings to Programs, In. Mathematical Aspects of Computer Science, Proc. Symp. Appl. Maths., Vol 19, American Mathematical Society, 1967, pp. 19-32
[100] C.A.R. Hoare, An Axiomatic Basis for Computer Programming, Comm. ACM, Vol. 12??No. 12, Oct. 1969,pp.576-583
[101] P. Naur, Proofs of Algorithms by General Snapshots, BIT Vol. 6, 1969, pp.310-316
[102] E.W. Dijkstra, Guarded commands, nondeterminacy and the formal derivation of programs, Comm. ACM Vol. 18, August 1975, pp. 453-457
[103] D.L. Parnas, A Technique for Software Module Specification With Examples, Comm. ACM Vol. 15, May 1972
[104] B.H. Liskov and S.N. Zilles, Specification Techniques for Data Abstractions, IEEE Transactions on Software Engineering, Vol. 1, No. 1, March 1975, pp. 7-18
[105] J.M. Wing, A Specifier's Introduction to Formal Methods, IEEE Computer, Vol. 23, No. 9, September 1990
[106] D. Craigen, S. Gerhart and T. Ralston, An International Survey of Industrial Applications of Formal Methods, US Dept. Commerce, NIST, Computer System Lab., NISTGCR 93/626, March 1993
[107] M.G Hinchey and J.P. Bowen(eds.), Applications of Formal Methods, Prentice Hall, 1995
[108] E.M. Clarke, J.M. Wing et al, Formal Methods: State of the Art and Future Directions, ACM Computing Surveys, Vol. 28, No. 4, December 1996, pp. 626-643
[109] J.M. Wing, J. Woodcock and J. Davies(eds.), FM-99-World Conference on Formal Methods in the Development of Computing Systems, LNCS 1708 and 1709, Springer-Verlag, 1999
[110] Science of Computer Programming, Special Issue on Formal Methods in Industry, Vol. 36, No. 1, January 2000
[111] Jeannette M Wing, Writing Larch interface language specification, ACM Transactions on Programming Languages and Systems, 1987, 9(1): 1-24
[112] E.M. Clarke, E.A. Emerson and A.P. Sistla, Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM Trans. Program. Lang. Syst. 8, 2, Apr. 1986,244-263
[113] C. Stirling, Comparing linear and branching time temporal logics. In Proceedings of the International Conference on Temporal Logic in Specification, B. Banieqbal, H. Barringer, and A. Pnueli, Eds. Springer Lecture Notes in Computer Science Springer-Verlag, New York, NY, 1-20
[114] R. Razouk, and M. Gorlick, Real-time interval logic for reasoning about executions of real-time programs, SIGSOFT Softw. Eng. Notes 14, 8 (Dec. 1989), 10-19
[115] J.S. Ostroff, Temporal Logic for Real-Time Systems, Research Studies Press LTD., Advanced Software Development Series, Taunton, Somerset, England, 1989
[116] A. Morzenti and P. San Pierto, Object-Oriented Logical Specification of Time Critical Systems, ACM Transaction on Software Engineering and Methodology, Vol. 3, No. 1, Jan. 1994, pp. 56-98
[117] X. Nicollin and J. Sifakis, An overview and synthesis on timed process algebras, In K. Larsen and A. Skou, editors, Proc. CAV'91 3rd InternationalWorkshop Computer Aided Verification, Alborg, Denmark(LNCS 575), Springer Verlag, July 1991, pages 376-398
[118] J.R. Buchi, On a decision method in restricted second order arithmetic, In Proc.??International Conference Logic, Method and Philos. Sci. 1960, Stanford, 1962. Stanford University Press, pages 1-12
[119] Matthew B. Dwyer, George S. Avrunin and James C. Corbett, Property Specification Patterns for Finite-state Verification, In the 2nd Workshop on Formal Methods in Software Practice, March, 1998
[120] Matthew B. Dwyer, George S. Avrunin and James C. Corbett, Patterns in Property Specifications for Finite-state Verification, In the Proceedings of the 21st International Conference on Software Engineering, May, 1999
[121] P. Puschner and A. Burns. Guest Editorial, A Review of Worst-Case Execution-Time Analysis, Real-Tim Systems, 18(2-3), May 2000, pp,115-128
[122] Jakob Engblom, Processor Pipelines and Static Worst-Case Execution Time Analysis, PhD thesis, Acta Universitatis Upsaliensis, Uppsala, Sweden, 2002
[123] Alfred V. Aho, Ravi Sethi, and Jeffrey D. Ullman, Compilers, Principles, Techniques, and Tools, Addison-Wesley, June 1997
[124] F. Jahanian, R. Rajkumar, and S. C. V. Raju, Runtime Monitoring of Timing Constraints in Distributed Real-Time Systems, Real-Time Systems, Vol. 7, No. 3, 1994, pp. 247-273
[125] A.C. Liu and R. Parthasarathi, Hardware Monitoring of a Multiprocessor System, IEEE Micro, Vol.9, No.5, Oct. 1989, pp.44-51
[126] J.J.P. Tsai, K.Y. Fang, and H.Y. Chen, A Noninvasive Architecture to Monitor Real-Time Distributed Systems, Computer, Vol.23, No.3, Mar. 1990, pp. 11-23
[127] W.C. Brantley, K.P. McAuliffe, and T.A. Ngo, RP3 Performance Monitoring Hardware, in Instrumentation for Future Parallel Computing Systems, M. Simmons, R. Koskela, and I. Bucher, eds., ACM Press, New York, 1989, pp.35-47
[128] P.S. Dodd and C.V. Ravishankar, Monitoring and Debugging Distributed Real-Time Programs, Software-Practice and Experience, Vol.22, No. 10, Oct. 1992, pp.863-877
[129] J. Joyce, G. Lomow, K. Slind, and B. Unger, Monitoring Distributed Systems, ACM Trans. Computer Systems, Vol.5, No.2, May 1987, pp.121-150
[130] H. Tokuda, M. Kotera, and C.W. Mercer, A Real-Time Monitor for a Distributed Real-Time Operating System, Proc. ACM Workshop Parallel and Distributed Debugging, 1988,pp.68-77
[131] Dennis K. Peters, and David Lorge Parnas, Requirements-based Monitors for Real-Time Systems, in IEEE Transactions on Software Engineering, Vol. 28, No. 2, February 2002, pp. 146-158
[132] F. Jahanian, Run-time monitoring of real-time systems, in Advances in Real-time Systems, Prentice-Hall, 1995, edited by S.H. Son, pp.435-460
[133] Erik Yu-Shing Hu, Guillem Bernat and Andy Wellings, Addressing Dynamic Dispatching Issues in WCET Analysis for Object-Oriented Hard Real-Time Systems, Proceedings of the 5th IEEE International Symposium on Object-Oriented Real-Time Distributed Computing, Washington D.C., USA, April 2002, pp. 109-116
[134] Jakob Engblom and Bengt Jonsson, Processor pipelines and their properties for static wcet analysis, In Proc. 2nd Embedded Software Conference: Alberto L.??Sangiovanni-Vincentelli, Joseph Sifakis (Eds.), Embedded Software, Grenoble, France: LNCS 2491 Springer Verlag, Oct. 2002, pp. 334-348
[135] Christopher A. Healy, Robert D. Arnold, Frank Mueller, David Whalley, and Marion G. Harmon, Bounding Pipeline and Instruction Cache Performance, IEEE Transactions on Computers, 48(1), Jan. 1999
[136] Christopher A. Healy, Robert D. Arnold, Frank Mueller, David Whalley, and Marion G. Harmon, Bounding Pipeline and Instruction Cache Performance, IEEE Transactions on Computers, 48(1), Jan. 1999
[137] Alan C. Shaw, Reasoning about time in higher level language software, IEEE Transactions on Software Engineering, 15(7), Jul. 1989, pp. 875-889
[138] Sung-Soo Lim, Young H. Bae, Gyu T. Jang, Byung-Do Rhee, Sang L. Min, Chang Y. Park, Heonshik Shin, Kunsoo Park, Soo-Mook Moon, and Chong-Sang Kim, An accurate worst case timing analysis for RISC processors, IEEE Transactions on Software Engineering, 21(7), 1995, pp. 593-604
[139] Christopher A. Healy, Mikael Sj¨odin, and David B. Whalley, Bounding Loop Iterations for Timing Analysis, In Proc. IEEE Real-Time Technology and Aplications Symposium, Jun. 1998, pages 12-21
[140] Jan Gustafsson and Andreas Ermedahl, Automatic derivation of path and loop annotations in object-oriented real-time programs, Parallel and Distributed Computing Practices, 1(2), Jun. 1998
[141] R. Mattolini and P. Nesi, Using tilco for specifying realtime systems, In proceedings of the 2nd IEEE International Conference on Engineering of Complex Computer Systems, ICECCS'96, Montreal, Canada, October 1996
[142] Xin Wang, Zhi-Chang Qi and Shuhao Li, An Optimized Method for Automatic Test Oracle Generation from Real-Time Specification, In proceedings of the 10nd IEEE International Conference on Engineering of Complex Computer Systems, ICECCS'05, Shanghai, China, June 2005
[143] Digital Equipment Corporation, Digital Semiconductor Alpha 21064 and Alpha 21064A Microprocessors Hardware Reference Manual, 1996
[144] 贾永年，计算机在测控网中的应用，国防工业出版社，2000
[145] 姬孟洛，李军，王馨，齐治昌，一种基于抽象解释的自动WCET分析工具，计算机工程，录用待发表[1] The Committee on Information and Communications R&D (CIC) of the National Science, Technology Council (NSTC). America in the Age of Information: A Forum on Federal Information and Communications R&D. Bethesda, Maryland. July 6-7, 1995
[2] Committee on Computing, Information, and Communications, National Science and Technology Council Research Challenges in High Confidence Systems: Proceedings of the Committee on Computing, Information, and Communications Workshop. http://www.hpcc.gOv/pubs/hcs-Aug97/.August 6-7, 1997
[3] High Confidence Systems Working Group, Committee on Computing, Information, and Communications Research and Development, National Science and Technology Council. SETTING AN INTERAGENCY HIGH CONFIDENCE SYSTEMS (HCS) RESEARCH AGENDA: Proceedings of the Interagency High Confidence Systems Workshop. Hosted by the National Coordination Office for Computing, Information, and Communications. Arlington, Virginia. 25 March 1998
[4] High Confidence Software and Systems Coordinating Group, Interagency Working Group on Information Technology Research and Development. HIGH CONFIDENCE SOFTWARE AND SYSTEMS RESEARCH NEEDS, http://www.ccic.gov/pubs/hcss-research.pdf. January 10, 2001
[5] Ministry of Defence: "INT DEF STAN 00-55: The Procurement of Safety Critical Software in Defence Equipment - Issue 1", MoD, April 1991. http://wheelie.tees.ac.uk/hazop/standards/55/
[6] Department of Defense. MIL-STD-882B System Safety Program Requirements, July 1, 1987 NOTICE 1. http://neon.airtime.co.uk/users/wysywig/ 882b.htm
[7] Laplante, P.: Real-Time Systems Design and Analysis: An Engineer' s Handbook. Ieee Press, New York (1992)
[8] J.A.Stankovic: Misconceptions about real-time computing a serious problem for next generation systems. IEEE Computer 21(10) (1998) 10-19
[9] P. J. Pulli, P. Marko, and Heikkinen, Concurrent engineering for real-time systems. IEEE Software, November/December 1993, 10(6): p. 33-38
[10] A. Pnueli. Applications of temporal logic to the specification and verification of reactive systems: a survey of current trends, In Current Trends in Concurrency. Overviews and Tutorials, New York, Springer Lecture Notes in Computer Science, Springer-Verlag, 1986
[11] M. Falla, Advances in Safety Critical Systems: Results and Achievements from the DTI/EPSRC R&D Programe in Safety Critical Systems, Mike Falla, 1997. http://www.comp.lancs.ac.uk/computing/resources/scs/
[12] Richard N Taylor, Structural testing of concurrent programs. IEEE transaction on Software Engineering, March, 18 1992
[13] S. V. Campos, A Quantitative Approach to the Formal Verification of Real-time System, PhD thesis, Carnegie Mellon University, 1996[14] 郑人杰，计算机软件测试技术，清华大学出版社，1992
[15] ANSI/IEEE Std 829-1983, IEEE Standard for Software Test Documentation
[16] 朱鸿，金凌紫，软件质量保障与测试，科学出版社，1997
[17] L. Baresi and M. Young, Test Oracles, Technical Report, CIS-TR01-02, Dept. of Computer and Information Science, Univ. of Oregon, Aug. 2001.http://www.cs.uoregon.edu/-michal/pubs/oracles.html
[18] W. E. Howden and P. Eichhorst, Proving properties of programs from program traces, in Tutorial: Software Testing and Validation, ed by E. Miller and W. E. Howden in IEEE Computer Society: New York. p. 46-56, 1978
[19] L. J. White and E. I. Cohe, A domain strategy for computer program testing. IEEE Transaction on Software Engineering, SE-6: p. 247-257, 1990
[20] R. Alur and T. A. Henzinger. A really temporal logic, In Proceedings of the 30th IEEE Conference on Foundatiions of Computer Science, Los Alamitos, CA, IEEE Computer Society Press, 1989
[21] P. Bellini, R. Mattolini, and P. Nesi, Temporal logics for real-time system specification. ACM Computing Surveys, 32(1): p. 12-42, March 2000
[22] Alur, R.: Techniques of Automatic Verification of Real-Time Systems. PhD thesis, PhD thesis, Stanford University (1991 )
[23] R. Alur, T. Feder, and T. Henzinger. The benefits of relaxing punctuality. Journal of the ACM, 43(1):116{146, January 1996
[24] 《冯友兰学术精华录》，北京师范学院出版社，鲍霁主编，1988年，第119至125页
[25] 明，王夫之，《船山全书》第七册，岳麓出版社，第110页
[26] D. J. Panzl, Automatic Software Test Drivers. Computer, April 1978, 11(4): p. 44-50
[27] Richard G. Hamlet, Testing Programs with the Aid of a Compiler. IEEE Transactions on Software Engineering, July 1977, 3(4): p. 279-290
[28] D. Chapman, A Program Testing Assistant. Communications of the ACM, September 1982
[29] Elaine J. Weyuker, On testing non-testable programs. Computer Journal, 25, 1982: p. 465-470
[30] J. D. Day and J. D. Gannon. A test oracle based on formal specifications. In Proc. SoftFair, A Second Conf. on Software Development Tools, Techniques, and Alternatives, ACM Press, San Francisco, Dec 1985, pages 126-130
[31] Richard N. Taylor, An integrated verification and testing environment. Software-Practice and Experience, 1983, 13: p. 697-713
[32] D. C. Luckham and F. W. von Henke, Overview of Anna, a Specification Language for Ada. IEEE Software, March 1985, 2(2): p. 9-22
[33] D. C. Luckham, F. W. von Henke, B. Krieg-Bruckner, and O. Owe, Anna-A Language for Annotating Ada Programs. Lecture Notes in Computer Science, Springer-Verlag, 1987
[34] S. Sankar, D. Rosenblum, and R. Neff. An Implementation of Anna, In Proceedings of the Ada International Conference on Ada in Use, ACM, Cambridge University Press, May 1985
[35] David Luckham, Programming with Specifications: An Introduction to ANNA, A Language for Specifying Ada Programs. Springer-Verlag, 1990
[36] David S. Rosenblum. Towards a Method of Programming with Assertions, In Proceedings??of the 14th International Conference on Software Engineering, May 1992
[37] David S. Rosenblum, A Practical Approach to Programming With Assertions. IEEE Transactions on Software Engineering, 21(1): p. 19-31, January 1995
[38] R. Kramer. iContract - The Java Design by Contract Tool, In Proceedings of TOOLS26: Technology of Object-Oriented Languages and Systems, IEEE Computer Society, 1998.
[39] P.J. Maker, GNU Nana - User's Guide (version 2.4), Technical report, School of Information Technology - Northern Territory University, July 1998
[40] Jones, C.B., Systematic Software using VDM, 2nd ed., Prentice Hall, 1990.
[41] Bertrand Meyer, Eiffel: The Language. Object-Oriented Series, Prentice Hall, New York, 1992
[42] Bertrand Meyer, Object-Oriented Software Construction. Second Edition, The Object-Oriented Series, Prentice-Hall, 1997
[43] S. Sankar and R. Hayes, ADL: An Interface Definition Language for Specifying and Testing Software. ACM SIGPLAN Notices, August 1994, 29(8): p. 13-21
[44] Sun Microsystems, ADL language reference manual, 1993
[45] ADL Project, Future plans: Ad1 2, http://adl.xopen.org/future/
[46] S. R. Viswanadha and S. Sankar. Preliminary Design of ADL/C++ - A Specification Langauge for C++, In Proceedings of the 2nd Conference on Object-Oriented Technologies and Systems (COOTS), Toronto, Canada, June 1996
[47] M. Obayashi, H. Kubota, S.P. McCarron, and L. Mallet, The Assertion Based Testing Tool for OOP: ADL2. May 1998
[48] Dennis K. Peters and David L. Parnas, Using Test Oracles Generated from Program Documentation. IEEE Transactions on Software Engineering, 1998, 24(3): p. 161-173
[49] D.L. Parnas, J. Madey, and M. Iglewski, Precise Documentation of Well-Structured Programs. IEEE Transactions on Software Engineering, December 1994, 20(12): p. 948-976
[50] John D. Gannon, Paul McMullin, and Richard G Hamlet, Data-Abstraction mplementation, Specification, and Testing. ACM Transactions on Programming Languages and Systems, July 1981, 3(3): p. 211-223
[51] Victor R. Basili. The Design and Implementation of a Family of Application-Oriented Languages. In Proceedings of the 5th Texas Conference on Computing Systems, October 1976, pages 6-12
[52] Sergio Antoy and Richard G. Hamlet, Automatically Checking an Implementation against Its Formal Specification. IEEE Transactions on Software Engineering, January 2000, 26(1): p. 55-69
[53] S. Fujiwara, G. v. Bochmann, F. Khendek, M. Amalou, and A. Ghedamsi, Test Selection Based on Finite State Models. IEEE Transactions on Software Engineering, June 1991, 17(6): p. 591-603
[54] Atif M. Memon, Martha E. Pollack, and Mary Lou Soffa. Automated test oracles for GUIs. In Proceedings of the ACM SIGSOFT 8th International Symposium on the Foundations of Software Engineering (FSE-00), volume 25, 6 of ACM Software Engineering Notes. ACM Press, November 2000, pages 30-39
[55] James H. Andrews. Testing using log file analysis: Tools, methods, and issues, In??Proceedings of the 13th IEEE International Conference on Advanced Software Engineering, Honolulu, Hawaii, October 1998
[56] James H. Andrews and Yingjun Zhang. Broad-spectrum studies of log file analysis, In Proceedings of the 22nd International Conference on Software Engineering (ICSE 2000), Limerick, Ireland, ACM Press, June 2000
[57] Martin S. Feather, Rapid application of lightweight formal methods for consistency analysis. IEEE Transactions on Software Engineering, November 1998, 24(11): p. 949-959
[58] Martin S. Feather and Ben Smith, Automatic generation of test oracles - from pilot studies to application. Automated Software Engineering Journal, 2001, 8(1): p. 31-62
[59] John M. Spivey. The Z Notation: A Reference Manual. Prentice-Hall, 1989
[60] D. Carrington, D. Duke, R. Duke, P. King, G Rose, and G. Smith. Object-Z: An object-oriented extension to Z. In Formal Description Techniques (FORTE '89), North-Holland Publishing Co., December 1989 , pages 281-296
[61] E. Mikk. Compilation of Z Specifications into C for Automatic Test Result Evaluation. In Proceedings of the 9th International Conference of Z Users, volume 967 of Lecture Notes in Computer Science, Springer-Verlag, 1995., pages 167-180
[62] J. McDonald, L. Murray, and P. Strooper. Translating Object-Z specifications to object-oriented test oracles. In Proceedings: 4th Asia-Pacific Software Engineering and International Computer Science Conference, IEEE Computer Society Press, 1997, pages 414-426
[63] J. McDonald and P. Strooper. Translating Object-Z specifications to passive test oracles. In Proceedings of the 2nd International Conference on Formal Engineering Methods (ICFEM98), IEEE Computer Society Press, 1998, pages 165-174
[64] Paul Stocks and David Carrington. A Framework for Specification-Based Testing. IEEE Transactions on Software Engineering, 1996, 22(11):777-793
[65] L.K. Dillon and Qing Yu. Oracles for Checking Temporal Properties of Concurrent Systems, In Proceedings of the ACM SIGSOFT '94 Symposium on the Foundations of Software Engineering, December 1994
[66] L.K. Dillon and Y.S. Ramakrishna. Generating Oracles from Your Favorite Temporal Logic Specifications, In Proceedings of the Fourth ACM SIGSOFT Symposium on the Foundations of Software Engineering, 21 ACM Press, October 1996
[67] Doron Drusinsky. The Temporal Rover and the ATG Rover, In SPIN Model Checking and Software Verification, Proc, 7th SPIN Workshop, Stanford, California, 1885 of Springer-Verlag Lecture Notes in Computer Science, Springer Verlag, 2000
[68] John Hakansson, Automated generation of test scripts from temporal logic specification, Master's thesis, Uppsala University, 2000
[69] A. Pnueli. The temporal logic of programs, In Proceedings of the 18th Annual Symposium on Foundations of Computer Science, Los Alamitos, CA IEEE Computer Society Press, 1977
[70] A. Pnueli, The temporal semantics of concurrent programs. Theor. Comput. Sci, 13, 1981
[71] A. Pnueli. Applications of temporal logic to the specification and verification of reactive systems: a survey of current trends, In Current Trends in Concurrency. Overviews and Tutorials, New York, Springer Lecture Notes in Computer Science, Springer-Verlag, 1986[72] L.K. Dillon, G. Kutty, L. E. Moser, P. M. Melliar-Smith, and Y. S. Ramakrishna. Graphical specification for concurrent software systems, In Proc. 14th IEEE Inter. Conf. Software Engineering, Melbourne, May 1992
[73] 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 Engineering and Methodology, 1994
[74] Pierre Wolper, The tableau method for temporal logic: An overview. Logique et Analyse, 1985,110-111: p.119-136
[75] Moshe Vardy and Pierre Wolper, Reasoning about infinite computations. Information and Computation, 115(1-37), 1994
[76] Rob Gerth, Doron Peled, Moshe Vardi, and Pierre Wolper. Simple on-the-fly automatic verification of linear temporal logic, In Protocol Specification Testing and Verification, Warsaw, Poland, Chapman & Hall, 1995
[77] Y. Kesten, Z. Manna, H. McGuire, and A. Pnueli, A decision algorithm for full prepositional temporal logic. In C. Courooubetis, ed., Proc. 1993 International Conference of Computer-Aided Verification, vol 697 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, 1993, pp. 97-109
[78] H. McGuire, Two Mehtods for Checking Formulas of Temporal Logic, PhD thesis, Dept. of Computer Science, Stanford University, Stanford, California, 1995
[79] Geilen, M.: On the construction of monitors for temporal logic properties. In: K. Havelund and G. Rosu, editors, Proceedings of RV'01 - First Workshop on Run-time Verification. Satellite Workshop of CAV'01, Electronic Notes in Theoretical Computer Science 55(2), Amsterdam, 2001. Elsevier Science, Paris, France (2001)
[80] Kupferman, O. and M. Y. Vardi, Model checking of safety properties, in: N. Halbwachs and D. Peled, editors, Computer Aided Verification: 11th International Conference Proceedings, CAV'99(LNCS 1633), Trento, Italy, July 6-10, 1999, pp. 172-183
[81] R. Koymans, Specifying real-time properties with metric temporal logic. Real-Time Systems, November 1990, 2(4): p. 255-299
[82] C. Ghezzi, D. Mandrioli, and A. Morzenti, TRIO: A logic language for executable specifications of real-time systems. Journal of Systems and software, 12(2): p. 107-123, May 1990
[83] M. Felder and A. Morzenti, Validating real-time systems by history-checking TRIO specifications. ACM Transaction on Software Engineering Methodology, 3(4): p. 308-339, October 1994
[84]M.C.W.Geilen, Formal Techniques for Verification of Complex Real-Time Systems, PhD Thesis, Eindhoven University of Technology, Netherlands, 2002, pp. 159-205
[85] Marius Mikucionis, Brian Nielsen and Kim G. Larsen, Real-time System Testing On-the-fly, The 15th Nordic Workshop on Programming Theory, Turku, Finland, October 29-31, 2003
[86] Wang Yi, Paul Pettersson and Mats Daniels, Automatic Verification of Real-Time Communicating Systems by Constraint Solving, In Proceedings of the 7th International Conference on Formal Description Techniques, North-Holland, 1994, pp. 223-238
[87] K. L. Heninger, J. Kallander, D. L. Parnas, and J. E. Shore, Software Requirements for the??A-7E Aircraft, NRL Memorandum Report 3876, United States Naval Research Laboratory, November 1978
[88] Angelo Gargantini and Connie Heitmeyer. Using Model Checking to Generate Tests from Requirements Specifications. In Proceedings of the 7th European Engineering Conference and the 7th ACM SIGSOFT Symposium on the Foundations of Software Engeneering, volume 24.6 of Software Engineering Notes (SEN), ACM Press, September 6-10 1999, pages 146-162
[89] Jin-Cherng Lin and Ian Ho, Generating timed test cases with oracles for real-time software. Advances in Engineering Software, 2001, 32(9): p. 705-715
[90] J. L. Peterson. Petri Nets Theory and the Modelling of Systems. Prentice-Hall, 1981
[91] Pamela Zave and Michael Jackson. Where Do Operations Come From? A Multiparadigm Specification Technique. IEEE Transactions on Software Engineering, 1996, 22(7):508-528
[92] Debra J. Richardson, Stephanie Leif-Aha, and T. Owen OMalley. Specificationbased Test Oracles for Reactive Systems. In Proceedings of the 14th International Conference on Software Engineering, May 1992, pages 105-118
[93] Comp.realtime: Frequently Asked Questions (FAQs). (version 3.5) http://www.faqs.org/faqs/realtime-computing/faq/index.html
[94] Xin Wang, Ji Wang and Zhi-chang Qi, Automatic Generation of Run-Time Test Oracles for Distributed Real-Time Systems, 24th IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems FORTE 2004, Madrid, Spain, LNCS 3235, Springer-Verlag, September, 2004, pp. 199-212
[95] 姬孟洛，李军，王馨等，实时系统，高等教育出版社，2003，第22页至27页
[96] Languages and methods for specifying real-time systems, Jan Carlson, MRTC report, Malardalen Real-Time Research Centre, Malardalen University, August, 2002
[97] Hans van Vliet. Software Engineering: Principles and Practice. John Wiley & Sons, Chichester, 1993
[98] B. Randell, The Origin of Digital Computer, Springer-Verlag, 1973
[99] R. Floyd, Assigning Meanings to Programs, In. Mathematical Aspects of Computer Science, Proc. Symp. Appl. Maths., Vol 19, American Mathematical Society, 1967, pp. 19-32
[100] C. A. R. Hoare, An Axiomatic Basis for Computer Programming, Comm. ACM, Vol. 12 No.12, Oct. 1969, pp.576-583
[101] P. Naur, Proofs of Algorithms by General Snapshots, BIT Vol. 6, 1969, pp.310-316
[102] E. W. Dijkstra, Guarded commands, nondeterminacy and the formal derivation of programs, Comm. ACM Vol. 18, August 1975, pp. 453-457
[103] D. L. Parnas, A Technique for Software Module Specification With Examples, Comm. ACM Vol. 15, May 1972
[104] B.H. Liskov and S.N. Zilles, Specification Techniques for Data Abstractions, IEEE Transactions on Software Engineering, Vol. 1, No. 1, March 1975, pp. 7-18
[105] J. M. Wing, A Specifier's Introduction to Formal Methods, IEEE Computer, Vol. 23, No. 9, September 1990
[106] D. Craigen, S. Gerhart and T. Ralston, An International Survey of Industrial Applications of Formal Methods, US Dept. Commerce, NIST. Computer System Lab., NISTGCR 93/626, March 1993[107] M.G. Hinchey and J.P. Bowen(eds.), Applications of Formal Methods, Prentice Hall, 1995
[108] E.M. Clarke, J.M. Wing et al, Formal Methods: State of the Art and Future Directions, ACM Computing Surveys, Vol. 28, No. 4, December 1996, pp. 626-643
[109] J.M. Wing, J. Woodcock and J. Davies(eds.), FM-99-World Conference on Formal Methods in the Development of Computing Systems, LNCS 1708 and 1709, Springer-Verlag, 1999
[110] Science of Computer Programming, Special Issue on Formal Methods in Industry, Vol. 36, No. 1, January 2000
[111] Jeannette M Wing, Writing Larch interface language specification, ACM Transactions on Programming Languages and Systems, 1987, 9(1): 1-24
[112] E.M. Clarke, E.A. Emerson and A.P. Sistla, Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM Trans. Program. Lang. Syst. 8, 2, Apr. 1986,244-263
[113] C. Stirling, Comparing linear and branching time temporal logics. In Proceedings of the International Conference on Temporal Logic in Specification, B. Banieqbal, H. Barringer, and A. Pnueli, Eds. Springer Lecture Notes in Computer Science Springer-Verlag, New York, NY, 1-20
[114] R. Razouk, and M. Gorlick, Real-time interval logic for reasoning about executions of real-time programs, SIGSOFT Softw. Eng. Notes 14, 8 (Dec. 1989), 10-19
[115] J.S. Ostroff, Temporal Logic for Real-Time Systems, Research Studies Press LTD., Advanced Software Development Series, Taunton, Somerset, England, 1989
[116] A. Morzenti and P. San Pierto, Object-Oriented Logical Specification of Time Critical Systems, ACM Transaction on Software Engineering and Methodology, Vol. 3, No. 1, Jan. 1994, pp. 56-98
[117] X. Nicollin and J. Sifakis, An overview and synthesis on timed process algebras, In K. Larsen and A. Skou, editors, Proc. CAV'91 3rd InternationalWorkshop Computer Aided Verification, Alborg, Denmark(LNCS 575), Springer Verlag, July 1991, pages 376-398
[118] J.R. Buchi, On a decision method in restricted second order arithmetic, In Proc. International Conference Logic, Method and Philos. Sci. 1960, Stanford, 1962. Stanford University Press, pages 1-12
[119]Matthew B. Dwyer, George S. Avrunin and James C. Corbett, Property Specification Patterns for Finite-state Verification, In the 2nd Workshop on Formal Methods in Software Practice, March, 1998
[120]Matthew B. Dwyer, George S. Avrunin and James C. Corbett, Patterns in Property Specifications for Finite-state Verification, In the Proceedings of the 21st International Conference on Software Engineering, May, 1999
[121] P. Puschner and A. Burns. Guest Editorial, A Review of Worst-Case Execution-Time Analysis, Real-Tim Systems, 18(2-3), May 2000, pp,115-128
[122] Jakob Engblom, Processor Pipelines and Static Worst-Case Execution Time Analysis, PhD thesis, Acta Universitatis Upsaliensis, Uppsala, Sweden, 2002
[123] Alfred V. Aho, Ravi Sethi, and Jeffrey D. Ullman, Compilers, Principles, Techniques, and Tools, Addison-Wesley, June 1997
[124] F. Jahanian, R. Rajkumar, and S. C. V. Raju, Runtime Monitoring of Timing Constraints in??Distributed Real-Time Systems, Real-Time Systems, Vol. 7, No. 3,1994, pp. 247-273
[125] A.C. Liu and R. Parthasarathi, Hardware Monitoring of a Multiprocessor System, IEEE Micro, Vol.9, No.5, Oct. 1989, pp.44-51
[126] J.J.P. Tsai, K.Y. Fang, and H.Y. Chen, A Noninvasive Architecture to Monitor Real-Time Distributed Systems, Computer, Vol.23, No.3, Mar. 1990, pp. 11-23
[127] W.C. Brantley, K.P. McAuliffe, and T.A. Ngo, RP3 Performance Monitoring Hardware, in Instrumentation for Future Parallel Computing Systems, M. Simmons, R. Koskela, and I. Bucher, eds., ACM Press, New York, 1989, pp.35-47
[128] P.S. Dodd and C.V. Ravishankar, Monitoring and Debugging Distributed Real-Time Programs, Software-Practice and Experience, Vol.22, No.10, Oct. 1992, pp.863-877
[129] J. Joyce, G. Lomow, K. Slind, and B. Unger, Monitoring Distributed Systems, ACM Trans. Computer Systems, Vol.5, No.2, May 1987, pp.121-150
[130] H. Tokuda, M. Kotera, and C.W. Mercer, A Real-Time Monitor for a Distributed Real-Time Operating System, Proc. ACM Workshop Parallel and Distributed Debugging, 1988, pp.68-77
[131] Dennis K. Peters, and David Lorge Parnas, Requirements-based Monitors for Real-Time Systems, in IEEE Transactions on Software Engineering, Vol. 28, No. 2, February 2002, pp. 146-158
[132] F. Jahanian, Run-time monitoring of real-time systems, in Advances in Real-time Systems, Prentice-Hall, 1995, edited by S.H. Son, pp.435-460
[133] Erik Yu-Shing Hu, Guillem Bernat and Andy Wellings, Addressing Dynamic Dispatching Issues in WCET Analysis for Object-Oriented Hard Real-Time Systems, Proceedings of the 5th IEEE International Symposium on Object-Oriented Real-Time Distributed Computing, Washington D.C., USA, April 2002, pp. 109-116
[134] Jakob Engblom and Bengt Jonsson, Processor pipelines and their properties for static wcet analysis, In Proc. 2nd Embedded Software Conference: Alberto L. Sangiovanni-Vincentelli, Joseph Sifakis (Eds.), Embedded Software, Grenoble, France: LNCS 2491 Springer Verlag, Oct. 2002, pp. 334-348
[135] Christopher A. Healy, Robert D. Arnold, Frank Mueller, David Whalley, and Marion G. Harmon, Bounding Pipeline and Instruction Cache Performance, IEEE Transactions on Computers, 48(1), Jan. 1999
[136] Christopher A. Healy, Robert D. Arnold, Frank Mueller, David Whalley, and Marion G. Harmon, Bounding Pipeline and Instruction Cache Performance, IEEE Transactions on Computers, 48(1), Jan. 1999
[137] Alan C. Shaw, Reasoning about time in higher level language software, IEEE Transactions on Software Engineering, 15(7), Jul. 1989, pp. 875-889
[138] Sung-Soo Lim, Young H. Bae, Gyu T. Jang, Byung-Do Rhee, Sang L. Min, Chang Y. Park, Heonshik Shin, Kunsoo Park, Soo-Mook Moon, and Chong-Sang Kim, An accurate worst case timing analysis for RISC processors, IEEE Transactions on Software Engineering, 21(7), 1995, pp. 593-604
[139] Christopher A. Healy, Mikael Sjodin, and David B. Whalley, Bounding Loop Iterations for Timing Analysis, In Proc. IEEE Real-Time Technology and Aplications Symposium, Jun.??1998, pages 12-21
[140] Jan Gustafsson and Andreas Ermedahl, Automatic derivation of path and loop annotations in object-oriented real-time programs, Parallel and Distributed Computing Practices, 1 (2), Jun. 1998
[141] R. Mattolini and P. Nesi, Using tilco for specifying realtime systems, In proceedings of the 2nd IEEE International Conference on Engineering of Complex Computer Systems, ICECCS'96, Montreal, Canada, October 1996
[142] Xin Wang, Zhi-Chang Qi and Shuhao Li, An Optimized Method for Automatic Test Oracle Generation from Real-Time Specification, In proceedings of the 10nd IEEE International Conference on Engineering of Complex Computer Systems, ICECCS'05, Shanghai, China, June 2005
[143] Digital Equipment Corporation, Digital Semiconductor Alpha 21064 and Alpha 21064A Microprocessors Hardware Reference Manual, 1996
[144] 贾永年，计算机在测控网中的应用，国防工业出版社，2000
[145] 姬孟洛，李军，王馨，齐治昌，一种基于抽象解释的自动WCET分析工具，计算机工程，录用待发表
[2] Committee on Computing, Information, and Communications, National Science and Technology Council Research Challenges in High Confidence Systems: Proceedings of the Committee on Computing, Information, and Communications Workshop, August 6-7, 1997, http://www.nitrd.gov/pubs/hcs-Aug97/
[3] High Confidence Systems Working Group, Committee on Computing, Information, and Communications Research and Development, National Science and Technology Council. SETTING AN INTERAGENCY HIGH CONFIDENCE SYSTEMS (HCS) RESEARCH AGENDA: Proceedings of the Interagency High Confidence Systems Workshop. Hosted by the National Coordination Office for Computing, Information, and Communications. Arlington, Virginia. 25 March 1998
[4] High Confidence Software and Systems Coordinating Group, Interagency Working Group on Information Technology Research and Development. HIGH CONFIDENCE SOFTWARE AND SYSTEMS RESEARCH NEEDS, 10, January 2001, http://www.nitrd.gov/pubs/hcss-research.pdf
[5] Ministry of Defence: "INT DEF STAN 00-55: The Procurement of Safety Critical Software in Defence Equipment - Issue 1", MoD, April 1991.
[6] Department of Defense. MIL-STD-882B System Safety Program Requirements, July 1, 1987 NOTICE 1. http://sparc.airtime.co.uk/users/wysywig/882b.htm
[7] Laplante, P.: Real-Time Systems Design and Analysis: An Engineer' s Handbook. Ieee Press, New York (1992)
[8] J.A.Stankovic: Misconceptions about real-time computing a serious problem for next generation systems. IEEE Computer 21(10) (1998) 10-19
[9] P. J. Pulli, P. Marko, and Heikkinen, Concurrent engineering for real-time systems. IEEE Software, November/December 1993,10(6): p. 33-38
[10] A. Pnueli. Applications of temporal logic to the specification and verification of reactive systems: a survey of current trends, In Current Trends in Concurrency. Overviews and Tutorials, New York, Springer Lecture Notes in Computer Science, Springer-Verlag, 1986
[11] M. Falla, Advances in Safety Critical Systems: Results and Achievements from the DTI/EPSRC R&D Programe in Safety Critical Systems, Mike Falla, 1997. http://www.comp.lancs.ac.uk/computing/resources/scs/
[12] Richard N Taylor, Structural testing of concurrent programs. IEEE transaction on Software Engineering, March, 18 1992
[13] S. V. Campos, A Quantitative Approach to the Formal Verification of Real-time System, PhD thesis, Carnegie Mellon University, 1996[14] 郑人杰，计算机软件测试技术，清华大学出版社，1992
[15] ANSI/IEEE Std 829-1983, IEEE Standard for Software Test Documentation
[16] 朱鸿，金凌紫，软件质量保障与测试，科学出版社，1997
[17] L. Baresi and M. Young, Test Oracles, Technical Report, CIS-TR01-02, Dept. of Computer and Information Science, Univ. of Oregon, Aug. 2001. http://www.cs.uoregon.edu/-michal/pubs/oracles.html
[18] W. E. Howden and P. Eichhorst, Proving properties of programs from program traces, in Tutorial: Software Testing and Validation, ed by E. Miller and W. E. Howden in IEEE Computer Society: New York. p. 46-56, 1978
[19] L. J. White and E. I. Cohe, A domain strategy for computer program testing. IEEE Transaction on Software Engineering, SE-6: p. 247-257, 1990
[20] R. Alur and T. A. Henzinger. A really temporal logic, In Proceedings of the 30th IEEE Conference on Foundatiions of Computer Science, Los Alamitos, CA, IEEE Computer Society Press, 1989
[21] P. Bellini, R. Mattolini, and P. Nesi, Temporal logics for real-time system specification. ACM Computing Surveys, 32(1): p. 12-42, March 2000
[22] Alur, R.: Techniques of Automatic Verification of Real-Time Systems. PhD thesis, PhD thesis, Stanford University (1991)
[23] R. Alur, T. Feder, and T. Henzinger. The benefits of relaxing punctuality. Journal of the ACM, 43(1): 116{146, January 1996
[24] 《冯友兰学术精华录》，北京师范学院出版社，鲍霁主编，1988年，第119至125页
[25] 明，王夫之，《船山全书》第七册，岳麓出版社，第110页
[26] D. J. Panzl, Automatic Software Test Drivers. Computer, April 1978, 11(4): p. 44-50
[27] Richard G. Hamlet, Testing Programs with the Aid of a Compiler. IEEE Transactions on Software Engineering, July 1977, 3(4): p. 279-290
[28] D. Chapman, A Program Testing Assistant. Communications of the ACM, September 1982
[29] Elaine J. Weyuker, On testing non-testable programs. Computer Journal, 25, 1982: p. 465-470
[30] J. D. Day and J. D. Gannon. A test oracle based on formal specifications. In Proc. SoftFair, A Second Conf. on Software Development Tools, Techniques, and Alternatives, ACM Press, San Francisco, Dec 1985, pages 126-130
[31] Richard N. Taylor, An integrated verification and testing environment. Software-Practice and Experience, 1983, 13: p. 697-713
[32] D.C. Luckham and F.W. von Henke, Overview of Anna, a Specification Language for Ada. IEEE Software, March 1985, 2(2): p. 9-22
[33] D. C. Luckham, F. W. von Henke, B. Krieg-Bruckner, and O. Owe, Anna-A Language for Annotating Ada Programs. Lecture Notes in Computer Science, Springer-Verlag, 1987
[34] S. Sankar, D. Rosenblum, and R. Neff. An Implementation of Anna, In Proceedings of the Ada International Conference on Ada in Use, ACM, Cambridge University Press, May 1985[35] David Luckham, Programming with Specifications: An Introduction to ANNA, A Language for Specifying Ada Programs. Springer-Verlag, 1990
[36] David S. Rosenblum. Towards a Method of Programming with Assertions, In Proceedings of the 14th International Conference on Software Engineering, May 1992
[37] David S. Rosenblum, A Practical Approach to Programming With Assertions. IEEE Transactions on Software Engineering, 21(1): p. 19-31, January 1995
[38] R. Kramer. iContract - The Java Design by Contract Tool, In Proceedings of TOOLS26: Technology of Object-Oriented Languages and Systems, IEEE Computer Society, 1998.
[39] P.J. Maker, GNU Nana - User's Guide (version 2.4), Technical report, School of Information Technology - Northern Territory University, July 1998
[40] Jones, C.B., Systematic Software using VDM, 2nd ed., Prentice Hall, 1990.
[41] Bertrand Meyer, Eiffel: The Language. Object-Oriented Series, Prentice Hall, New York, 1992
[42] Bertrand Meyer, Object-Oriented Software Construction. Second Edition, The Object-Oriented Series, Prentice-Hall, 1997
[43] S. Sankar and R. Hayes, ADL: An Interface Definition Language for Specifying and Testing Software. ACM SIGPLAN Notices, August 1994, 29(8): p. 13-21
[44] Sun Microsystems, ADL language reference manual, 1993
[45] ADL Project, Ad1 2, http://adl.opengroup.org/exgr/
[46] S. R. Viswanadha and S. Sankar. Preliminary Design of ADL/C++ - A Specification Langauge for C++, In Proceedings of the 2nd Conference on Object-Oriented Technologies and Systems (COOTS), Toronto, Canada, June 1996
[47] M. Obayashi, H. Kubota, S.P. McCarron, and L. Mallet, The Assertion Based Testing Tool for OOP: ADL2. May 1998
[48] Dennis K. Peters and David L. Parnas, Using Test Oracles Generated from Program Documentation. IEEE Transactions on Software Engineering, 1998, 24(3): p. 161-173
[49] D.L. Parnas, J. Madey, and M. Iglewski, Precise Documentation of Well-Structured Programs. IEEE Transactions on Software Engineering, December 1994, 20(12): p. 948-976
[50] John D. Gannon, Paul McMullin, and Richard G Hamlet, Data-Abstraction mplementation, Specification, and Testing. ACM Transactions on Programming Languages and Systems, July 1981, 3(3): p. 211-223
[51] Victor R. Basili. The Design and Implementation of a Family of Application-Oriented Languages. In Proceedings of the 5th Texas Conference on Computing Systems, October 1976, pages 6-12
[52] Sergio Antoy and Richard G. Hamlet, Automatically Checking an Implementation against Its Formal Specification. IEEE Transactions on Software Engineering, January 2000, 26(1): p. 55-69
[53] S. Fujiwara, G. v. Bochmann, F. Khendek, M. Amalou, and A. Ghedamsi, Test Selection Based on Finite State Models. IEEE Transactions on Software Engineering, June 1991, 17(6): p. 591-603[54] Atif M. Memon, Martha E. Pollack, and Mary Lou Soffa. Automated test oracles for GUIs. In Proceedings of the ACM SIGSOFT 8th International Symposium on the Foundations of Software Engineering (FSE-00), volume 25, 6 of ACM Software Engineering Notes. ACM Press, November 2000, pages 30-39
[55] James H. Andrews. Testing using log file analysis: Tools, methods, and issues, In Proceedings of the 13 th IEEE International Conference on Advanced Software Engineering, Honolulu, Hawaii, October 1998
[56] James H. Andrews and Yingjun Zhang. Broad-spectrum studies of log file analysis, In Proceedings of the 22nd International Conference on Software Engineering (ICSE 2000), Limerick, Ireland, ACM Press, June 2000
[57] Martin S. Feather, Rapid application of lightweight formal methods for consistency analysis. IEEE Transactions on Software Engineering, November 1998, 24(11): p. 949-959
[58] Martin S. Feather and Ben Smith, Automatic generation of test oracles - from pilot studies to application. Automated Software Engineering Journal, 2001, 8(1): p. 31-62
[59] John M. Spivey. The Z Notation: A Reference Manual. Prentice-Hall, 1989
[60] D. Carrington, D. Duke, R. Duke, P. King, G. Rose, and G Smith. Object-Z: An object-oriented extension to Z. In Formal Description Techniques (FORTE '89), North-Holland Publishing Co., December 1989 , pages 281-296
[61] E. Mikk. Compilation of Z Specifications into C for Automatic Test Result Evaluation. In Proceedings of the 9th International Conference of Z Users, volume 967 of Lecture Notes in Computer Science, Springer-Verlag, 1995., pages 167-180
[62] J. McDonald, L. Murray, and P. Strooper. Translating Object-Z specifications to object-oriented test oracles. In Proceedings: 4th Asia-Pacific Software Engineering and International Computer Science Conference, IEEE Computer Society Press, 1997, pages 414-426
[63] J. McDonald and P. Strooper. Translating Object-Z specifications to passive test oracles. In Proceedings of the 2nd International Conference on Formal Engineering Methods (ICFEM98), IEEE Computer Society Press, 1998, pages 165-174
[64] Paul Stocks and David Carrington. A Framework for Specification-Based Testing. IEEE Transactions on Software Engineering, 1996, 22(11):777-793
[65] L.K. Dillon and Qing Yu. Oracles for Checking Temporal Properties of Concurrent Systems, In Proceedings of the ACM SIGSOFT '94 Symposium on the Foundations of Software Engineering, December 1994
[66] L.K. Dillon and Y.S. Ramakrishna. Generating Oracles from Your Favorite Temporal Logic Specifications, In Proceedings of the Fourth ACM SIGSOFT Symposium on the Foundations of Software Engineering, 21 ACM Press, October 1996
[67] Doron Drusinsky. The Temporal Rover and the ATG Rover, In SPIN Model Checking and Software Verification, Proc, 7th SPIN Workshop, Stanford, California, 1885 of Springer-Verlag Lecture Notes in Computer Science, Springer Verlag, 2000
[68] John Hakansson, Automated generation of test scripts from temporal logic specification, Master's thesis, Uppsala University, 2000[69] A. Pnueli. The temporal logic of programs, In Proceedings of the 18th Annual Symposium on Foundations of Computer Science, Los Alamitos, CA IEEE Computer Society Press, 1977
[70] A. Pnueli, The temporal semantics of concurrent programs. Theor. Comput. Sci, 13, 1981
[71] A. Pnueli. Applications of temporal logic to the specification and verification of reactive systems: a survey of current trends, In Current Trends in Concurrency. Overviews and Tutorials, New York, Springer Lecture Notes in Computer Science, Springer-Verlag, 1986
[72] L.K. Dillon, G. Kutty, L. E. Moser, P. M. Melliar-Smith, and Y. S. Ramakrishna. Graphical specification for concurrent software systems, In Proc. 14th IEEE Inter. Conf. Software Engineering, Melbourne, May 1992
[73] 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 Engineering and Methodology, 1994
[74] Pierre Wolper, The tableau method for temporal logic: An overview. Logique et Analyse, 1985,110-111: p. 119-136
[75] Moshe Vardy and Pierre Wolper, Reasoning about infinite computations. Information and Computation, 115(1-37), 1994
[76] Rob Gerth, Doron Peled, Moshe Vardi, and Pierre Wolper. Simple on-the-fly automatic verification of linear temporal logic, In Protocol Specification Testing and Verification, Warsaw, Poland, Chapman & Hall, 1995
[77] Y. Kesten, Z. Manna, H. McGuire, and A. Pnueli, A decision algorithm for full prepositional temporal logic. In C. Courooubetis, ed., Proc. 1993 International Conference of Computer-Aided Verification, vol 697 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, 1993, pp. 97-109
[78] H. McGuire, Two Mehtods for Checking Formulas of Temporal Logic, PhD thesis, Dept. of Computer Science, Stanford University, Stanford, California, 1995
[79] Geilen, M.: On the construction of monitors for temporal logic properties. In: K. Havelund and G Rosu, editors, Proceedings of RV'01 - First Workshop on Run-time Verification. Satellite Workshop of CAV'01, Electronic Notes in Theoretical Computer Science 55(2), Amsterdam, 2001. Elsevier Science, Paris, France (2001)
[80] Kupferman, O. and M. Y. Vardi, Model checking of safety properties, in: N. Halbwachs and D. Peled, editors, Computer Aided Verification: 11th International Conference Proceedings, CAV'99(LNCS 1633), Trento, Italy, July 6-10, 1999, pp. 172-183
[81] R. Koymans, Specifying real-time properties with metric temporal logic. Real-Time Systems, November 1990, 2(4): p. 255-299
[82] C. Ghezzi, D. Mandrioli, and A. Morzenti, TRIO: A logic language for executable specifications of real-time systems. Journal of Systems and software, 12(2): p. 107-123, May 1990
[83] M. Felder and A. Morzenti, Validating real-time systems by history-checking TRIO specifications. ACM Transaction on Software Engineering Methodology, 3(4): p. 308-339, October 1994[84] M.C.W.Geilen, Formal Techniques for Verification of Complex Real-Time Systems, PhD Thesis, Eindhoven University of Technology, Netherlands, 2002, pp. 159-205
[85] Marius Mikucionis, Brian Nielsen and Kim G. Larsen, Real-time System Testing On-the-fly, The 15th Nordic Workshop on Programming Theory, Turku, Finland, October 29-31,2003
[86] Wang Yi, Paul Pettersson and Mats Daniels, Automatic Verification of Real-Time Communicating Systems by Constraint Solving, In Proceedings of the 7th International Conference on Formal Description Techniques, North-Holland, 1994, pp. 223-238
[87] K. L. Heninger, J. Kallander, D. L. Parnas, and J. E. Shore, Software Requirements for the A-7E Aircraft, NRL Memorandum Report 3876, United States Naval Research Laboratory, November 1978
[88] Angelo Gargantini and Connie Heitmeyer. Using Model Checking to Generate Tests from Requirements Specifications. In Proceedings of the 7th European Engineering Conference and the 7th ACM SIGSOFT Symposium on the Foundations of Software Engeneering, volume 24.6 of Software Engineering Notes (SEN), ACM Press, September 6-10 1999, pages 146-162
[89] Jin-Cherng Lin and Ian Ho, Generating timed test cases with oracles for real-time software. Advances in Engineering Software, 2001, 32(9): p. 705-715
[90] J. L. Peterson. Petri Nets Theory and the Modelling of Systems. Prentice-Hall, 1981
[91] Pamela Zave and Michael Jackson. Where Do Operations Come From? A Multiparadigm Specification Technique. IEEE Transactions on Software Engineering, 1996, 22(7):508-528
[92] Debra J. Richardson, Stephanie Leif-Aha, and T. Owen OMalley. Specificationbased Test Oracles for Reactive Systems. In Proceedings of the 14th International Conference on Software Engineering, May 1992, pages 105-118
[93] Comp.realtime: Frequently Asked Questions (FAQs). (version 3.5) http://www.faqs.org/faqs/realtime-computing/faq/index.html
[94] Xin Wang, Ji Wang and Zhi-chang Qi, Automatic Generation of Run-Time Test Oracles for Distributed Real-Time Systems, 24th IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems FORTE 2004, Madrid, Spain, LNCS 3235, Springer-Verlag, September, 2004, pp. 199-212
[95] 姬孟洛,李军,王馨等,实时系统,高等教育出版社,2003,第22页至27页
[96] Languages and methods for specifying real-time systems, Jan Carlson, MRTC report, Malardalen Real-Time Research Centre, Malardalen University, August, 2002
[97] Hans van Vliet. Software Engineering: Principles and Practice.John Wiley & Sons, Chichester, 1993
[98] B. Randell, The Origin of Digital Computer, Springer-Verlag, 1973
[99] R. Floyd, Assigning Meanings to Programs, In. Mathematical Aspects of Computer Science, Proc. Symp. Appl. Maths., Vol 19, American Mathematical Society, 1967, pp. 19-32
[100] C.A.R. Hoare, An Axiomatic Basis for Computer Programming, Comm. ACM, Vol. 12??No. 12, Oct. 1969,pp.576-583
[101] P. Naur, Proofs of Algorithms by General Snapshots, BIT Vol. 6, 1969, pp.310-316
[102] E.W. Dijkstra, Guarded commands, nondeterminacy and the formal derivation of programs, Comm. ACM Vol. 18, August 1975, pp. 453-457
[103] D.L. Parnas, A Technique for Software Module Specification With Examples, Comm. ACM Vol. 15, May 1972
[104] B.H. Liskov and S.N. Zilles, Specification Techniques for Data Abstractions, IEEE Transactions on Software Engineering, Vol. 1, No. 1, March 1975, pp. 7-18
[105] J.M. Wing, A Specifier's Introduction to Formal Methods, IEEE Computer, Vol. 23, No. 9, September 1990
[106] D. Craigen, S. Gerhart and T. Ralston, An International Survey of Industrial Applications of Formal Methods, US Dept. Commerce, NIST, Computer System Lab., NISTGCR 93/626, March 1993
[107] M.G Hinchey and J.P. Bowen(eds.), Applications of Formal Methods, Prentice Hall, 1995
[108] E.M. Clarke, J.M. Wing et al, Formal Methods: State of the Art and Future Directions, ACM Computing Surveys, Vol. 28, No. 4, December 1996, pp. 626-643
[109] J.M. Wing, J. Woodcock and J. Davies(eds.), FM-99-World Conference on Formal Methods in the Development of Computing Systems, LNCS 1708 and 1709, Springer-Verlag, 1999
[110] Science of Computer Programming, Special Issue on Formal Methods in Industry, Vol. 36, No. 1, January 2000
[111] Jeannette M Wing, Writing Larch interface language specification, ACM Transactions on Programming Languages and Systems, 1987, 9(1): 1-24
[112] E.M. Clarke, E.A. Emerson and A.P. Sistla, Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM Trans. Program. Lang. Syst. 8, 2, Apr. 1986,244-263
[113] C. Stirling, Comparing linear and branching time temporal logics. In Proceedings of the International Conference on Temporal Logic in Specification, B. Banieqbal, H. Barringer, and A. Pnueli, Eds. Springer Lecture Notes in Computer Science Springer-Verlag, New York, NY, 1-20
[114] R. Razouk, and M. Gorlick, Real-time interval logic for reasoning about executions of real-time programs, SIGSOFT Softw. Eng. Notes 14, 8 (Dec. 1989), 10-19
[115] J.S. Ostroff, Temporal Logic for Real-Time Systems, Research Studies Press LTD., Advanced Software Development Series, Taunton, Somerset, England, 1989
[116] A. Morzenti and P. San Pierto, Object-Oriented Logical Specification of Time Critical Systems, ACM Transaction on Software Engineering and Methodology, Vol. 3, No. 1, Jan. 1994, pp. 56-98
[117] X. Nicollin and J. Sifakis, An overview and synthesis on timed process algebras, In K. Larsen and A. Skou, editors, Proc. CAV'91 3rd InternationalWorkshop Computer Aided Verification, Alborg, Denmark(LNCS 575), Springer Verlag, July 1991, pages 376-398
[118] J.R. Buchi, On a decision method in restricted second order arithmetic, In Proc.??International Conference Logic, Method and Philos. Sci. 1960, Stanford, 1962. Stanford University Press, pages 1-12
[119] Matthew B. Dwyer, George S. Avrunin and James C. Corbett, Property Specification Patterns for Finite-state Verification, In the 2nd Workshop on Formal Methods in Software Practice, March, 1998
[120] Matthew B. Dwyer, George S. Avrunin and James C. Corbett, Patterns in Property Specifications for Finite-state Verification, In the Proceedings of the 21st International Conference on Software Engineering, May, 1999
[121] P. Puschner and A. Burns. Guest Editorial, A Review of Worst-Case Execution-Time Analysis, Real-Tim Systems, 18(2-3), May 2000, pp,115-128
[122] Jakob Engblom, Processor Pipelines and Static Worst-Case Execution Time Analysis, PhD thesis, Acta Universitatis Upsaliensis, Uppsala, Sweden, 2002
[123] Alfred V. Aho, Ravi Sethi, and Jeffrey D. Ullman, Compilers, Principles, Techniques, and Tools, Addison-Wesley, June 1997
[124] F. Jahanian, R. Rajkumar, and S. C. V. Raju, Runtime Monitoring of Timing Constraints in Distributed Real-Time Systems, Real-Time Systems, Vol. 7, No. 3, 1994, pp. 247-273
[125] A.C. Liu and R. Parthasarathi, Hardware Monitoring of a Multiprocessor System, IEEE Micro, Vol.9, No.5, Oct. 1989, pp.44-51
[126] J.J.P. Tsai, K.Y. Fang, and H.Y. Chen, A Noninvasive Architecture to Monitor Real-Time Distributed Systems, Computer, Vol.23, No.3, Mar. 1990, pp. 11-23
[127] W.C. Brantley, K.P. McAuliffe, and T.A. Ngo, RP3 Performance Monitoring Hardware, in Instrumentation for Future Parallel Computing Systems, M. Simmons, R. Koskela, and I. Bucher, eds., ACM Press, New York, 1989, pp.35-47
[128] P.S. Dodd and C.V. Ravishankar, Monitoring and Debugging Distributed Real-Time Programs, Software-Practice and Experience, Vol.22, No. 10, Oct. 1992, pp.863-877
[129] J. Joyce, G. Lomow, K. Slind, and B. Unger, Monitoring Distributed Systems, ACM Trans. Computer Systems, Vol.5, No.2, May 1987, pp.121-150
[130] H. Tokuda, M. Kotera, and C.W. Mercer, A Real-Time Monitor for a Distributed Real-Time Operating System, Proc. ACM Workshop Parallel and Distributed Debugging, 1988,pp.68-77
[131] Dennis K. Peters, and David Lorge Parnas, Requirements-based Monitors for Real-Time Systems, in IEEE Transactions on Software Engineering, Vol. 28, No. 2, February 2002, pp. 146-158
[132] F. Jahanian, Run-time monitoring of real-time systems, in Advances in Real-time Systems, Prentice-Hall, 1995, edited by S.H. Son, pp.435-460
[133] Erik Yu-Shing Hu, Guillem Bernat and Andy Wellings, Addressing Dynamic Dispatching Issues in WCET Analysis for Object-Oriented Hard Real-Time Systems, Proceedings of the 5th IEEE International Symposium on Object-Oriented Real-Time Distributed Computing, Washington D.C., USA, April 2002, pp. 109-116
[134] Jakob Engblom and Bengt Jonsson, Processor pipelines and their properties for static wcet analysis, In Proc. 2nd Embedded Software Conference: Alberto L.??Sangiovanni-Vincentelli, Joseph Sifakis (Eds.), Embedded Software, Grenoble, France: LNCS 2491 Springer Verlag, Oct. 2002, pp. 334-348
[135] Christopher A. Healy, Robert D. Arnold, Frank Mueller, David Whalley, and Marion G. Harmon, Bounding Pipeline and Instruction Cache Performance, IEEE Transactions on Computers, 48(1), Jan. 1999
[136] Christopher A. Healy, Robert D. Arnold, Frank Mueller, David Whalley, and Marion G. Harmon, Bounding Pipeline and Instruction Cache Performance, IEEE Transactions on Computers, 48(1), Jan. 1999
[137] Alan C. Shaw, Reasoning about time in higher level language software, IEEE Transactions on Software Engineering, 15(7), Jul. 1989, pp. 875-889
[138] Sung-Soo Lim, Young H. Bae, Gyu T. Jang, Byung-Do Rhee, Sang L. Min, Chang Y. Park, Heonshik Shin, Kunsoo Park, Soo-Mook Moon, and Chong-Sang Kim, An accurate worst case timing analysis for RISC processors, IEEE Transactions on Software Engineering, 21(7), 1995, pp. 593-604
[139] Christopher A. Healy, Mikael Sj¨odin, and David B. Whalley, Bounding Loop Iterations for Timing Analysis, In Proc. IEEE Real-Time Technology and Aplications Symposium, Jun. 1998, pages 12-21
[140] Jan Gustafsson and Andreas Ermedahl, Automatic derivation of path and loop annotations in object-oriented real-time programs, Parallel and Distributed Computing Practices, 1(2), Jun. 1998
[141] R. Mattolini and P. Nesi, Using tilco for specifying realtime systems, In proceedings of the 2nd IEEE International Conference on Engineering of Complex Computer Systems, ICECCS'96, Montreal, Canada, October 1996
[142] Xin Wang, Zhi-Chang Qi and Shuhao Li, An Optimized Method for Automatic Test Oracle Generation from Real-Time Specification, In proceedings of the 10nd IEEE International Conference on Engineering of Complex Computer Systems, ICECCS'05, Shanghai, China, June 2005
[143] Digital Equipment Corporation, Digital Semiconductor Alpha 21064 and Alpha 21064A Microprocessors Hardware Reference Manual, 1996
[144] 贾永年，计算机在测控网中的应用，国防工业出版社，2000
[145] 姬孟洛，李军，王馨，齐治昌，一种基于抽象解释的自动WCET分析工具，计算机工程，录用待发表[1] The Committee on Information and Communications R&D (CIC) of the National Science, Technology Council (NSTC). America in the Age of Information: A Forum on Federal Information and Communications R&D. Bethesda, Maryland. July 6-7, 1995
[2] Committee on Computing, Information, and Communications, National Science and Technology Council Research Challenges in High Confidence Systems: Proceedings of the Committee on Computing, Information, and Communications Workshop. http://www.hpcc.gOv/pubs/hcs-Aug97/.August 6-7, 1997
[3] High Confidence Systems Working Group, Committee on Computing, Information, and Communications Research and Development, National Science and Technology Council. SETTING AN INTERAGENCY HIGH CONFIDENCE SYSTEMS (HCS) RESEARCH AGENDA: Proceedings of the Interagency High Confidence Systems Workshop. Hosted by the National Coordination Office for Computing, Information, and Communications. Arlington, Virginia. 25 March 1998
[4] High Confidence Software and Systems Coordinating Group, Interagency Working Group on Information Technology Research and Development. HIGH CONFIDENCE SOFTWARE AND SYSTEMS RESEARCH NEEDS, http://www.ccic.gov/pubs/hcss-research.pdf. January 10, 2001
[5] Ministry of Defence: "INT DEF STAN 00-55: The Procurement of Safety Critical Software in Defence Equipment - Issue 1", MoD, April 1991. http://wheelie.tees.ac.uk/hazop/standards/55/
[6] Department of Defense. MIL-STD-882B System Safety Program Requirements, July 1, 1987 NOTICE 1. http://neon.airtime.co.uk/users/wysywig/ 882b.htm
[7] Laplante, P.: Real-Time Systems Design and Analysis: An Engineer' s Handbook. Ieee Press, New York (1992)
[8] J.A.Stankovic: Misconceptions about real-time computing a serious problem for next generation systems. IEEE Computer 21(10) (1998) 10-19
[9] P. J. Pulli, P. Marko, and Heikkinen, Concurrent engineering for real-time systems. IEEE Software, November/December 1993, 10(6): p. 33-38
[10] A. Pnueli. Applications of temporal logic to the specification and verification of reactive systems: a survey of current trends, In Current Trends in Concurrency. Overviews and Tutorials, New York, Springer Lecture Notes in Computer Science, Springer-Verlag, 1986
[11] M. Falla, Advances in Safety Critical Systems: Results and Achievements from the DTI/EPSRC R&D Programe in Safety Critical Systems, Mike Falla, 1997. http://www.comp.lancs.ac.uk/computing/resources/scs/
[12] Richard N Taylor, Structural testing of concurrent programs. IEEE transaction on Software Engineering, March, 18 1992
[13] S. V. Campos, A Quantitative Approach to the Formal Verification of Real-time System, PhD thesis, Carnegie Mellon University, 1996[14] 郑人杰，计算机软件测试技术，清华大学出版社，1992
[15] ANSI/IEEE Std 829-1983, IEEE Standard for Software Test Documentation
[16] 朱鸿，金凌紫，软件质量保障与测试，科学出版社，1997
[17] L. Baresi and M. Young, Test Oracles, Technical Report, CIS-TR01-02, Dept. of Computer and Information Science, Univ. of Oregon, Aug. 2001.http://www.cs.uoregon.edu/-michal/pubs/oracles.html
[18] W. E. Howden and P. Eichhorst, Proving properties of programs from program traces, in Tutorial: Software Testing and Validation, ed by E. Miller and W. E. Howden in IEEE Computer Society: New York. p. 46-56, 1978
[19] L. J. White and E. I. Cohe, A domain strategy for computer program testing. IEEE Transaction on Software Engineering, SE-6: p. 247-257, 1990
[20] R. Alur and T. A. Henzinger. A really temporal logic, In Proceedings of the 30th IEEE Conference on Foundatiions of Computer Science, Los Alamitos, CA, IEEE Computer Society Press, 1989
[21] P. Bellini, R. Mattolini, and P. Nesi, Temporal logics for real-time system specification. ACM Computing Surveys, 32(1): p. 12-42, March 2000
[22] Alur, R.: Techniques of Automatic Verification of Real-Time Systems. PhD thesis, PhD thesis, Stanford University (1991 )
[23] R. Alur, T. Feder, and T. Henzinger. The benefits of relaxing punctuality. Journal of the ACM, 43(1):116{146, January 1996
[24] 《冯友兰学术精华录》，北京师范学院出版社，鲍霁主编，1988年，第119至125页
[25] 明，王夫之，《船山全书》第七册，岳麓出版社，第110页
[26] D. J. Panzl, Automatic Software Test Drivers. Computer, April 1978, 11(4): p. 44-50
[27] Richard G. Hamlet, Testing Programs with the Aid of a Compiler. IEEE Transactions on Software Engineering, July 1977, 3(4): p. 279-290
[28] D. Chapman, A Program Testing Assistant. Communications of the ACM, September 1982
[29] Elaine J. Weyuker, On testing non-testable programs. Computer Journal, 25, 1982: p. 465-470
[30] J. D. Day and J. D. Gannon. A test oracle based on formal specifications. In Proc. SoftFair, A Second Conf. on Software Development Tools, Techniques, and Alternatives, ACM Press, San Francisco, Dec 1985, pages 126-130
[31] Richard N. Taylor, An integrated verification and testing environment. Software-Practice and Experience, 1983, 13: p. 697-713
[32] D. C. Luckham and F. W. von Henke, Overview of Anna, a Specification Language for Ada. IEEE Software, March 1985, 2(2): p. 9-22
[33] D. C. Luckham, F. W. von Henke, B. Krieg-Bruckner, and O. Owe, Anna-A Language for Annotating Ada Programs. Lecture Notes in Computer Science, Springer-Verlag, 1987
[34] S. Sankar, D. Rosenblum, and R. Neff. An Implementation of Anna, In Proceedings of the Ada International Conference on Ada in Use, ACM, Cambridge University Press, May 1985
[35] David Luckham, Programming with Specifications: An Introduction to ANNA, A Language for Specifying Ada Programs. Springer-Verlag, 1990
[36] David S. Rosenblum. Towards a Method of Programming with Assertions, In Proceedings??of the 14th International Conference on Software Engineering, May 1992
[37] David S. Rosenblum, A Practical Approach to Programming With Assertions. IEEE Transactions on Software Engineering, 21(1): p. 19-31, January 1995
[38] R. Kramer. iContract - The Java Design by Contract Tool, In Proceedings of TOOLS26: Technology of Object-Oriented Languages and Systems, IEEE Computer Society, 1998.
[39] P.J. Maker, GNU Nana - User's Guide (version 2.4), Technical report, School of Information Technology - Northern Territory University, July 1998
[40] Jones, C.B., Systematic Software using VDM, 2nd ed., Prentice Hall, 1990.
[41] Bertrand Meyer, Eiffel: The Language. Object-Oriented Series, Prentice Hall, New York, 1992
[42] Bertrand Meyer, Object-Oriented Software Construction. Second Edition, The Object-Oriented Series, Prentice-Hall, 1997
[43] S. Sankar and R. Hayes, ADL: An Interface Definition Language for Specifying and Testing Software. ACM SIGPLAN Notices, August 1994, 29(8): p. 13-21
[44] Sun Microsystems, ADL language reference manual, 1993
[45] ADL Project, Future plans: Ad1 2, http://adl.xopen.org/future/
[46] S. R. Viswanadha and S. Sankar. Preliminary Design of ADL/C++ - A Specification Langauge for C++, In Proceedings of the 2nd Conference on Object-Oriented Technologies and Systems (COOTS), Toronto, Canada, June 1996
[47] M. Obayashi, H. Kubota, S.P. McCarron, and L. Mallet, The Assertion Based Testing Tool for OOP: ADL2. May 1998
[48] Dennis K. Peters and David L. Parnas, Using Test Oracles Generated from Program Documentation. IEEE Transactions on Software Engineering, 1998, 24(3): p. 161-173
[49] D.L. Parnas, J. Madey, and M. Iglewski, Precise Documentation of Well-Structured Programs. IEEE Transactions on Software Engineering, December 1994, 20(12): p. 948-976
[50] John D. Gannon, Paul McMullin, and Richard G Hamlet, Data-Abstraction mplementation, Specification, and Testing. ACM Transactions on Programming Languages and Systems, July 1981, 3(3): p. 211-223
[51] Victor R. Basili. The Design and Implementation of a Family of Application-Oriented Languages. In Proceedings of the 5th Texas Conference on Computing Systems, October 1976, pages 6-12
[52] Sergio Antoy and Richard G. Hamlet, Automatically Checking an Implementation against Its Formal Specification. IEEE Transactions on Software Engineering, January 2000, 26(1): p. 55-69
[53] S. Fujiwara, G. v. Bochmann, F. Khendek, M. Amalou, and A. Ghedamsi, Test Selection Based on Finite State Models. IEEE Transactions on Software Engineering, June 1991, 17(6): p. 591-603
[54] Atif M. Memon, Martha E. Pollack, and Mary Lou Soffa. Automated test oracles for GUIs. In Proceedings of the ACM SIGSOFT 8th International Symposium on the Foundations of Software Engineering (FSE-00), volume 25, 6 of ACM Software Engineering Notes. ACM Press, November 2000, pages 30-39
[55] James H. Andrews. Testing using log file analysis: Tools, methods, and issues, In??Proceedings of the 13th IEEE International Conference on Advanced Software Engineering, Honolulu, Hawaii, October 1998
[56] James H. Andrews and Yingjun Zhang. Broad-spectrum studies of log file analysis, In Proceedings of the 22nd International Conference on Software Engineering (ICSE 2000), Limerick, Ireland, ACM Press, June 2000
[57] Martin S. Feather, Rapid application of lightweight formal methods for consistency analysis. IEEE Transactions on Software Engineering, November 1998, 24(11): p. 949-959
[58] Martin S. Feather and Ben Smith, Automatic generation of test oracles - from pilot studies to application. Automated Software Engineering Journal, 2001, 8(1): p. 31-62
[59] John M. Spivey. The Z Notation: A Reference Manual. Prentice-Hall, 1989
[60] D. Carrington, D. Duke, R. Duke, P. King, G Rose, and G. Smith. Object-Z: An object-oriented extension to Z. In Formal Description Techniques (FORTE '89), North-Holland Publishing Co., December 1989 , pages 281-296
[61] E. Mikk. Compilation of Z Specifications into C for Automatic Test Result Evaluation. In Proceedings of the 9th International Conference of Z Users, volume 967 of Lecture Notes in Computer Science, Springer-Verlag, 1995., pages 167-180
[62] J. McDonald, L. Murray, and P. Strooper. Translating Object-Z specifications to object-oriented test oracles. In Proceedings: 4th Asia-Pacific Software Engineering and International Computer Science Conference, IEEE Computer Society Press, 1997, pages 414-426
[63] J. McDonald and P. Strooper. Translating Object-Z specifications to passive test oracles. In Proceedings of the 2nd International Conference on Formal Engineering Methods (ICFEM98), IEEE Computer Society Press, 1998, pages 165-174
[64] Paul Stocks and David Carrington. A Framework for Specification-Based Testing. IEEE Transactions on Software Engineering, 1996, 22(11):777-793
[65] L.K. Dillon and Qing Yu. Oracles for Checking Temporal Properties of Concurrent Systems, In Proceedings of the ACM SIGSOFT '94 Symposium on the Foundations of Software Engineering, December 1994
[66] L.K. Dillon and Y.S. Ramakrishna. Generating Oracles from Your Favorite Temporal Logic Specifications, In Proceedings of the Fourth ACM SIGSOFT Symposium on the Foundations of Software Engineering, 21 ACM Press, October 1996
[67] Doron Drusinsky. The Temporal Rover and the ATG Rover, In SPIN Model Checking and Software Verification, Proc, 7th SPIN Workshop, Stanford, California, 1885 of Springer-Verlag Lecture Notes in Computer Science, Springer Verlag, 2000
[68] John Hakansson, Automated generation of test scripts from temporal logic specification, Master's thesis, Uppsala University, 2000
[69] A. Pnueli. The temporal logic of programs, In Proceedings of the 18th Annual Symposium on Foundations of Computer Science, Los Alamitos, CA IEEE Computer Society Press, 1977
[70] A. Pnueli, The temporal semantics of concurrent programs. Theor. Comput. Sci, 13, 1981
[71] A. Pnueli. Applications of temporal logic to the specification and verification of reactive systems: a survey of current trends, In Current Trends in Concurrency. Overviews and Tutorials, New York, Springer Lecture Notes in Computer Science, Springer-Verlag, 1986[72] L.K. Dillon, G. Kutty, L. E. Moser, P. M. Melliar-Smith, and Y. S. Ramakrishna. Graphical specification for concurrent software systems, In Proc. 14th IEEE Inter. Conf. Software Engineering, Melbourne, May 1992
[73] 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 Engineering and Methodology, 1994
[74] Pierre Wolper, The tableau method for temporal logic: An overview. Logique et Analyse, 1985,110-111: p.119-136
[75] Moshe Vardy and Pierre Wolper, Reasoning about infinite computations. Information and Computation, 115(1-37), 1994
[76] Rob Gerth, Doron Peled, Moshe Vardi, and Pierre Wolper. Simple on-the-fly automatic verification of linear temporal logic, In Protocol Specification Testing and Verification, Warsaw, Poland, Chapman & Hall, 1995
[77] Y. Kesten, Z. Manna, H. McGuire, and A. Pnueli, A decision algorithm for full prepositional temporal logic. In C. Courooubetis, ed., Proc. 1993 International Conference of Computer-Aided Verification, vol 697 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, 1993, pp. 97-109
[78] H. McGuire, Two Mehtods for Checking Formulas of Temporal Logic, PhD thesis, Dept. of Computer Science, Stanford University, Stanford, California, 1995
[79] Geilen, M.: On the construction of monitors for temporal logic properties. In: K. Havelund and G. Rosu, editors, Proceedings of RV'01 - First Workshop on Run-time Verification. Satellite Workshop of CAV'01, Electronic Notes in Theoretical Computer Science 55(2), Amsterdam, 2001. Elsevier Science, Paris, France (2001)
[80] Kupferman, O. and M. Y. Vardi, Model checking of safety properties, in: N. Halbwachs and D. Peled, editors, Computer Aided Verification: 11th International Conference Proceedings, CAV'99(LNCS 1633), Trento, Italy, July 6-10, 1999, pp. 172-183
[81] R. Koymans, Specifying real-time properties with metric temporal logic. Real-Time Systems, November 1990, 2(4): p. 255-299
[82] C. Ghezzi, D. Mandrioli, and A. Morzenti, TRIO: A logic language for executable specifications of real-time systems. Journal of Systems and software, 12(2): p. 107-123, May 1990
[83] M. Felder and A. Morzenti, Validating real-time systems by history-checking TRIO specifications. ACM Transaction on Software Engineering Methodology, 3(4): p. 308-339, October 1994
[84]M.C.W.Geilen, Formal Techniques for Verification of Complex Real-Time Systems, PhD Thesis, Eindhoven University of Technology, Netherlands, 2002, pp. 159-205
[85] Marius Mikucionis, Brian Nielsen and Kim G. Larsen, Real-time System Testing On-the-fly, The 15th Nordic Workshop on Programming Theory, Turku, Finland, October 29-31, 2003
[86] Wang Yi, Paul Pettersson and Mats Daniels, Automatic Verification of Real-Time Communicating Systems by Constraint Solving, In Proceedings of the 7th International Conference on Formal Description Techniques, North-Holland, 1994, pp. 223-238
[87] K. L. Heninger, J. Kallander, D. L. Parnas, and J. E. Shore, Software Requirements for the??A-7E Aircraft, NRL Memorandum Report 3876, United States Naval Research Laboratory, November 1978
[88] Angelo Gargantini and Connie Heitmeyer. Using Model Checking to Generate Tests from Requirements Specifications. In Proceedings of the 7th European Engineering Conference and the 7th ACM SIGSOFT Symposium on the Foundations of Software Engeneering, volume 24.6 of Software Engineering Notes (SEN), ACM Press, September 6-10 1999, pages 146-162
[89] Jin-Cherng Lin and Ian Ho, Generating timed test cases with oracles for real-time software. Advances in Engineering Software, 2001, 32(9): p. 705-715
[90] J. L. Peterson. Petri Nets Theory and the Modelling of Systems. Prentice-Hall, 1981
[91] Pamela Zave and Michael Jackson. Where Do Operations Come From? A Multiparadigm Specification Technique. IEEE Transactions on Software Engineering, 1996, 22(7):508-528
[92] Debra J. Richardson, Stephanie Leif-Aha, and T. Owen OMalley. Specificationbased Test Oracles for Reactive Systems. In Proceedings of the 14th International Conference on Software Engineering, May 1992, pages 105-118
[93] Comp.realtime: Frequently Asked Questions (FAQs). (version 3.5) http://www.faqs.org/faqs/realtime-computing/faq/index.html
[94] Xin Wang, Ji Wang and Zhi-chang Qi, Automatic Generation of Run-Time Test Oracles for Distributed Real-Time Systems, 24th IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems FORTE 2004, Madrid, Spain, LNCS 3235, Springer-Verlag, September, 2004, pp. 199-212
[95] 姬孟洛，李军，王馨等，实时系统，高等教育出版社，2003，第22页至27页
[96] Languages and methods for specifying real-time systems, Jan Carlson, MRTC report, Malardalen Real-Time Research Centre, Malardalen University, August, 2002
[97] Hans van Vliet. Software Engineering: Principles and Practice. John Wiley & Sons, Chichester, 1993
[98] B. Randell, The Origin of Digital Computer, Springer-Verlag, 1973
[99] R. Floyd, Assigning Meanings to Programs, In. Mathematical Aspects of Computer Science, Proc. Symp. Appl. Maths., Vol 19, American Mathematical Society, 1967, pp. 19-32
[100] C. A. R. Hoare, An Axiomatic Basis for Computer Programming, Comm. ACM, Vol. 12 No.12, Oct. 1969, pp.576-583
[101] P. Naur, Proofs of Algorithms by General Snapshots, BIT Vol. 6, 1969, pp.310-316
[102] E. W. Dijkstra, Guarded commands, nondeterminacy and the formal derivation of programs, Comm. ACM Vol. 18, August 1975, pp. 453-457
[103] D. L. Parnas, A Technique for Software Module Specification With Examples, Comm. ACM Vol. 15, May 1972
[104] B.H. Liskov and S.N. Zilles, Specification Techniques for Data Abstractions, IEEE Transactions on Software Engineering, Vol. 1, No. 1, March 1975, pp. 7-18
[105] J. M. Wing, A Specifier's Introduction to Formal Methods, IEEE Computer, Vol. 23, No. 9, September 1990
[106] D. Craigen, S. Gerhart and T. Ralston, An International Survey of Industrial Applications of Formal Methods, US Dept. Commerce, NIST. Computer System Lab., NISTGCR 93/626, March 1993[107] M.G. Hinchey and J.P. Bowen(eds.), Applications of Formal Methods, Prentice Hall, 1995
[108] E.M. Clarke, J.M. Wing et al, Formal Methods: State of the Art and Future Directions, ACM Computing Surveys, Vol. 28, No. 4, December 1996, pp. 626-643
[109] J.M. Wing, J. Woodcock and J. Davies(eds.), FM-99-World Conference on Formal Methods in the Development of Computing Systems, LNCS 1708 and 1709, Springer-Verlag, 1999
[110] Science of Computer Programming, Special Issue on Formal Methods in Industry, Vol. 36, No. 1, January 2000
[111] Jeannette M Wing, Writing Larch interface language specification, ACM Transactions on Programming Languages and Systems, 1987, 9(1): 1-24
[112] E.M. Clarke, E.A. Emerson and A.P. Sistla, Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM Trans. Program. Lang. Syst. 8, 2, Apr. 1986,244-263
[113] C. Stirling, Comparing linear and branching time temporal logics. In Proceedings of the International Conference on Temporal Logic in Specification, B. Banieqbal, H. Barringer, and A. Pnueli, Eds. Springer Lecture Notes in Computer Science Springer-Verlag, New York, NY, 1-20
[114] R. Razouk, and M. Gorlick, Real-time interval logic for reasoning about executions of real-time programs, SIGSOFT Softw. Eng. Notes 14, 8 (Dec. 1989), 10-19
[115] J.S. Ostroff, Temporal Logic for Real-Time Systems, Research Studies Press LTD., Advanced Software Development Series, Taunton, Somerset, England, 1989
[116] A. Morzenti and P. San Pierto, Object-Oriented Logical Specification of Time Critical Systems, ACM Transaction on Software Engineering and Methodology, Vol. 3, No. 1, Jan. 1994, pp. 56-98
[117] X. Nicollin and J. Sifakis, An overview and synthesis on timed process algebras, In K. Larsen and A. Skou, editors, Proc. CAV'91 3rd InternationalWorkshop Computer Aided Verification, Alborg, Denmark(LNCS 575), Springer Verlag, July 1991, pages 376-398
[118] J.R. Buchi, On a decision method in restricted second order arithmetic, In Proc. International Conference Logic, Method and Philos. Sci. 1960, Stanford, 1962. Stanford University Press, pages 1-12
[119]Matthew B. Dwyer, George S. Avrunin and James C. Corbett, Property Specification Patterns for Finite-state Verification, In the 2nd Workshop on Formal Methods in Software Practice, March, 1998
[120]Matthew B. Dwyer, George S. Avrunin and James C. Corbett, Patterns in Property Specifications for Finite-state Verification, In the Proceedings of the 21st International Conference on Software Engineering, May, 1999
[121] P. Puschner and A. Burns. Guest Editorial, A Review of Worst-Case Execution-Time Analysis, Real-Tim Systems, 18(2-3), May 2000, pp,115-128
[122] Jakob Engblom, Processor Pipelines and Static Worst-Case Execution Time Analysis, PhD thesis, Acta Universitatis Upsaliensis, Uppsala, Sweden, 2002
[123] Alfred V. Aho, Ravi Sethi, and Jeffrey D. Ullman, Compilers, Principles, Techniques, and Tools, Addison-Wesley, June 1997
[124] F. Jahanian, R. Rajkumar, and S. C. V. Raju, Runtime Monitoring of Timing Constraints in??Distributed Real-Time Systems, Real-Time Systems, Vol. 7, No. 3,1994, pp. 247-273
[125] A.C. Liu and R. Parthasarathi, Hardware Monitoring of a Multiprocessor System, IEEE Micro, Vol.9, No.5, Oct. 1989, pp.44-51
[126] J.J.P. Tsai, K.Y. Fang, and H.Y. Chen, A Noninvasive Architecture to Monitor Real-Time Distributed Systems, Computer, Vol.23, No.3, Mar. 1990, pp. 11-23
[127] W.C. Brantley, K.P. McAuliffe, and T.A. Ngo, RP3 Performance Monitoring Hardware, in Instrumentation for Future Parallel Computing Systems, M. Simmons, R. Koskela, and I. Bucher, eds., ACM Press, New York, 1989, pp.35-47
[128] P.S. Dodd and C.V. Ravishankar, Monitoring and Debugging Distributed Real-Time Programs, Software-Practice and Experience, Vol.22, No.10, Oct. 1992, pp.863-877
[129] J. Joyce, G. Lomow, K. Slind, and B. Unger, Monitoring Distributed Systems, ACM Trans. Computer Systems, Vol.5, No.2, May 1987, pp.121-150
[130] H. Tokuda, M. Kotera, and C.W. Mercer, A Real-Time Monitor for a Distributed Real-Time Operating System, Proc. ACM Workshop Parallel and Distributed Debugging, 1988, pp.68-77
[131] Dennis K. Peters, and David Lorge Parnas, Requirements-based Monitors for Real-Time Systems, in IEEE Transactions on Software Engineering, Vol. 28, No. 2, February 2002, pp. 146-158
[132] F. Jahanian, Run-time monitoring of real-time systems, in Advances in Real-time Systems, Prentice-Hall, 1995, edited by S.H. Son, pp.435-460
[133] Erik Yu-Shing Hu, Guillem Bernat and Andy Wellings, Addressing Dynamic Dispatching Issues in WCET Analysis for Object-Oriented Hard Real-Time Systems, Proceedings of the 5th IEEE International Symposium on Object-Oriented Real-Time Distributed Computing, Washington D.C., USA, April 2002, pp. 109-116
[134] Jakob Engblom and Bengt Jonsson, Processor pipelines and their properties for static wcet analysis, In Proc. 2nd Embedded Software Conference: Alberto L. Sangiovanni-Vincentelli, Joseph Sifakis (Eds.), Embedded Software, Grenoble, France: LNCS 2491 Springer Verlag, Oct. 2002, pp. 334-348
[135] Christopher A. Healy, Robert D. Arnold, Frank Mueller, David Whalley, and Marion G. Harmon, Bounding Pipeline and Instruction Cache Performance, IEEE Transactions on Computers, 48(1), Jan. 1999
[136] Christopher A. Healy, Robert D. Arnold, Frank Mueller, David Whalley, and Marion G. Harmon, Bounding Pipeline and Instruction Cache Performance, IEEE Transactions on Computers, 48(1), Jan. 1999
[137] Alan C. Shaw, Reasoning about time in higher level language software, IEEE Transactions on Software Engineering, 15(7), Jul. 1989, pp. 875-889
[138] Sung-Soo Lim, Young H. Bae, Gyu T. Jang, Byung-Do Rhee, Sang L. Min, Chang Y. Park, Heonshik Shin, Kunsoo Park, Soo-Mook Moon, and Chong-Sang Kim, An accurate worst case timing analysis for RISC processors, IEEE Transactions on Software Engineering, 21(7), 1995, pp. 593-604
[139] Christopher A. Healy, Mikael Sjodin, and David B. Whalley, Bounding Loop Iterations for Timing Analysis, In Proc. IEEE Real-Time Technology and Aplications Symposium, Jun.??1998, pages 12-21
[140] Jan Gustafsson and Andreas Ermedahl, Automatic derivation of path and loop annotations in object-oriented real-time programs, Parallel and Distributed Computing Practices, 1 (2), Jun. 1998
[141] R. Mattolini and P. Nesi, Using tilco for specifying realtime systems, In proceedings of the 2nd IEEE International Conference on Engineering of Complex Computer Systems, ICECCS'96, Montreal, Canada, October 1996
[142] Xin Wang, Zhi-Chang Qi and Shuhao Li, An Optimized Method for Automatic Test Oracle Generation from Real-Time Specification, In proceedings of the 10nd IEEE International Conference on Engineering of Complex Computer Systems, ICECCS'05, Shanghai, China, June 2005
[143] Digital Equipment Corporation, Digital Semiconductor Alpha 21064 and Alpha 21064A Microprocessors Hardware Reference Manual, 1996
[144] 贾永年，计算机在测控网中的应用，国防工业出版社，2000
[145] 姬孟洛，李军，王馨，齐治昌，一种基于抽象解释的自动WCET分析工具，计算机工程，录用待发表