| [1] Standish Group.The CHAOS Report[R].Found at http://www.standishgroup.com.1995.[2] The Inquiry Board.Ariane 5 Flight 105 Inquiry Board Report[R].Paris:European Space Agency Press,July 1996.[3] National Science,Technology Council(NSTC).America in the Age of Information:A Forum on Federal Information and Communications R&D[R].Bethesda, Maryland, July 6-7,1995.[4] NSTC.Research challenges in high confidence systems[A].Proceedings of the Committee on Computing, Information, and Communications Workshop[C].USA:http://www.hpcc.gov/pubs/hcs-Aug97/intro.html, August 6-7,1997.[5] High Confidence Systems Working Group, NSTC.Setting an interagency high confidence systems(HCS) research agenda[A].Proceedings of the Interagency High Confidence Systems Workshop[C].Arlington,Virginia,25 March 1998.[6] High Confidence Software and Systems Coordinating Group.High Confidence Software and Systems Research Needs[R].USA:http://www.ccic.gov/pubs/hcss-research.pdf, January 10,2001.[7] President's Information Technology Advisory Committee.Information Technology Research:Investing in Our Future[R].Report to the President, USA:http://www.cs.rice.edu/～ken/presentations/PITAC.pdf, February 24,1999.[8] C A R Hoare.An axiomatic basis for computer programming[J].Communications of the ACM, 1969,12(10):576-580.[9] C A R Hoare.Communicating Sequential Processes[M].Prentice-Hall International Series in Computing Science, Prentice-Hall International,Englewood Cliffs, N J London, 1985.[10] Robin Milner.A Calculus of Communicating Systems[M].USA:Springer, 1980.[11] N Lynch, M Tuttle.An introduction to input/output automata[J].CWI Quarterly, 1989,2(3):219-246.[12] Zohar Manna, Amir Pnueli.The Temporal Logic of Reactive and Concurrent Systems:Specification[M].Berlin:Springer-Verlag, 1992.[13] R Alur.Timed automata[A].11th International Conference on Computer-Aided Verification[C].LNCS 1633, Berlin:Springer-Verlag, 1999.8-22.[14] R Alur, C Courcoubetis, T A Henzinger, P H Ho.Hybrid automata:An algorithmic approach to the specification and verification of hybrid systems[A].Hybrid Systems[C].LNCS 736, Berlin:Springer-Verlag,1993.209-229.[15] Edmund M Clarke, Jeannette M Wing.Formal methods:State of the art and future directions[J].ACM Computing Surveys, 1996,28(4):626-643.[16] J M Spivey.The Z Notation:A Reference Manual[M].New Jersey:International Series in Computer Science, Prentice Hall, 1989.[17] C B Jones.Systematic Software Development Using VDM[M].New Jersey:Prentice Hall International Series in Computer Science, Prentice Hall, 1986.[18] David Harel.Statecharts:A visual formalism for complex systems[J].Science of Computer Programming, 1987,8(3):231-274.[19] Mogens Nielsen, Klaus Havelund, Kim Bitter Wagner, Chris George.The RAISE language, method and tools[J].Formal Asp.Comput,1989,1(1):85-114.[20] Edmund Clarke, Bernd-Holger Schlingloff.Model checking[A].Handbook of Automated Reasoning[M].Edited by Alan Robinson and Andrei Voronkov, Boston:MIT Press,2001.1635-1790.[21] 林惠民、张文辉.模型检测:理论、方法与应用[J].电子学报,2002,30(12A):1907-1912.[22] K L McMillan.Symbolic model checking-an approach to the state explosion problem[D].SCS, Carnegie Mellon University, 1992.[23] Gerard J Holzmann.The Spin Model Checker Primer and Reference Manual[M].Boston:Addison-Wesley, 2003.[24] S Owre, J M Rushby, N Shankar.PVS:A prototype verification system[A].D Kapur, editor.Automated Deduction(CADE-11)[C].volume607 of Lecture Notes in Computer Science, Berlin:Springer-Verlag,1992.748-752.[25] Michael J C Gordon.Introduction to the HOL system[A].TPHOLs[C].New York, USA:IEEE Computer Society, 1991.2-3.[26] Sergey Berezin.Model Checking and Theorem Proving:a Unified Framework[D].Also a TR number CMU-CS-02-100.Carnegie Mellon University, 2002.[27] NASA.Software Safety NASA Technical Standard.NASA-STD-8719.13A[S].September 15,1997.[28] Michael R Lyu.Software Fault-Tolerance[M].New York:John Wiley,1995.[29] John Musa.Software Reliability Engineering[M].New York:McGraw-Hill, 1999.[30] Mark C Paulk, Charles V Weber, Bill Curtis, Mary Beth Chrissis.The Capability Maturity Model Guidelines for Improving the Software Process[M].Boston:Addison-Wesley Publishing Company, 1998.[31] Stacy J Prowell, Carmen J Trammell, Richard C Linger, Jesse H Poore.Cleanroom Software Engineering:Technology and Process[M].Boston:Addison Wesley Professional, 1999.[32] Mike Falla.Advances in Safety Critical Systems-Results and Achievements from the DTI/EPSRC R&D Programme in Safety Critical Systems[R].Lancaster University Computing Department, http://www.comp.lancs.ac.uk/computing/resources/scs/index.html, 1997.[33] David L Parnas.Software aspects of stratigic defense systems[J].Communications of the ACM, 1985,28(12):1326-1335.[34] Siddhartha R Dalal, Jesse H Poore, Michael L Cohen.Innovations in Software Engineering for Defense Systems[M].Washington:the National Academies Press, D.C,2003.[35] John Hatcliff, William Deng, Matthew Dwyer, Georg Jung, Venkatesh Prasad.Cadena:An integrated development, analysis, and verification environment for component-based systems[A].Proceedings of the International Conference on Software Engineering(ICSE 2003)[C].New York:IEEE Press,2003.160-173.[36] 杨芙清、梅宏、吕建、金芝.浅论软件技术发展[J].电子学报,2002,30(12A):1901-1906.[37] George C Necula, Peter Lee.Safe kernel extensions without run-time checking[A].2nd Symposium on Operating Systems Design and Implementation(OSDI'96)[M].Seattle, WA, October, 1996.229-243.[38] Sumant Kowshik, Dinakar Dhurjati, Vikram Adve.Ensuring code safety without runtime checks for real-time control systems[A].Proc Int Conf on Compilers, Architecture and Synthesis for Embedded Systems(CASES02)[C].Grenoble, France, Oct.2002.288-297.[39] Tony Hoare.The verifying compiler:A grand challenge for computing research[J].JACM,2003,50(1):25-35. |
