Requirements Modeling and Analysis

Model-Based Design & Analysis (Powerpoint Talk)

Requirements modeling lies at the heart of our approach. Creating an executable model of the system’s behavior will uncover more oversights and inconsistencies than simply writing natural-language specifications. Moreover, such models can be connected to a mock-up of the user interface and executed with the customer to validate the behavior that the customer wants. While many tools strive to produce specifications that can be reviewed with all stakeholders, it is also important that the notation have a formal semantics that can support automated analyses such as consistency and completeness checks and proof of safety properties.  In this way, one model can support validation with the customer, verification of key properties, test case generation, and code generation.

Early work on the MT-FCS project focused on use of the RSML^-e language supported by the CriSys Laboratory of the University of Minnesota. More recently, we have developed translators that allow us use a variety of formal analysis tools (NuSMV, PVS, and SAL) with commercially supported modeling tools such Simulink and SCADE. When using these commercial modeling tools, we view the models as detailed software requirements, restate the system requirements allocated to software into formal properties over these models, and prove that the models satisfy these requirements.

Publications Related to Requirements Modeling and Analysis

• Steven P. Miller, Elise A. Anderson, Lucas G. Wagner, Michael W. Whalen, and Mats P.E. Heimdahl, Formal Verification of Flight Critical Software, in Proceedings of the AIAA Guidance, Navigation and Control Conference and Exhibit, San Francisco, August 15-18, 2005.
• Steven P. Miller, Early Validation of Requirements, in Proceedings of the World Computer Congress 2004, Toulouse, France, August 23-27, 2004.
• Steven P. Miller, Alan C. Tribble, Michael W. Whalen, and Mats P. E. Heimdahl, Proving the Shalls: Early Validation of Requirements Through Formal Methods, Journal of Software Tools for Technology Transfer, [in press].
• Steven P. Miller, Mats P.E. Heimdahl, and Alan C. Tribble, Proving the Shalls, in Proceedings of FM 2003: the 12^th International FME Symposium, Sept. 8-14, 2003
• Steven P. Miller, Alan C. Tribble, Timothy M. Carlson and Eric J. Danielson, Flight Guidance System Requirements Specification , NASA/CR-2003-212426, June 2003.
• Steven P. Miller, Alan C. Tribble, Extending the Four-Variable Model to Bridge the System-Software Gap, in Proceedings of the 20th Digital Avionics Systems Conference, Oct. 14-18, 2001. Selected as best paper of the Systems Engineering track.