Jim Woodcock
Skip Abstract Section
Abstract
Formal methods use mathematical models for analysis and verification at any part of the program life-cycle. We describe the state of the art in the industrial use of formal methods, concentrating on their increasing use at the earlier stages of specification and design. We do this by reporting on a new survey of industrial use, comparing the situation in 2009 with the most significant surveys carried out over the last 20 years. We describe some of the highlights of our survey by presenting a series of industrial projects, and we draw some observations from these surveys and records of experience. Based on this, we discuss the issues surrounding the industrial adoption of formal methods. Finally, we look to the future and describe the development of a Verified Software Repository, part of the worldwide Verified Software Initiative. We introduce the initial projects being used to populate the repository, and describe the challenges they address.
- Abrial, J.-R. 1996. The B-book: Assigning Programs to Meanings. Cambridge University Press, Cambridge, MA. Google Scholar
Cross Ref
- Abrial, J.-R. 2007. Formal methods: Theory becoming practice. JUCS 13, 5, 619--628.Google Scholar
- Allen, R. 1997. A formal approach to software architecture. Ph.D. dissertation, School of Computer Science, Carnegie Mellon University. Issued as CMU Technical Report CMU-CS-97-144. Google ScholarDigital Library
- Allen, R. B. and Garlan, D. 1992. A formal approach to software architectures. In Algorithms, Software, Architecture—Information Processing '92, Volume 1, Proceedings of the IFIP 12th World Computer Congress, Madrid, Spain, 7--11 Sep. 1992, J. van Leeuwen, Ed. IFIP Transactions, vol. A-12. North-Holland, Amsterdam, 134--141. Google ScholarDigital Library
- Arvind, Dave, N., and Katelman, M. 2008. Getting formal verification into design flow. In FM 2008: Formal Methods. Lecture Notes in Computer Science, vol. 5014. Springer-Verlag, Berlin, Heidelberg, Germany, 12--32. Google ScholarDigital Library
- Austin, S. and Parkin, G. 1993. Formal methods: A survey. Tech. rep., National Physical Laboratory, Teddington, Middlesex, UK. Mar.Google Scholar
- Avigad, J. 2007. Course: Practical decision procedures. www.andrew.cmu.edu/user/avigad/practical/. Cited 9 Mar. 2009.Google Scholar
- Aydal, E. G., Paige, R. F., and Woodcock, J. 2007. Evaluation of OCL for large-scale modelling: A different view of the Mondex purse. In MoDELS Workshops. Lecture Notes in Computer Science, vol. 5002. Springer, Berlin, Heidelberg, Germany, 194--205. Google ScholarDigital Library
- Back, R.-J. and von Wright, J. 1990. Refinement calculus, Part I: Sequential nondeterministic programs. In Proceedings of the Stepwise Refinement of Distributed Systems, Models, Formalisms, Correctness, REX Workshop. Lecture Notes in Computer Science, vol. 430. Springer-Verlag, Berlin, Heidelberg, Germany, 42--66. Google ScholarDigital Library
- Badeau, F. and Amelot, A. 2005. Using B as a high level programming language in an industrial project: Roissy VAL. In ZB. Lecture Notes in Computer Science, vol. 3455. Springer-Verlag, Berlin, Heidelberg, Germany, 334--354. Google ScholarDigital Library
- Ball, T. and Rajamani, S. K. 2002. The SLAM project: Debugging system software via static analysis. In POPL, ACM, New York, 1--3. Google ScholarDigital Library
- Balser, M., Reif, W., Schellhorn, G., Stenzel, K., and Thums, A. 2000. Formal system development with KIV. In Proceedings of the 3rd International Conference on Fundamental Approaches to Software Engineering, FASE 2000 (Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS 2000). Lecture Notes in Computer Science, vol. 1783. Springer-Verlag, Berlin, Heidelberg, Germany, 363--366. Google ScholarDigital Library
- Barnes, J. 2003. High Integrity Ada: The SPARK Approach to Safety and Security. Addison-Wesley, Reading, MA. Google ScholarDigital Library
- Barnes, J., Chapman, R., Johnson, R., Widmaier, J., Cooper, D., and Everett, B. 2006. Engineering the Tokeneer enclave protection system. In Proceedings of the 1st International Symposium on Secure Software Engineering. IEEE Computer Society Press, Los Alamitos, CA.Google Scholar
- Barrett, C., Sebastiani, R., Seshia, S. A., and Tinelli, C. 2008. Satisfiability modulo theories. In Handbook of Satisfiability, IOS Press, Amsterdam, The Netherlands, Chapter 12, 737--797.Google Scholar
- Barrett, G. 1987. Formal methods applied to a floating-point number system. Technical Monograph PRG-58, Oxford University Computing Laboratory, Oxford Univ.Google Scholar
- Barrett, G. 1989. Formal methods applied to a floating-point number system. IEEE Trans. Software Eng. 15, 5, 611--621. Google ScholarDigital Library
- Barrett, G. 1990. Verifying the Transputer. In Transputer Research and Applications, Proceedings of the 1st Conference of the North American Transputer Users Group, IOS, Amsterdam, The Netherlands, 17--24. Google ScholarDigital Library
- Behm, P., Benoit, P., Faivre, A., and Meynadier, J.-M. 1999. Météor: A successful application of B in a large project. In World Congress on Formal Methods. Lecture Notes in Computer Science, vol. 1708. Springer-Verlag, Berlin, Heidelberg, Germany, 369--387. Google ScholarDigital Library
- Berry, G. 2008. Synchronous design and verification of critical embedded systems using SCADE and Esterel. In Proceedings of the Formal Methods for Industrial Critical Systems. Lecture Notes in Computer Science, vol. 4916. Springer-Verlag, Berlin, Heidelberg Germany. Google ScholarDigital Library
- Bicarregui, J., Hoare, C. A. R., and Woodcock, J. C. P. 2006. The Verified Software Repository: A step towards the verifying compiler. Formal Asp. Comput. 18, 2, 143--151. Google ScholarCross Ref
- Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., and Rival, X. 2003. A static analyzer for large safety-critical software. In PLDI, ACM, New York, 196--207. Google ScholarDigital Library
- Bloomfield, R. and Craigen, D. 1999. Formal methods diffusion: Past lessons and future prospects. Tech. Rep. D/167/6101, Adelard, Coborn House, 3 Coborn Road, London, UK. Dec.Google Scholar
- Börger, E. and Stärk, R. 2003. Abstract State Machines: A Method for High-Level System Design and Analysis. Springer-Verlag, Berlin, Heidelberg Germany. Google ScholarDigital Library
- Bowen, J. and Stavridou, V. 1993. Safety-critical systems, formal methods and standards. Softw. Eng. J. 8, 4, 189--209.Google ScholarCross Ref
- Bowen, J. P. and Hinchey, M. G. 1995. Ten commandments of formal methods. IEEE Comput. 28, 4 (Apr.), 56--62. Google ScholarDigital Library
- Bowen, J. P. and Hinchey, M. G. 2006. Ten commandments of formal methods… ten years later. IEEE Comput. 39, 1 (Jan.), 40--48. Google ScholarDigital Library
- Burdy, L., Cheon, Y., Cok, D. R., Ernst, M. D., Kiniry, J. R., Leavens, G. T., Leino, K. R. M., and Poll, E. 2005. An overview of JML tools and applications. Softw. Tools. tech. Trans. 7, 3, 212--232.Google Scholar
- Bush, W. R., Pincus, J. D., and Sielaff, D. J. 2000. A static analyzer for finding dynamic programming errors. Softw., Pract. Exper. 30, 7, 775--802. Google ScholarDigital Library
- Butler, M. and Yadav, D. 2008. An incremental development of the Mondex system in Event-B. Formal Asp. Comput. 20, 1, 61--77.Google ScholarCross Ref
- Butterfield, A. 1997. Introducing formal methods to existing processes. In Proceedings of the IEEE Colloquium on Industrial Use of Formal Methods, IET, 7--10.Google ScholarCross Ref
- CADE. 2009. The CADE ATP system competition: The world championship for 1st order automated theorem proving. www.cs.miami.edu/~tptp/CASC/. Cited 9 Mar. 2009.Google Scholar
- Cavalcanti, A., Clayton, P., and O'Halloran, C. 2005. Control law diagrams in circus. In FM 2005: Formal Methods, Lecture Notes in Computer Science, vol. 3582. Springer-Verlag, Berlin, Heidelberg, Germany, 253--268. Google ScholarDigital Library
- CCRA. 2006. Common criteria for information technology security evaluation. Part 1: Introduction and general model. Tech. Rep. CCMB-2006-09-001, Version 3.1, Revision 1, Common Criteria Recognition Agreement. Sept.Google Scholar
- Chalin, P., Kiniry, J. R., Leavens, G. T., and Poll, E. 2006. Beyond assertions: Advanced specification and verification with JML and ESC/Java2. In Proceedings of the 4th International Symposium on Formal Methods for Components and Objects, FMCO 2005. Lecture Notes in Computer Science, vol. 4111. Springer-Verlag, Berlin, Heidelberg, Germany, 342--363. Google ScholarDigital Library
- Chapman, R. 2008. Tokeneer ID Station Overview and Reader's Guide. Tech. Rep. S.P1229.81.8, Issue 1.0, Praxis High Integrity Systems.Google Scholar
- Clarke, E. M., Gupta, A., Jain, H., and Veith, H. 2008. Model checking: Back and forth between hardware and software. In Verified Software: Theories, Tools, Experiments, First IFIP TC 2/WG 2.3 Conference, VSTTE 2005, Revised Selected Papers and Discussions. Lecture Notes in Computer Science, vol. 4171. Springer-Verlag, Berlin, Heidelberg, Germany, 251--255. Google ScholarDigital Library
- Clarke, E. M. and Wing, J. M. 1996. Formal methods: State of the art and future directions. ACM Comput. Surv, 28, 4, 626--643. Google ScholarDigital Library
- Clarke, L. A. and Rosenblum, D. S. 2006. A historical perspective on runtime assertion checking in software development. ACM SIGSOFT Softw. Eng. Notes 31, 3, 25--37. Google ScholarDigital Library
- Craigen, D., Gerhart, S., and Ralston, T. 1993a. An International Survey of Industrial Applications of Formal Methods. Vol. 1 Purpose, Approach, Analysis and Conclusions. U.S. Department of Commerce, Technology Administration, National Institute of Standards and Technology, Computer Systems Laboratory, Gaithersburg, MD.Google Scholar
- Craigen, D., Gerhart, S., and Ralston, T. 1993b. An International Survey of Industrial Applications of Formal Methods. Vol. 2 Case Studies. U.S. Department of Commerce, Technology Administration, National Institute of Standards and Technology, Computer Systems Laboratory, Gaithersburg, MD.Google Scholar
- Cuadrado, J. 1994. Teach formal methods. Byte 19, 12 (Dec.), 292.Google Scholar
- Das, M., Lerner, S., and Seigle, M. 2002. ESP: Path-sensitive program verification in polynomial time. In Proceedings of the Symposium on Programming Language Design and Implementation (PLDI). ACM, New York, 57--68. Google ScholarDigital Library
- DBLP. 2009. Computer Science bibliography. www.informatik.uni-trier.de/~ley/db/. Cited 9 Mar. 2009.Google Scholar
- Dennis, L. A., Collins, G., Norrish, M., Boulton, R. J., Slind, K., and Melham, T. F. 2003. The PROSPER toolkit. Int. J. Softw. Tools Techn. Trans. 4, 2 (Feb.), 189--210.Google ScholarCross Ref
- Deploy. 2009. www.deploy-project.eu. Cited 9 Mar. 2009.Google Scholar
- Dijkstra, E. W. 1975. Guarded commands, nondeterminacy and formal derivation of programs. Commun. ACM 18, 8, 453--457. Google ScholarDigital Library
- EPSRC. 2009. Engineering and Physical Sciences Research Council. www.epsrc.ac.uk. Cited 9 Mar. 2009.Google Scholar
- Evans, D. and Larochelle, D. 2002. Improving security using extensible lightweight static analysis. IEEE Softw. 19, 42--52. Google ScholarDigital Library
- Finney, K. and Fenton, N. Evaluating the effectiveness of Z: The claims made about CICS and where we go from here. J. Syst. Softw. 35, 209--216. Google ScholarDigital Library
- Fitzgerald, J., Larsen, P. G., and Sahara, S. 2008. VDMTools: Advances in support for formal modeling in VDM. SIGPLAN Notices 43, 2 (Feb.), 3--11. Google ScholarDigital Library
- Floyd, R. 1967. Assigning meanings to programs. In Mathematical Aspects of Computer Science, Proceedings of Symposia in Applied Mathematics, Rhode Island. American Mathematical Society, Providence, RI, 19--32.Google Scholar
- Freitas, L. and Woodcock, J. 2008. Mechanising Mondex with Z/Eves. Formal Asp. Comput. 20, 1, 117--139.Google ScholarCross Ref
- Gaudel, M.-C. 1995. Testing can be formal, too. In TAPSOFT'95: Proceedings of the 6th International Joint Conference Theory and Practice of Software Development, CAAP/FASE. Lecture Notes in Computer Science, vol. 915. Springer-Verlag, Berlin, Heidelberg, 82--96. Google ScholarDigital Library
- George, C. and Haxthausen, A. E. 2008. Specification, proof, and model checking of the Mondex electronic purse using RAISE. Formal Asp. Comput. 20, 1, 101--116.Google ScholarCross Ref
- George, V. and Vaughn, R. 2003. Application of lightweight formal methods in requirement engineering. Crosstalk: The J. Defense Softw. Eng.Google Scholar
- Ghose, A. 2000. Formal methods for requirements engineering. In Proceedings of the 2000 International Symposium on Multimedia Software Engineering (ISMSE 2000). IEEE Computer Society Press, Los Alamitos, CA, 13--16. Google ScholarDigital Library
- Gibbons, J. 1993. Formal methods: Why should I care? The development of the T800 Transputer floating-point unit. In Proceedings of the 13th New Zealand Computer Society Conference, New Zealand Computer Society, Auckland, NZ, 207--217.Google Scholar
- Gibbs, W. W. 1994. Software's chronic crisis. Sci. Amer. 271, 3 (Sept.), 72--81.Google Scholar
- Glass, R. L. 1996. Formal methods are a surrogate for a more serious software concern. IEEE Comput. 29, 4 (Apr.), 19.Google Scholar
- Goldsmith, M., Cox, A., and Barrett, G. 1987. An algebraic transformation system for Occam programs. In STACS. Lecture Notes in Computer Science, vol. 247. Springer-Verlag, Berlin, Heidelberg, Germany, 481. Google ScholarDigital Library
- Greve, D. and Wilding, M. 2002. Evaluatable, high-assurance microprocessors. In Proceedings of the NSA High-Confidence Systems and Software Conference (HCSS).Google Scholar
- Guiho, G. D. and Hennebert, C. 1990. SACEM software validation (experience report). In ICSE: Proceedings of the 12th International Conference on Software Engineering. IEEE Computer Society Press, Los Alamitos, CA, 186--191. Google ScholarDigital Library
- Hall, A. 1990. Seven myths of formal methods. IEEE Softw. 7, 5 (Sept.), 11--19. Google ScholarDigital Library
- Hall, A. and Chapman, R. 2002. Correctness by construction: Developing a commercial secure system. IEEE Softw. 19, 1, 18--25. Google ScholarDigital Library
- Haneberg, D., Schellhorn, G., Grandy, H., and Reif, W. 2008. Verification of Mondex electronic purses with KIV: From transactions to a security protocol. Formal Asp. Comput. 20, 1, 41--59. Google ScholarCross Ref
- Hennebert, C. and Guiho, G. D. 1993. SACEM: A fault tolerant system for train speed control. In Proceedings of the Fault Tolerence Computing Systems (FTCS). IEEE Computer Society Press, Los Alamitos, CA, 624--628.Google Scholar
- Hierons, R. M., Bowen, J. P., and Harman, M., Eds. 2008. Formal Methods and Testing An Outcome of the FORTEST Network. Revised Selected Papers. Lecture Notes in Computer Science, vol. 4949. Springer-Verlag, Berlin, Heidelberg, Germany. Google ScholarDigital Library
- Hinchey, M. G. and Bowen, J. P. 1995. Applications of Formal Methods. Prentice-Hall, Englewood Cliffs, NJ. Google ScholarDigital Library
- Hinchey, M. G. and Bowen, J. P. 1996. To formalize or not to formalize? IEEE Comput. 29, 4 (Apr.), 18--19. Google ScholarDigital Library
- Hoare, C. A. R. 1969. An axiomatic basis for computer programming. Commun. ACM 12, 10 (Oct.), 576--581. Google ScholarDigital Library
- Hoare, C. A. R. 1972. Proof of correctness of data representations. Acta Inf. 1, 271--281.Google ScholarDigital Library
- Hoare, C. A. R. 1985. Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs, NJ. Google ScholarDigital Library
- Hoare, C. A. R. 2002a. Assertions in modern software engineering practice. In Proceedings of the 26th International Computer Software and Applications Conference (COMPSAC 2002), Prolonging Software Life: Development and Redevelopment. IEEE Computer Society Press, Los Alamitos, CA, 459--462. Google ScholarDigital Library
- Hoare, C. A. R. 2003. The verifying compiler: A Grand Challenge for computing research. J. ACM 50, 1, 63--69. Google ScholarDigital Library
- Hoare, T. 2002b. Assert early and assert often: Practical hints on effective asserting. Presentation at Microsoft Techfest.Google Scholar
- Hoare, T. 2007. The ideal of program correctness: Third Computer Journal Lecture. Comput. J. 50, 3, 254--260.Google ScholarCross Ref
- Hoare, T. and Misra, J. 2008. Verified software: Theories, tools, and experiments: Vision of a Grand Challenge project. In Verified Software: Theories, Tools, and Experiments. First IFIP TC2/EG2.3 Conference, Lecture Notes in Computer Science, vol. 4171. Springer-Verlag, Berlin, Heidelberg, Germany, 1--18. Google ScholarDigital Library
- Holzmann, G. J. 2004. The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley, Reading, MA. Google ScholarDigital Library
- Hommersom, A., Groot, P., Lucas, P. J. F., Balser, M., and Schmitt, J. 2007. Verification of medical guidelines using background knowledge in task networks. IEEE Trans. Knowl. Data Eng. 19, 6, 832--846. Google ScholarDigital Library
- Houston, I. and King, S. 1991. Experiences and results from the use of Z in IBM. In VDM '91: Formal Software Development Methods. Lecture Notes in Computer Science, vol. 551. Springer-Verlag, Berlin, Heidelberg, Germany, 588--595. Google ScholarDigital Library
- IEC. 1997. Functional safety of electrical/electronic/programmable electronic safety-related systems. Tech. Rep. IEC 61508, International Electrotechnical Commission.Google Scholar
- IEEE. 1985. Standard for Binary Floating-Point Arithmetic, Standard 754-1985 ed. ANSI/IEEE, New York.Google Scholar
- Inmos Ltd. 1988a. Occam2 Reference Manual. Prentice Hall, Englewood Cliffs, NJ.Google Scholar
- Inmos Ltd. 1988b. Transputer Reference Manual. Prentice Hall, Englewood Cliffs, NJ. Google ScholarDigital Library
- ITSEC. 1991. Information technology security evaluation criteria (ITSEC): Preliminary harmonised criteria. Tech. Rep. Document COM(90) 314, Version 1.2, Commission of the European Communities. Jun.Google Scholar
- Jackson, D. and Wing, J. 1996. Lightweight formal methods. IEEE Comput. 29, 4 (Apr.), 22--23.Google Scholar
- Johnson, S. 1978. lint, a C program checker, Unix Programmer, Aos, Manual. Tech. Rep. 65, AT&T Bell Laboratories.Google Scholar
- Jones, C. 1996. A rigorous approach to formal methods. IEEE Comput. 29, 4 (Apr.), 20--21.Google Scholar
- Jones, C. B. 1990. Systematic Software Development Using VDM, 2nd ed. Prentice-Hall International, Englewood Cliffs, NJ. Google ScholarDigital Library
- Jones, C. B. and Pierce, K. G. 2007. What can the π-calculus tell us about the Mondex purse system? In Proceedings of the 12th International Conference on Engineering of Complex Computer Systems (ICECCS 2007). IEEE Computer Society Press, Los Alamitos, CA, 300--306. Google ScholarDigital Library
- Jones, G. and Goldsmith, M. 1988. Programming in Occam2. Prentice-Hall, Englewood Cliffs, NJ. Google ScholarDigital Library
- Josey, A. 2004. The Single Unix Specification Version 3. Open Group, San Francisco, CA. ISBN: 193162447X.Google Scholar
- Joshi, R. and Holzmann, G. J. 2007. A mini challenge: Build a verifiable filesystem. Formal Asp. Comput. 19, 2, 269--272. Google ScholarCross Ref
- Kars, P. 1997. The application of PROMELA and SPIN in the BOS project. In The SPIN Verification System: The Second Workshop on the SPIN Verification System. Proceedings of a DIMACS Workshop. DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol. 33. Rutgers University, Piscataway, NJ, 51--63.Google Scholar
- Krishnaswami, N. R., Aldrich, J., Birkedal, L., Svendsen, K., and Buisse, A. 2009. Design patterns in separation logic. In Proceedings of TLDI'08: 2008 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation. ACM, New York, 105--116. Google ScholarDigital Library
- Kuhlmann, M. and Gogolla, M. 2008. Modeling and validating Mondex scenarios described in UML and OCL with USE. Formal Asp. Comput. 20, 1, 79--100.Google ScholarCross Ref
- Kurita, T., Chiba, M., and Nakatsugawa, Y. 2008. Application of a formal specification language in the development of the “Mobile FeliCa” IC chip firmware for embedding in mobile phones. In FM 2008: Formal Methods. Lecture Notes in Computer Science. Springer-Verlag, Berlin, Heidelberg, Germany, 425--429. Google ScholarDigital Library
- Larsen, P. G. and Fitzgerald, J. 2007. Recent industrial applications of VDM in Japan. In FACS 2007 Christmas Workshop: Formal Methods in Industry, BCS, eWIC, London, U.K. Google ScholarDigital Library
- Larsen, P. G., Fitzgerald, J., and Brookes, T. 1996. Applying formal specification in industry. IEEE Softw. 13, 3 (May), 48--56. Google ScholarDigital Library
- Larus, J. R., Ball, T., Das, M., DeLine, R., Fähndrich, M., Pincus, J. D., Rajamani, S. K., and Venkatapathy, R. 2004. Righting software. IEEE Softw. 21, 3, 92--100. Google ScholarDigital Library
- Leino, K. R. M. 2007. Specifying and verifying programs in Spec#. In Perspectives of Systems Informatics, 6th International Andrei Ershov Memorial Conference, PSI 2006, Revised Papers. Lecture Notes in Computer Science, vol. 4378. Springer-Verlag, Berlin, Heidelberg, Germany, 20. Google ScholarDigital Library
- May, D., Barrett, G., and Shepherd, D. 1992. Designing chips that work. Philosoph. Trans. Roy. Soc. A 339, 3--19.Google ScholarCross Ref
- Meyer, B. 1991. In Advances in Object-Oriented Software Engineering, Prentice-Hall, Englewood Cliffs, NJ, Chapter Design by Contract, 1--50.Google Scholar
- Miller, S. and Srivas, M. 1995. Formal verification of the AAMP5 microprocessor. In Proceedings of the Workshop on Industrial-Strength Formal Specification Techniques (WIFT95). IEEE Computer Society Press, Los Alamitos, CA. Google ScholarDigital Library
- Miller, S. P. 1998. The industrial use of formal methods: Was Darwin right? In Proceedings of the 2nd IEEE Workshop on Industrial Strength Formal Specification Techniques. IEEE Computer Society Press, Los Alamitos, CA, 74--82. Google ScholarDigital Library
- Miller, S. P., Greve, D. A., and Srivas, M. K. 1996. Formal verification of the AAMP5 and AAMP-FV microcode. In Proceedings of the 3rd AMAST Workshop on Real-Time Systems.Google Scholar
- Morgan, C. 1988. The specification statement. ACM Trans. Program. Lang. Syst. 10, 3, 403--419. Google ScholarDigital Library
- Morris, J. M. 1987. A theoretical basis for stepwise refinement and the programming calculus. Sci. Comput. Program. 9, 3, 287--306. Google ScholarDigital Library
- NASA. 1997. Formal methods, specification and verification guidebook for the verification of software and computer systems. vol II: A practitioner's companion. Tech. Rep. NASA-GB-001-97, Washington, DC. May.Google Scholar
- NASA. 1998. Formal methods, specification and verification guidebook for the verification of software and computer systems. vol I: Planning and technology insertion. Tech. Rep. NASA/TP-98-208193, Washington, DC. Dec.Google Scholar
- Norman, D. A. 1999. The Invisible Computer: Why Good Products Can Fail, the Personal Computer Is So Complex, and Information Appliances Are the Solution. MIT Press, Cambridge, MA. Google ScholarDigital Library
- O'Hearn, P. W., Reynolds, J. C., and Yang, H. 2001. Local reasoning about programs that alter data structures. In Computer Science Logic, 15th International Workshop, CSL 2001. 10th Annual Conference of the EACSL. Lecture Notes in Computer Science, vol. 2142. Springer-Verlag, Berlin, Heidelberg, Germany, 1--19. Google ScholarDigital Library
- Overture-Core-Team. 2007. Overture web site. www.overturetool.org. Cited 9 Mar. 2009.Google Scholar
- Owre, S., Rushby, J. M., and Shankar, N. 1992. PVS: A prototype verification system. In CADE-11, Proceedings of the 11th International Conference on Automated Deduction. Lecture Notes in Computer Science, vol. 607. Springer-Verlag, Berlin, Heidelberg, Germany, 748--752. Google ScholarDigital Library
- RAISE Language Group. 1992. The RAISE Specification Language. The BCS Practitioners Series. Prentice-Hall, Englewood Cliffs, NJ.Google Scholar
- RAISE Method Group. 1995. The RAISE Development Method. The BCS Practitioners Series. Prentice-Hall International, Engleward Cliffs, NJ.Google Scholar
- Ramananandro, T. 2008. Mondex, an electronic purse: Specification and refinement checks with the Alloy model-finding method. Formal Asp. Comput. 20, 1, 21--39. Google ScholarCross Ref
- Riazanov, A. and Voronkov, A. 2002. The design and implementation of VAMPIRE. AI Commun. 15, 2--3, 91--110. Google ScholarDigital Library
- RODIN-Project-Members. 2007. RODIN web site. rodin.cs.ncl.ac.uk/. Cited 9 Mar. 2009.Google Scholar
- Romanovsky, A. 2008. DEPLOY: Industrial deployment of advanced system engineering methods for high productivity and dependability. ERCIM News 74, 54--55.Google Scholar
- Roscoe, A. W. and Hoare, C. A. R. 1988. The laws of Occam programming. Theoret. Comput. Sci. 60, 177--229. Google ScholarDigital Library
- Rushby, J. 1993. Formal methods and the certification of critical systems. Tech. Rep. CSL-93-7, Computer Science Laboratory, Menlo Park, CA. Dec.Google ScholarCross Ref
- Rushby, J. 2000. Disappearing formal methods. In High Assurance Systems Engineering, 2000, Fifth IEEE International Symposium on HASE 2000. IEEE Computer Society Press, Los Alamitos, CA.Google ScholarCross Ref
- Saiedian, H. 1996. An invitation to formal methods. IEEE Comput. 29, 4 (Apr.), 16--30. Google ScholarDigital Library
- Shankar, N. and Woodcock, J., Eds. 2008. Verified Software: Theories, Tools, Experiments, Second International Conference, VSTTE 2008. Lecture Notes in Computer Science, vol. 5295. Springer-Verlag, Berlin, Heidelberg, Germany. Google ScholarDigital Library
- Shepherd, D. 1988. The role of Occam in the design of the IMS T800. In Communicating Process Architectures. Prentice-Hall, Englewood Cliffs, NJ.Google Scholar
- Shepherd, D. and Wilson, G. 1989. Making chips that work. New Scientist 1664, 39--42.Google Scholar
- Snook, C. and Butler, M. 2006. UML-B: Formal modeling and design aided by UML. ACM Trans. Softw. Eng. Methodol. 15, 1, 92--122. Google ScholarDigital Library
- Snook, C. and Harrison, R. 2001. Practitioners' views on the use of formal methods: An industrial survey by structured interview. Inf. Softw. Tech. 43, 275--283.Google ScholarCross Ref
- Spinellis, D. 2008. A look at zero-defect code. www.spinellis.gr/blog/20081018/. Cited 9 Mar. 2009.Google Scholar
- Spivey, J. M. 1989. The Z Notation: a Reference Manual. International Series in Computer Science. Prentice-Hall, Englewood Cliffs, NJ. Google ScholarDigital Library
- Srivas, M. and Miller, S. 1995. Applying formal verification to a commercial microprocessor. In Proceedings of the IFIP Conference on Hardware Description Languages and their Applications (CHDL'95).Google Scholar
- Stepney, S., Cooper, D., and Woodcock, J. 2000. An electronic purse: Specification, refinement, and proof. Technical Monograph PRG-126, Oxford University Computing Laboratory. Jul.Google Scholar
- Thomas, M. 1992. The industrial use of formal methods. Microproc. Microsyst. 17, 1 (Jan.), 31--36. Google ScholarDigital Library
- Tiwari, A., Shankar, N., and Rushby, J. 2003. Invisible formal methods for embedded control systems. Proc. IEEE 91, 1 (Jan), 29--39.Google ScholarCross Ref
- Tokeneer. 2009. www.adacore.com/tokeneer. Cited 9 Mar. 2009.Google Scholar
- TPTP. 2009a. Entrants' system descriptions. www.cs.miami.edu/~tptp/CASC/J2/SystemDescriptions.html. Cited 9 Mar. 2009.Google Scholar
- TPTP. 2009b. The TPTP problem library for automated theorem proving. www.cs.miami.edu/~tptp/. Cited 9 Mar. 2009.Google Scholar
- Tretmans, J., Wijbrans, K., and Chaudron, M. 2001. Software engineering with formal methods: The development of a storm surge barrier control system revisiting seven myths of formal methods. Form. Methods Syst. Des. 19, 2, 195--215. Google ScholarDigital Library
- Vafeiadis, V. and Parkinson, M. J. 2007. A marriage of rely/guarantee and separation logic. In Proceedings of the 18th International Conference on Concurrency Theory, CONCUR 2007. Lecture Notes in Computer Science, vol. 4703. Springer-Verlag, Berlin, Heidelberg, Germany, 256--271. Google ScholarDigital Library
- van Lamsweerde, A. 2003. From system goals to software architecture. In SFM. 25--43.Google Scholar
- VSR. 2009. Verified Software Repository. vsr.sourceforge.net/fmsurvey.htm. Cited 9 Mar. 2009.Google Scholar
- Ward, M. P. and Bennett, K. H. 1995. Formal methods to aid the evolution of software. Int. J. Softw. Eng. Knowl. Eng. 5, 25--47.Google ScholarCross Ref
- Wijbrans, K., Buve, F., Rijkers, R., and Geurts, W. 2008. Software engineering with formal methods: Experiences with the development of a storm surge barrier control system. In FM2008: Formal Methods, Vol. 5014. Springer-Verlag, Berlin, Heidelberg, Germany, 419--424. Google ScholarDigital Library
- Wilding, M., Greve, D., and Hardin, D. 2001. Efficient simulation of formal processor models. Form. Meth. Syst. Des. 18, 3 (May), 233--248. Google ScholarDigital Library
- Wing, J. M. 1990. A specifier's introduction to formal methods. IEEE Comput. 23, 9, 8--24. Google ScholarDigital Library
- Woodcock, J. and Davies, J. 1996. Using Z: Specification, Refinement, and Proof. International Series in Computer Science. Prentice-Hall, Englewood Cliffs, NJ. Google ScholarDigital Library
- Woodcock, J., Stepney, S., Cooper, D., Clark, J. A., and Jacob, J. 2008. The certification of the Mondex electronic purse to ITSEC Level E6. Formal Asp. Comput. 20, 1, 5--19.Google ScholarCross Ref
- Younger, E. J., Luo, Z., Bennett, K. H., and Bull, T. M. 1996. Reverse engineering concurrent programs using formal modelling and analysis. In Proceedings of the 1996 International Conference on Software Maintenance (ICSM '96). IEEE Computer Society Press, Los Alamitos, CA, 255--264. Google ScholarDigital Library
Index Terms
- Formal methods: Practice and experience
Recommendations
Mechanising Mondex with Z/Eves
AbstractWe describe our experiences in mechanising the specification, refinement, and proof of the Mondex Electronic Purse using the Z/Eves theorem prover. We took a conservative approach and mechanised the original LaTEX sources without changing their ...
The certification of the Mondex electronic purse to ITSEC Level E6
Abstract.Ten years ago the Mondex electronic purse was certified to ITSEC Level E6, the highest level of assurance for secure systems. This involved building formal models in the Z notation, linking them with refinement, and proving that they correctly ...
A Formal Specification of Mondex Using SAM
SOSE '08: Proceedings of the 2008 IEEE International Symposium on Service-Oriented System EngineeringThis paper presents a formal specification of Mondex, an electronic purse, using SAM. Mondex is the first pilot project for the 6th Grand Challenge to develop an integrated, automated toolset that developers can use to establish the correctness of ...
Comments