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.
[2]
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.
[3]
Robin Milner.A Calculus of Communicating Systems[M].USA:Springer, 1980.
[4]
N Lynch, M Tuttle.An introduction to input/output automata[J].CWI Quarterly, 1989,2(3):219-246.
[5]
R Alur.Timed automata[A].11th International Conference on Computer-Aided Verification[C].LNCS 1633, Berlin:Springer-Verlag, 1999.8-22.
[6]
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.
[7]
C B Jones.Systematic Software Development Using VDM[M].New Jersey:Prentice Hall International Series in Computer Science, Prentice Hall, 1986.
[8]
Mogens Nielsen, Klaus Havelund, Kim Bitter Wagner, Chris George.The RAISE language, method and tools[J].Formal Asp.Comput,1989,1(1):85-114.
Gerard J Holzmann.The Spin Model Checker Primer and Reference Manual[M].Boston:Addison-Wesley, 2003.
[11]
Michael J C Gordon.Introduction to the HOL system[A].TPHOLs[C].New York, USA:IEEE Computer Society, 1991.2-3.
[12]
NASA.Software Safety NASA Technical Standard.NASA-STD-8719.13A[S].September 15,1997.
[13]
John Musa.Software Reliability Engineering[M].New York:McGraw-Hill, 1999.
[14]
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.
[15]
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.
[16]
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.
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.
[19]
Tony Hoare.The verifying compiler:A grand challenge for computing research[J].JACM,2003,50(1):25-35.
[20]
Standish Group.The CHAOS Report[R].Found at http://www.standishgroup.com.1995.
[21]
The Inquiry Board.Ariane 5 Flight 105 Inquiry Board Report[R].Paris:European Space Agency Press,July 1996.
[22]
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.
[23]
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.
[24]
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.
[25]
C A R Hoare.An axiomatic basis for computer programming[J].Communications of the ACM, 1969,12(10):576-580.
[26]
C A R Hoare.Communicating Sequential Processes[M].Prentice-Hall International Series in Computing Science, Prentice-Hall International,Englewood Cliffs, N J London, 1985.
[27]
Zohar Manna, Amir Pnueli.The Temporal Logic of Reactive and Concurrent Systems:Specification[M].Berlin:Springer-Verlag, 1992.
[28]
Edmund M Clarke, Jeannette M Wing.Formal methods:State of the art and future directions[J].ACM Computing Surveys, 1996,28(4):626-643.
[29]
J M Spivey.The Z Notation:A Reference Manual[M].New Jersey:International Series in Computer Science, Prentice Hall, 1989.
[30]
David Harel.Statecharts:A visual formalism for complex systems[J].Science of Computer Programming, 1987,8(3):231-274.
[31]
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.
[32]
K L McMillan.Symbolic model checking-an approach to the state explosion problem[D].SCS, Carnegie Mellon University, 1992.
[33]
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.
[34]
Sergey Berezin.Model Checking and Theorem Proving:a Unified Framework[D].Also a TR number CMU-CS-02-100.Carnegie Mellon University, 2002.
[35]
Michael R Lyu.Software Fault-Tolerance[M].New York:John Wiley,1995.
[36]
Stacy J Prowell, Carmen J Trammell, Richard C Linger, Jesse H Poore.Cleanroom Software Engineering:Technology and Process[M].Boston:Addison Wesley Professional, 1999.
[37]
David L Parnas.Software aspects of stratigic defense systems[J].Communications of the ACM, 1985,28(12):1326-1335.
[38]
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.
[39]
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.
