University of Minnesota
Software Engineering Center
/

You are here

Critical Systems Research Group

The Critical Systems Research Group’s (CriSys) research interests are in the general area of software engineering; in particular, software development for critical software applications — applications where incorrect operation of the software could lead to loss of life, substantial material or environmental damage, or large monetary losses. The long-term goal of our research activities is the development of a comprehensive framework for the development of software for critical software systems. Our work has focused on some of the most difficult and least understood aspects of software development—requirements specification and validation/verification.

Recent Publications

A flexible and non-intrusive approach for computing complex structural coverage metrics

Software analysis tools and techniques often leverage structural code coverage information to reason about the dynamic behavior of software. Existing techniques instrument the code with the required structural obligations and then monitor the execution of the compiled code to report coverage. Instrumentation based approaches often incur considerable runtime overhead for complex structural coverage metrics such as Modified Condition/Decision (\mcdc). Code instrumentation, in general, has to be approached with great care to ensure it does not modify the behavior of the original code.

Are We There Yet? Determining the Adequacy of Formalized Requirements and Test Suites

Structural coverage metrics have traditionally categorized code as either covered or uncovered. Recent work presents a stronger notion of coverage, checked coverage, which counts only statements whose execution contributes to an outcome checked by an oracle. While this notion of coverage addresses the adequacy of the oracle, for Model-Based Development of safety critical systems, it is still not enough; we are also interested in how much of the oracle is covered, and whether the values of program variables are masked when the oracle is evaluated.

Towards Realizability Checking of Contracts using Theories

Virtual integration techniques focus on building architectural models of systems that can be analyzed early in the design cycle to try to lower cost, reduce risk, and improve quality of complex embedded systems. Given appropriate architectural descriptions and compositional reasoning rules, these techniques can be used to prove important safety properties about the architecture prior to system construction.

Pages