About Us


  Process Models

  SE Resources


  Contact us

Breaking News!

A new blog ... visit OnCenter, Roger Pressman's running commentary on the world at large

A new edition ... the 7th edition of Software Engineering is available now

A new book ... Roger Pressman and David Lowe on Web Engineering

A first novel ... Roger Pressman's first novel is a technothriller -- The Aymara Bridge

A new curriculum! RSP&A has partnered with QAI to develop a comprehensive Internet-based software engineering curriculum.

A redesigned site! ... we've done a major redesign and added many new features for 2009 - 2010

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


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.

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

Site search! We've added links to a search engine that will enable you to search our entire site for information you need. Enter the appropriate word or phrase below.


Home About us Products Product Models SE Resources Commentary Contact us

Web site and all contents © R.S. Pressman & Associates, Inc. 2001 - 2010, All rights reserved.

Free website templates