Title :
A tool for practical reasoning about state machine designs
Author :
Cant, A. ; Eastaughffe, K.A. ; Ozols, M.A.
Author_Institution :
Div. of Inf. Technol., Defence Sci. & Technol. Organ., Salisbury, SA, Australia
Abstract :
Critical systems (e.g. safety critical and security critical systems) need the highest levels of assurance. The effective engineering design of critical systems still lacks easy to use, practical and above all trustworthy tools which allow the exploration of possible design strategies, and support formal reasoning about their critical properties. We describe the Veracity prototype tool, aimed at providing support for modelling and reasoning about state machine designs for critical software based devices. The tool has three main components: a graph editor, for constructing state transition diagrams; an animator, for exploring symbolic execution of the machine; and a prover, for verifying critical properties of the machine
Keywords :
finite state machines; program verification; quality control; safety-critical software; security of data; theorem proving; Veracity prototype tool; animator; critical properties; critical software based devices; critical system; engineering design; formal reasoning; graph editor; practical reasoning; security critical systems; state machine designs; state transition diagrams; symbolic execution; trustworthy tools; Automation; Formal specifications; Functional programming; Graphical user interfaces; Power engineering and energy; Pressing; Process design; Prototypes; User interfaces; Writing;
Conference_Titel :
Australian Software Engineering Conference, 1996., Proceedings of 1996
Conference_Location :
Melbourne, Vic.
Print_ISBN :
0-8186-7635-3
DOI :
10.1109/ASWEC.1996.534119