Software Engineering Resources
	Formal Methods Formal methods allow a software engineer to create a specification that is more complete, consistent, and unambiguous than those produced using conventional or object-oriented methods. Set theory and logic notation are used to create a clear statement of facts (requirements). This mathematical specification can then be analyzed to prove correctness and consistency. Because the specification is created using mathematical notation, it is inherently less ambiguous that informal modes of representation. The following topic categories are presented: Formal Methods (FM) Resources Tutorials, Articles and Papers on FM Languages that Support Formal Methods FM Tools Books Formal Methods (FM) Resources The Formal Methods - Europe Hub Contains a large collection of worthwhile information on FM. Recommended. NASA Formal Methods Site many useful resources and pointers to other organizations that focus on FM. Formal Methods Resources - 1 Extensive information on formal methods and tools. Formal Methods Resources - 2 A set of useful FM resources has been prepared by DoD's DACS. Formal Methods Resources - 3 A collection of general FM resources maintained by the NRC Canada. Formal Methods Resources - 4 Useful information, including a tutorial can be found at NASA Langley's FM site. Formal Methods Resources - 5 Many useful links inlcuding pointers to "reasoning tools." Formal Methods Resources - 6 Prepared at the University of Maryland and specific to usability engineering. Formal Methods Resources - 7 A categorized list of FM resources. Tutorials, Articles and Papers on FM The NASA Formal Methods Guidebook (2 volumes) Vol. 1 (88 pp.) is written for project decision makers, including managers, engineers, and assurance personnel, who are considering the use of Formal Methods on their project. Vol. 2 (245 pp.) is designed for practitioners to help transition Formal Methods from experimental use into practical application for critical software requirements and design within NASA. Both are downloadable. Recommended. A Review of Formal Methods An indepth discussion of FM. Formal Methods Concepts A breif overview. Set Theory Related Resources Pointers to a vast array of set theory -related web sites. "Formal Methods and their Role in the Certification of Critical Systems" A paper by John Rushby whose purpose is to explain the use of formal methods in the specification and verification of software and hardware requirements, designs, and implementations, to identify the benefits, weaknesses, and difficulties in applying these methods to digital systems used in critical applications, and to suggest factors for consideration when formal methods are offered in support of certification. FM in HCI Development A variety of resources (including a tutorial) that discuss the use of FM in human-computer interaction development. Formal Specification and Development of Embedded Systems A very brief description and series of pointers. Lightweight Formal Methods A brief paper that presents "a lightweight [FM] approach, which, in contrast, emphasizes partiality and focused application, [and] can bring greater benefits at reduced cost. What are the elements of a lightweight approach?" Languages that Support Formal Methods The Z Formal Specification Language Detailed information on Z including a FAQ. Formal Methods and Z Pointers to a variety of Z resources. An Analysis of Z and VDM An article that compares these two languages. Object Constraint Language (OCL) Descriptive information about OCL semantics and syntax.See also additional examples and detailed discussion. The OCL Center Contains a number of useful tutorials, papers and links to other resources. FM Tools FM Tools Many useful links including pointers to a variety of FM tools. Books A fairly large number of books on formal methods topics have been published over the past decade. A listing of some of the more useful offerings follows: Bowan, J., Formal Specification and Documentation using Z: A Case Study Approach, International Thomson Computer Press, 1996. Casey, C., A Programming Approach to Formal Methods, McGraw-Hill, 2000. Clark. T. et al (eds.), Object Modeling with OCL, Springer-Verlag, 2002. Cooper, D. and R. Barden, Z in Practice, Prentice-Hall, 1995. Craigen, D., S. Gerhart, and T. Ralston, Industrial Application of Formal Methods to Model, Design and Analyze Computer Systems, Noyes Data Corp., 1995. Harry, A., Formal Methods Fact File: VDM and Z, Wiley, 1997. Hinchley, M. and J. Bowan, Applications of Formal Methods, Prentice-Hall, 1995. Hinchley, M. and J. Bowan, Industrial Strength Formal Methods, Academic Press, 1997. Hussmann, H., Formal Foundations for Software Engineering Methods, Springer-Verlag, 1997. Jacky, J., The Way of Z: Practical Programming with Formal Methods, Cambridge University Press, 1997. Monin, F. and M. Hinchey, Understanding Formal Methods, Springer-Verlag, 2003. Rann, D., J. Turner, and J. Whitworth, Z: A Beginner's Guide, Chapman and Hall, 1994. Ratcliff, B., Introducing Specification Using Z: A Practical Case Study Approach, McGraw-Hill, 1994. Sheppard, D., An Introduction to Formal Specification with Z and VDM, McGraw-Hill, 1995. Warmer, J. and A. Kleppe, Object Constraint Language, Addison-Wesley, 1998. Dean (Essence of Discrete Mathematics, Prentice-Hall, 1996), Gries (A Logical Approach to Discrete Math, third edition, Springer-Verlag, 1995) and Lipschultz and Lipson (2000 Solved Problems in Discrete Mathematics, McGraw-Hill, 1991) present useful information for those who must learn more about the mathematical underpinnings of formal methods.