Title :
Proving properties of a safety-critical system
Author :
Atkinson, Will ; Cunningham, Jim
Author_Institution :
Dept. of Adv. Comput., AEA Technol., Harwell, UK
fDate :
3/1/1991 12:00:00 AM
Abstract :
The paper describes the FOREST approach to formal requirements specification and particularly the role of an automated theorem prover in validating specifications written in MAL, the FOREST logic. The MAL prover uses a tableau method for constructing its proofs, with rules to handle the action modalities and quantification of MAL. The authors illustrate its use in validation by using the prover to establish that a safety-critical railway-signalling specification has some desirable safety properties
Keywords :
formal specification; program verification; safety; software reliability; theorem proving; FOREST approach; MAL; automated theorem prover; formal requirements specification; safety properties; safety-critical railway-signalling specification; safety-critical system; tableau method; validation;
Journal_Title :
Software Engineering Journal
