University of Minnesota
Software Engineering Center
/

You are here

Darren Cofer

Recent Publications

Your "What" is My "How": Iteration and Hierarchy in System Design

Systems are naturally constructed in hierarchies, in which design choices made at higher levels of abstraction levy requirements on system components at the lower levels. Thus, whether an aspect of a system is a design choice or a requirement largely depends on your vantage point within the system components' hierarchy. Systems are also often constructed from the middle-out rather than top-down; compatibility with existing systems and architectures and availability of specific components influence high-level requirements.

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.

Circular Hierarchical Reasoning using Past Time LTL

We describe a composition rule for hierarchically composed components that may involve circular reasoning between the components. It is similar to previous work by McMillan, specialized to component level reasoning. In contrast to McMillan's work, our composition rule can be used in provers that only support safety properties (e.g. k-induction model checkers) as long as the system and component contracts consist of state invariants. The composition rule still holds for richer contracts, but the resulting verification conditions then require a general purpose model checker.

Pages