TY - GEN
T1 - Formal verification of flight critical software
AU - Miller, Steven P.
AU - Anderson, Elise A.
AU - Wagner, Lucas G.
AU - Whalen, Michael W.
AU - Heimdahl, Mats P.E.
PY - 2005
Y1 - 2005
N2 - Recent advances in modeling languages have made it feasible to formally specify and analyze the behavior of large system components. Synchronous data flow languages, such as Lustre, SCR, and RSML-e are well suited to this task, and commercial versions of these tools such as SCADE and Simulink are growing rapidly in popularity among designers of safety critical systems, largely due to their ability to automatically generate code from the models. At the same time, advances in formal analysis tools have made it practical to formally verify important properties of these models to ensure that design defects are identified and corrected early in the lifecycle. This report describes how such formal verification tools have been applied to the FCS 5000, a new family of Flight Control Systems being developed by Rockwell Collins Inc.
AB - Recent advances in modeling languages have made it feasible to formally specify and analyze the behavior of large system components. Synchronous data flow languages, such as Lustre, SCR, and RSML-e are well suited to this task, and commercial versions of these tools such as SCADE and Simulink are growing rapidly in popularity among designers of safety critical systems, largely due to their ability to automatically generate code from the models. At the same time, advances in formal analysis tools have made it practical to formally verify important properties of these models to ensure that design defects are identified and corrected early in the lifecycle. This report describes how such formal verification tools have been applied to the FCS 5000, a new family of Flight Control Systems being developed by Rockwell Collins Inc.
UR - http://www.scopus.com/inward/record.url?scp=29744452175&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=29744452175&partnerID=8YFLogxK
M3 - Conference contribution
AN - SCOPUS:29744452175
SN - 1563477378
SN - 9781563477379
T3 - Collection of Technical Papers - AIAA Guidance, Navigation, and Control Conference
SP - 5751
EP - 5766
BT - Collection of Technical Papers - AIAA Guidance, Navigation, and Control Conference 2005
T2 - AIAA Guidance, Navigation, and Control Conference 2005
Y2 - 15 August 2005 through 18 August 2005
ER -