Proving the Shalls: The Future of Requirements

October 7, 2004

Location: Amundson 162

Thursday, 
October 7, 2004
5:30-8:00  p.m. at  The University of Minnesota
5:30 start for networking,  6:15 start for  meeting.

Topic: Proving the Shalls: The Future of Requirements
Speaker:  Dr. Steve Miller, Rockwell Collins Inc.

Directions:   
A map is available at  http://onestop.umn.edu/Maps/AmundH/index.html
Check out the detailed map.


This  Month's Meeting:

 
Abstract:     
This presentation describes a case study conducted to determine how effectively formal methods could be used to capture and validate the requirements of a typical embedded system. A model of the mode logic of a Flight Guidance System was specified in the RSML-e notation and translated into the NuSMV model checker and the PVS theorem prover. These tools were then used to verify several hundred properties of the RSML-e model.  In the process, several errors were discovered and corrected in the original model.  This demonstrates that formal requirements models can be written for real problems and that formal analysis tools have matured to the point where they can be used to find errors before implementation.

Steve Miller is a Senior Principal Engineer in the Advanced Technology Center of Rockwell Collins and has over 20 years of experience in software development. He received his Ph.D. in computer science from the University of Iowa in 1991 and a B.A. in physics and mathematics from the University of Iowa.

His current research interests include requirements modeling and analysis, formal methods, software safety analysis, mode awareness, product family engineering, and software testing. He is principle investigator on a project sponsored by NASA Langley and Collins to investigate advanced methods and tools for the development flight critical systems. Prior to this he has lead several research efforts at Collins, including a collaborative effort with SRI International and NASA Langley to formally verify the microcode in the AAMP5 and AAMP-FV microprocessors using the PVS verification system.

Dr. Steven P. Miller
Rockwell Collins
400 Collins Road NE, MS 108-206
Cedar Rapids, Iowa 52498-0001
Phone       (319) 295-2055
Fax   (319) 295-2005
Email spmiller@rockwellcollins.com

The following files related to this presentation are available for download:

Proving the Shalls: Slides from Presentation
Type: application/pdf, Size: 856 KB
Description:

Proving the Shalls - Prepublication version of paper to appear.
Type: application/pdf, Size: 487 KB
Description: