University of Minnesota
Software Engineering Center

You are here

Steven Miller

Recent Publications

Compositional Verification of Architectural Models

This paper describes a design flow and supporting tools to significantly improve the design and verification of complex cyber-physical systems. We focus on system architecture models composed from libraries of components and complexity-reducing design patterns having formally verified properties. This allows new system designs to be developed rapidly using patterns that have been shown to reduce unnecessary complexity and coupling between components.

Software Model Checking Takes Off

The increasing popularity of model-based development and the growing power of model checkers are making it practical to use formal verification for important classes of software designs. A barrier to doing this in an industrial setting has been the need to translate the commercial modeling languages developers use into the input languages of the verification tools. This paper describes a translator framework that enables the use of model checking and theorem proving on complex avionics systems and describes its use in three industrial case studies.

Software Model Checking for Avionics SSoftware MSoftware Model Checking for Avionics SSoftware Model Checking for Avionics Systemsystemsodel Checking for Avionics Systemsystems

The adoption of model-based development tools is changing the cost-benefit equation for the industrial use of formal methods. The integration of formal methods such as model checking into software development environments makes it possible to fight increasing cost and complexity with automation and rigor. This paper describes how formal analysis tools can be inserted into a model-based development process to decrease costs and increase quality of safety-critical avionics software.