The document is structured as follows:
Pages
Projects
- Common Framework Initiative
- The lack of a common framwork for algebraic specification greatly hinders the dissemination and application of research results in algebraic specification. In particular, the proliferation of specification languages, some differing in only quite minor ways from each other, is a considerable obstacle for the use of algebraic methods in industrial contexts, making it difficult to exploit standard examples, case studies and training material. A common framework with widespread support throughout the research community is urgently needed.
Papers
- Ten Commandments of Formal Methods
- Jonathan P. Bowen and Michael G. Hinchey
This is an interpretation of ten commandments for formal methods.- An Introduction to Formal Hardware Verification
- Carl-Johan H. Seger
This paper provides an introduction to formal hardware verification by describing three of the main approaches to formal hardware verification: theorem-proving, model checking and symbolic simulation.- The FM9001 Microprocessor
- The FM9001 is a general-purpose 32-bit microprocessor whose gate-level netlist design implementation was developed using a theorem-proving environment in conjunction with a traditional CAD system.
Z & VDM
Pages
- The Z Language
- Z is a formal specification language that has been developed by the Programming Research Group (PRG) at the Oxford University Computing Laboratory (OUCL).
- The VDM
- VDM stands for "Vienna Development Method". VDM's origins lie in the research on formal semantics of programming languages at IBM's Vienna Laboratory in the 1960s and 70s.
Papers
- Case studies in the verification of specifications in VDM and Z (99 pages)
- Peter Lindsay and Erik van Keulen
This is a technical report from the University of Queensland It contains case studies for the specification of the following cases:It also contains some interesting points about VDM, Z, and
- Birthday Book
- Traffic Management System
- Message Transmitter
- Dependency Management System
- A Simple Grammar
mural(a verification tool for VDM).- Understanding the differences between VDM and Z
- I. J. Hayes, C. B. Jones and J. E. Nicholls
This paper attempts to provide an understanding of the interesting differences between two well-known specification languages. The main ideas are presented in the form of a discussion.- VDM Bibliography
- This document contains the annotated VDM bibliography with 524 entries related to VDM. The listed items come from a wide variety of sources, but unfortunately the list is not yet exhaustive.
This version contains a partitioning of entries into categories of subjects. A little introduction and background material is given, and some advice on how to get started with VDM (for newcomers).
- VDM Examples Repository
- This is a collection of examples of how you can use VDM for different applications. These are real examples of usage of VDM.
- A Guide to Reading VDM Specifications
- Bob Fields
The intention of this document is to give an overview of the syntax of the specification language of the Vienna Development Method (VDM) as an aid to those who are to some extend familiar with formal notations and have to read or review documents containing VDM.- The Z-into-Haskell tool-kit
- Howard S. Goodman
A new method of writing Haskell programs from Z specifications is proposed, whose use is illustrated elsewhere in my ZUM '95 paper. This method can be regarded as a kind of `tool-kit', consisting essentially of three discrete parts: a set of high-level guidelines for the programmer; a framework for handling input/output and state; and a set of lower-level rules, indicating how to translate various Z constructs, in particular, those of Z's `mathematical tool-kit', into Haskell. This paper presents the Z-into-Haskell tool-kit itself, as it currently stands, in the form of a combined tutorial and reference manual. It is intended that the reader, with some knowledge of Z and Haskell, can use this to begin to develop his/her own programs from specifications.TLA
Papers
- Introduction to TLA (8 pages)
- Leslie Lamport
A short (8-page) introduction to what TLA formulas mean. It should allow you to understand TLA specifications.- TLA+ (37 pages)
- Leslie Lamport
TLA+ is a formal language for defining and asserting the validity of TLA formulas. This paper should enable you to understand TLA+ specifications, but it does not explain how to write them.SDL
SDL is a Specification and Description Language standardised by ITU-T (formerly CCITT). The language has been evolving since the first recommendation in 1980, 1984, 1988 and 1992 when Object Oriented features were included in the language. SDL is widely used in the telecommunications field.