Validation of Contracts using Enabledness Preserving Finite State Abstractions
Guido de Caso∗ Víctor Braberman∗
∗ Departamento de Computación, FCEyN, UBA
Buenos Aires, Argentina
{gdecaso, vbraber, diegog, suchitel}@dc.uba.ar
Diego Garbervetsky∗ Sebastián Uchitel∗†
† Department of Computing, Imperial College
London, UK
su2@doc.ic.ac.uk
Abstract
Pre/post condition-based specifications are common-
place in a variety of software engineering activities that
range from requirements through to design and implemen-
tation. The fragmented nature of these specifications can
hinder validation as it is difficult to understand if the spec-
ifications for the various operations fit together well. In
this paper we propose a novel technique for automatically
constructing abstractions in the form of behaviour mod-
els from pre/post condition-based specifications. The level
of abstraction at which such models are constructed pre-
serves enabledness of sets of operations, resulting in a fi-
nite model that is intuitive to validate and which facilitates
tracing back to the specification for debugging. The paper
also reports on the application of the approach to an indus-
trial strength protocol specification in which concerns were
identified.
1. Introduction
Pre/post condition specifications constitute good prac-
tice in a variety of software engineering activities [16].
In requirements engineering they provide the link between
declarative high-level system goals, and operational re-
quirements for the software-to-be [21]. Use case specifi-
cations, which are popular in development processes such
as RUP are also equipped with pre and postconditions. In
design, the notion of design by contract [14] is underpinned
with pre/post conditions. At the code level, the use of asser-
tions to verify at run-time pre/post conditions is considered
good-practice [17].
A pair pre/post condition constitutes a specification that
is local to a specific operation (method, procedure, use case,
event, etc). The precondition is an assertion that is expected
to hold before the occurrence of the operation, the postcon-
dition is an assertion that is guaranteed to hold after the oc-
currence of the operation if the precondition held before the
occurrence. Although writing the pre/post condition for an
operation requires expertise, it is a comparably simple task
compared with writing pre/post conditions for a set of re-
lated operations. Ensuring that the pre/post conditions of a
set of operations of an API are correct requires a cohesive
model of how the various pre/post conditions should fit to-
gether. Validating a use case model requires understanding
how the various use-cases can be combined to provide (and
only provide) the expected software-wide requirements.
Behaviour models such as finite state machines and ac-
tion machines [9] are well founded formalisms that allow
describing the temporal relation between the occurrence of
events. Depending on the context of use, these events can
be interpreted in various ways such as operations, meth-
ods, procedures. Behaviour models are used in require-
ments engineering for providing the expected behaviour of
the software-to-be or of external agents that interact with it.
These models are also used to explain the expected usage
of an API, the expected communication protocol between
processes, or to provide an abstract view of the state space
of a system and how various operations affect it.
Behaviour models are a popular target for synthesising
fragmented behaviour information. They can be synthe-
sised from requirements specifications [11], use cases, and
scenarios [22]. Their intuitive graphical representation and
their executable semantics makes them good choices for
validation. The aim of this work is to support validation
of software engineering artifacts that rely on pre/post con-
ditions as a means for specification by automated construc-
tion and tool-supported analysis of behaviour models.
In this paper we propose a novel technique for construct-
ing behaviour models from contract specifications, i.e. op-
erations specified with pre- and post conditions. Given a
contract, the resulting behaviour model is an abstraction of
all possible implementations that satisfy the contract. The
level of abstraction chosen to construct the behaviour model
can be seen as a generalisation of the pre/post condition
philosophy: A precondition describes the state in which a
specific operation is permissible, we are interested in cap-
ICSE’09, May 16-24, 2009, Vancouver, Canada
978-1-4244-3452-7/09/$25.00 © 2009 IEEE 452