Validation of Formal Models: A Case Study

A valid formal model is well-defined in the portion of the real world being modeled, and relevant to the system-development project it is intended to support. This paper explains in depth what makes a formal model valid, and shows its critical importance in formal methods for system development, including program verification. The paper is based on a classroom presentation [8] of the well-known Peterson algorithm for locking in concurrent systems [23]. The paper shows how to formalize this case study in Alloy [10], and uses it to present a list of manual and automated techniques for validating formal models.