Title :
Position paper for WIFT´98 [“Pushbutton” analysis via integration of industrial tools with formal validation]
Author :
Feather, Martin S. ; Dunphy, Julia ; Rouquette, Nicolas
Author_Institution :
Jet Propulsion Lab., California Inst. of Technol., Pasadena, CA, USA
Abstract :
Spacecraft fault protection software is a challenging and critical system. Our goal is to use the same specifications for the starting point of both the code development (whether manual or automated) and the formal analysis. Furthermore, we aim to automate as much as possible of the analysis process, to make it an easy-to-apply “pushbutton”-like activity. Towards this end, we are integrating an industrial tool (Rational Rose, a UML tool) with a formal methods tool (the SPIN model checker). In particular, we are developing an automatic translator from Rational Rose statecharts to Promela (the input language of SPIN). We intend to use this translator to convert statechart descriptions of fault protection designs into Promela, and to apply SPIN to check crucial properties of those designs
Keywords :
aerospace computing; fault diagnosis; formal specification; formal verification; protection; safety-critical software; software tools; space vehicles; Promela; Rational Rose; SPIN; UML tool; automatic translator; code development; design properties checking; fault protection designs; formal methods; formal specifications; formal validation; high-assurance systems; industrial processes; integrated techniques; model checker; pushbutton-like activity; spacecraft fault protection software; statechart descriptions; Protection; Space vehicles; Unified modeling language;
Conference_Titel :
Industrial Strength Formal Specification Techniques, 1998. Proceedings. 2nd IEEE Workshop on
Conference_Location :
Boca Raton, FL
Print_ISBN :
0-7695-0081-1
DOI :
10.1109/WIFT.1998.766309
