DocumentCode
1457409
Title
Proving properties of a safety-critical system
Author
Atkinson, Will ; Cunningham, Jim
Author_Institution
Dept. of Adv. Comput., AEA Technol., Harwell, UK
Volume
6
Issue
2
fYear
1991
fDate
3/1/1991 12:00:00 AM
Firstpage
41
Lastpage
50
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;
fLanguage
English
Journal_Title
Software Engineering Journal
Publisher
iet
ISSN
0268-6961
Type
jour
Filename
73716
Link To Document