ePrints

A Proof of Satisfiability in Mukherjee and Stavridou's Ammunition Control System

Lookup NU author(s): Professor John Fitzgerald

Downloads

• Published version [.pdf]

Abstract

This report illustrates the use of rigorous proof in the validation of a model in the formal language VDM-SL. The illustration is based on a system which monitors and controls the safe storage of explosives. Using the established proof theory of VDM-SL, the proof of satisfiability of an operation is conducted to a high degree of rigour, with proofs of supporting auxiliary results. The paper is intended to serve as a case study for researchers developing proof and validation support systems for model-oriented specification languages.

Publication metadata

Author(s): Fitzgerald JS

Publication type: Report

Publication status: Published

Series Title: Department of Computing Science Technical Report Series

Year: 1997

Pages: 27

Print publication date: 01/01/1997

Source Publication Date: 1997

Report Number: 616

Institution: Department of Computing Science, University of Newcastle upon Tyne

Place Published: Newcastle upon Tyne

URL: http://www.cs.ncl.ac.uk/publications/trs/papers/616.pdf

Share