Publications

Symbolic program manipulation plays a key role in program comprehension and verification. Logic formulae are used to represent the program' s state and transformation rules describe the effect of statement executions on the program's state. A well-known problem arises in the case of loops, since the number of iterations is generally unknown. The effect of a loop is therefore abstracted into a loop invariant, whose derivation cannot in general be automated and requires human ingenuity. In this paper, we present a preliminary approach that in tegrates genetic programming into the synthesis of invariant formula that describes the behavior of a loop. We present a specific representation of formulae that works well with loops manipulating arrays. The technique has been validated with a set of relevant examples with increasing complexity. The preliminary results are promising and show the feasibility of our approach.

We focus on the problem of searching components based on semantic queries on their provided interface. Although semantics-based search has long been advocated as a key enabler in the context of component-based software development and, more recently, service-oriented computing, no practical and scalable approach has been proposed yet. This paper presents a promising model-based search technique for interface behaviors based on operational specifications, called behavioral equivalence models (Bems). Semantic queries are expressed equationally, following an algebraic specification style. The search engine tries to match specifications against queries. This can be done quite efficiently by encoding Bems into relational models and queries into relational logic formulae, whose satisfiability is checked with the SAT-based constraint solver KodKod. We can report on an initial very promising assessment of the proposed technique, which has been applied to searching components in Java libraries providing container functionalities.

The problem of formal software specification has been addressed and discussed since the infancy of software engineering. However, among all the proposed solutions, none is universally accepted yet. Many different formal descriptions can in fact be given for the same software component; thus, the problem of determining the consistency relation among those descriptions becomes relevant and potentially critical. In this work, we propose a method for comparing two specific kinds of formal specifications of containers. In particular, we check the consistency of intensional behavior models with algebraic specifications. The consistency check is performed by generating a behavioral equivalence model from the intensional model, converting the algebraic axioms into temporal logic formulae, and then checking them against the model by using the NuSMV model checker. An automated software tool which encodes the problem as model checking has been implemented to check the consistency of recovered specifications of relevant Java classes.

This paper describes an approach (SPY) to recover the specification of a software component from the observation of its run-time behavior. It focuses on components that behave as data abstractions. Components are assumed to be black boxes that do not allow any implementation inspection. The inferred description may help understand what the component does when no formal specification is available. SPY works in two main stages. First, it builds a deterministic finite-state machine that models the partial behavior of instances of the data abstraction. This is then generalized via graph transformation rules. The rules can generate a possibly infinite number of behavior models, which generalize the description of the data abstraction under an assumption of “regularity” with respect to the observed behavior. The rules can be viewed as a likely specification of the data abstraction. We illustrate how SPY works on relevant examples and we compare it with competing methods.

This paper proposes an approach for the specification of the behavior of software components that implement data abstractions. By generalizing the approach of behavior models using graph transformation, we provide a concise specification for data abstractions that describes the relationship between the internal state, represented in a canonical form, and the observers of the component. Graph transformation also supports the generation of behavior models that are amenable to verification. To this end, we provide a translation approach into an LTL model on which we can express useful properties that can be model-checked with a SAT solver.

Specification recovery is a necessary step of many reverse engineering and reuse efforts. This paper deals with recovering the semantic part of a component's interface. It focuses on stateful components that provide data abstractions. Recovery is achieved by following a black-box strategy, i.e. by observing the component's dynamic behavior. Among the published approaches, Heureka recovers algebraic specifications from Java classes. Another approach (Adabu) recovers behavioral models. The work we describe here adapts the latter, which provides an approximate semantic description for the class, to significantly optimize the former. The resulting approach, called Adiheu, is described in the paper with a preliminary assessment.