University of Minnesota
Software Engineering Center

You are here

Willem Visser

Recent Publications

The Hidden Models of Model Checking

In the past, applying formal analysis, such as model checking, to industrial problems required a team of formal methods experts and a great deal of effort. Model checking has become popular, because model checkers have evolved to allow domain-experts, who lack model checking expertise, to analyze their systems. What made this shift possible and what roles did models play in this? That is the main question we consider here.

FITE: Future Integrated Testing Environment

It is well known that the later software errors are discovered during the development process, the more costly they are to repair, yet testing and automated analysis tools tend to be applied late in the development cycle. In this paper, we describe a future integrated testing environment (FITE) that continually analyzes code for a variety of functional and non-functional properties to provide developer feedback as code is being written. This instant feedback allows developers to fix errors as they are introduced, increasing developer productivity and software quality.

Auto-Generating Test Sequences using Model Checkers: A Case Study

Use of model-checking approaches for test generation from requirement models have been proposed by several researchers. These approaches leverage the witness (or counter-example) generation capability of model-checkers for constructing test cases. Test criteria are expressed as temporal properties. Witness traces generated for these properties are instantiated to create complete test sequences, satisfying the criteria. State-space explosion can, however, adversely impact model-checking and hence such test generation. Thus, there is a need to