|
|
|
MUTT
Overview
MUTT (MSIL Unit Testing Tools) is a joint project of the SRR and FSE groups. MUTT's goal is to automate the generation of unit tests for managed code (.NET). We envision MUTT as an intelligent assistant to the programmer that can automatically generate a set of unit tests by symbolic analysis of the code and then interact with the programmer in order to increase the coverage of the set of tests. Because we expect units to be of moderate size, MUTT will be able to perform accurate semantic analysis of the code. The Pex project is the active continuation of the MUTT project. We have developed a set of tools in the context of the MUTT project: Unit Meister requires specifications in the form of parameterized unit tests. Parameterized unit tests extend the current industry practice of using closed unit tests defined as parameterless methods. Parameterized unit tests separate two concerns: 1) They specify the external behavior of the involved methods for all possible test arguments. 2) Test cases can be re-obtained as traditional closed unit tests by instantiating the parameterized unit tests. Unit Meister uses symbolic execution and constraint solving to automatically choose a minimal set of inputs that exercise a parameterized unit test with respect to possible code paths of the implementation. In addition, Unit Meister uses parameterized unit tests as symbolic summaries which allows symbolic execution to scale for arbitrary abstraction levels. Crash Meister is a variant of Unit Meister. It works in the absence of user-provided specifications. Using default exploration bounds, it executes one method at a time with symbolic inputs, and finds unexpected exceptions like null pointer dereferences, index out of bounds, etc. Crash Meister generates unit tests which represent explored paths. Crash Meister can also be used to study a method's dynamic behavior since it visualizes all explored paths in the form of an execution tree. Axiom Meister is a recent addition to the set of tools. This prototype implements a new way to automatically infer specifications from code. Given an implementation of an abstract data type, it infers axioms of its observable behavior. It does so in three steps. First it executes a given modifier method symbolically; next it applies observer methods in constrained states, resulting in many specialized axioms; finally it generalizes, merges and simplifies the axioms. The resulting likely specifications can be examined by the user; they can also be used as input for Unit Meister, or as input to Spec#, a program verification system. We develop a theory to reason about completeness and soundness of the generated axioms. Except for limitations of employed theorem provers, the user can approach full completeness and soundness by providing more observers. Publications
People
Project Members
(Past) interns:
Associated Groups
|
||||||||
