%0 Journal Article %1 miller_07_providing %A Miller, Steven %A Tribble, Alan %A Whalen, Michael %A Heimdahl, Mats P. %D 2007 %J International Journal on Software Tools for Technology Transfer (STTT) %K 2007 mdd formal_verification requirements %R 10.1007/s10009-006-0173-9 %T Providing the shalls %U http://dx.doi.org/10.1007/s10009-006-0173-9 %X Incomplete, inaccurate, ambiguous, and volatile requirements have plagued the software industry since its inception. The convergence of model-based development and formal methods offers developers of safety-critical systems a powerful new approach to the early validation of requirements. This paper describes an exercise conducted to determine if formal methods could be used to validate system requirements early in the lifecycle at reasonable cost. Several hundred functional and safety requirements for the mode logic of a typical flight guidance system were captured as natural language ^a€oeshall"i¿½? statements. A formal model of the mode logic was written in the RSML^aˆ’e language and translated into the NuSMV model checker and the PVS theorem prover using translators developed as part of the project. Each ^a€oeshall"i¿½? statement was manually translated into a NuSMV or PVS property and proven using these tools. Numerous errors were found in both the original requirements and the RSML^aˆ’e model. This demonstrates that formal models can be written for realistic systems and that formal analysis tools have matured to the point where they can be effectively used to find errors before implementation.

@article{miller_07_providing, abstract = {Incomplete, inaccurate, ambiguous, and volatile requirements have plagued the software industry since its inception. The convergence of model-based development and formal methods offers developers of safety-critical systems a powerful new approach to the early validation of requirements. This paper describes an exercise conducted to determine if formal methods could be used to validate system requirements early in the lifecycle at reasonable cost. Several hundred functional and safety requirements for the mode logic of a typical flight guidance system were captured as natural language ^{a}€{oe}shall"{i}¿½? statements. A formal model of the mode logic was written in the RSML^{a}ˆ’e language and translated into the NuSMV model checker and the PVS theorem prover using translators developed as part of the project. Each ^{a}€{oe}shall"{i}¿½? statement was manually translated into a NuSMV or PVS property and proven using these tools. Numerous errors were found in both the original requirements and the RSML^{a}ˆ’e model. This demonstrates that formal models can be written for realistic systems and that formal analysis tools have matured to the point where they can be effectively used to find errors before implementation.}, added-at = {2009-02-11T20:52:50.000+0100}, author = {Miller, Steven and Tribble, Alan and Whalen, Michael and Heimdahl, Mats P.}, biburl = {https://www.bibsonomy.org/bibtex/242437e8ac45db88a85d6acd54a7c1047/leonardo}, citeulike-article-id = {1736742}, doi = {10.1007/s10009-006-0173-9}, interhash = {4990c2df057e5b67165e6d3065b06775}, intrahash = {42437e8ac45db88a85d6acd54a7c1047}, journal = {International Journal on Software Tools for Technology Transfer (STTT)}, keywords = {2007 mdd formal_verification requirements}, posted-at = {2007-10-07 19:00:17}, priority = {2}, timestamp = {2009-02-11T20:52:50.000+0100}, title = {Providing the shalls}, url = {http://dx.doi.org/10.1007/s10009-006-0173-9}, year = 2007 }