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 including pointers to "reasoning tools." Formal Methods Resources - 6 Prepared at the University of Maryland and specific to usability engineering. Software Engineering and Formal Methods - Knowledge Bases A portal containing an extensive list of pointers to formal methods resources. Formal Methods Education Resources Links to tools, papers, instructional materials, and methods information. Bug Free Software Pointers to resources about correctness proofs and program verification. Formal Methods : Related Resources Pointers to a small set of useful resources. Formal Methods Links Still more FM links. Formal Methods - Web Links Still more FM links. Software Engineering using Formal Methods Collected, annotated links to papers and tools. Formal Methods Group Homepage Developed by the FM groups at The University of Manchester (UK), this page presents a useful list (with links) to major FM achievements. Tutorials, Articles and Papers on FM • Introductory Concepts Formal methods A in-depth discussion at Wkipedia. What is formal methods? A good introduction with a number of useful links to important papers and resources. A Review of Formal Methods An in-depth discussion of FM. Formal Methods Concepts A brief overview. pdf: Seven Myths of Formal Methods A paper by Anthony Hall that addresses 7 commonly held (but incorrect) beliefs about FM. Formal Methods in IT Theory, methods, philosophy, and languages.. 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. • Advanced Topics A "Grand Challenge'': Unifying Theories of Formal Methods In what looks like the beginning of a book, the author provides useful discussion and links to many resources, languages and tools. Presently (2009) under construction, but still worth a visit. IBM Research Formal Verification and Testing Technologies Formal tools and techniques used by IBM. Toward Formal-Methods Oecumenism? A discussion of the "religious wars" that arise between proponents of one FM approach or another. Formal Methods Proofs A few brief examples of small program proofs in Haskell and Isabelle/HOL. Set Theory Related Resources Pointers to a vast array of set theory -related web sites. • Articles and Papers Formal Methods Books and Reports A list of books and reports that are relevant to FM. Recommended. pdf: Formal Methods In Software Engineering A worthwhile overview of FM in the SE context. "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. • Applied Methods Using Lightweight Formal Methods in User Interface Verification FM applied during the development of GUIs. Lightweight formal methods A short discussion of "lightweight" FMs. 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?" Formal Methods for Developing Adaptable, Secure, Situation-Aware Service-Oriented (AS3) Architectures "In this paper, the authors are concerned with formal methods for developing agent-based, situation-aware, secure, survivable architectures for on-demand discovery and composition of web services." Downloadable. Free registration required. Formal Methods for Industrial Critical Systems A brief discussion with a list of pointers to applicable resources and papers. Formal methods in HCI Links to papers and resources for FM applied to human-computer interaction (HCI). Formal Specification and Development of Embedded Systems A very brief description and series of pointers. Languages that Support Formal Methods • Z, VDM and LARCH 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. VDM Resources Links to VDM related resources LARCH Resources Links to a number of LARCH resources • Object Constraint Language (OCL) Introduction to OCL A brief but worthwhile introduction. Recommended. What is OCL? Useful information provided in a white paper about OCL. OCL Center Information on the latest release of the standards, general introduction, tools, and other resources. OCL Tutorial In-depth discussion of OCL along with many examples. OCL Resources OCL resources and statements from IBM. OCL Resources A limited collection of pointers to documents and tools. OCL Resources-Tools Pointers to selected OCL tools. Object Constraint Language Quotes, pointers and other useful information. pdf: UML 2.0 OCL Specification "This specification contains defines the Object Constraint Language (OCL), version 2.0. OCL version 2.0 is the version of. OCL that is aligned with UML 2.0." pdf: Object Constraint Language (OCL) Introduction A fairly detailed slideshow on OCL. Recommended. Using OCL for Meta-Modeling An in-depth report out of McGill University. OCL examples Examples of important OCL notation. Some Shortcomings of OCL, the Object Constraint Language of UML A downloadable paper. Object Constraint Language (OCL) Descriptive information about OCL semantics and syntax. See also additional examples and detailed discussion. FM Tools FM Tools Many useful links including pointers to a variety of FM tools. Formal Methods Tools-List 1 An abbreviated list of FM tools and research initiatives. Formal Methods Tools-List 2 An abbreviated list of FM tools and research initiatives. Formal Methods Education Resources-Tools Links to a variety of FM tools and languages. 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: • Concepts and Methods Formal Specification and Documentation using Z: A Case Study Approach A Programming Approach to Formal Methods Industrial Application of Formal Methods Industrial-Strength Formal Methods Formal Foundations for Software Engineering Methods Applications of Formal Methods Understanding Formal Methods • Languages, Z, VDM, and OCL Z in Practice The Way of Z: Practical Programming with Formal Methods Z: A Beginner's Guide Introducing Specification Using Z: A Practical Case Study Approach Formal Methods Fact File: VDM and Z An Introduction to Formal Specification with Z and VDM Object Constraint Language Object Modeling with OCL • Mathematical Elements Essence of Discrete Mathematics A Logical Approach to Discrete Math 2000 Solved Problems in Discrete Mathematics