University of Minnesota
Software Engineering Center

You are here

Beyond Static Code Analysis

Date of Event: 
Thursday, July 23, 2009 - 3:00pm
Static code analysis is an approach for reasoning about the behavior of software without executing it. There are several "lightweight" analyses that allow a user to show that a program is well-formed in some way: e.g., it doesn't contain any runtime errors. While these analyses can show the absence of certain undesirable behaviors, they cannot determine whether a program is correct, that is, it meets its requirements specification. In this talk, I will briefly describe property-driven software development, in which formalized requirements are used to drive the development process. Once requirements are formalized, it is possible to check them for consistency and completeness, and to use a variety of tools to automatically test or even prove that software meets its requirements. Recent advances in model checkingtools have made it practical, for certain kinds of software, to quickly and automatically prove whether or not software meets its requirements. I will present some case studies of using this approach on complex avionics and security systems, and argue that a significant amount of medical device software is amenable to this development approach.
Presentation Files: