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

Challenges in Testing Next Generation CPS Systems

Testing cyber-physical systems presents a unique set of testing challenges: heterogeneity, timing, and, especially, observability. In particular, some of the mechanisms that are designed to make embedded software robust are the same mechanisms that present challenges for automated testing techniques: e.g., rate limiting, fault masking, and debounce logic, which can lead to long lags between problematic inputs and their manifestation in system outputs. In addition, much of the control behavior of CPS is mathematically intensive more than "branchy".

Domain Modeling for Development Process Simulation

Simulating agile processes prior to adoption can reduce the risk of enacting an ill-fitting process. Agent-based simulation is well-suited to capture the individual decision-making valued in agile. Yet, agile's lightweight nature creates simulation difficulties as agents must fill-in gaps within the specified process. Deliberative agents can do this given a suitable planning domain model. However, no such model, nor guidance for creating one, currently exists.

Towards Synthesis from Assume-Guarantee Contracts involving Infinite Theories: A Preliminary Report

In previous work, we have introduced a contract-based {\em realizability checking} algorithm for assume-guarantee contracts involving infinite theories, such as linear integer/real arithmetic and uninterpreted functions over infinite domains. This algorithm can determine whether or not it is possible to construct a realization (i.e. an implementation) of an assume-guarantee contract. The algorithm is similar to k-induction model checking, but involves the use of quantifiers to determine implementability.

Pages