Software modelers refactor their design models to improve design quality while preserving essential functional properties. Tools that allow modelers to check whether their refactorings preserve specified essential behaviors are needed to support rigorous model evolution. In this paper we describe a rigorous approach to analyzing design model refactorings that involve changes to operation specifications expressed in the Object Constraint Language (OCL). The analysis checks whether the refactored model preserves the essential behavior of changed operations in a source design model. A refactoring example involving the Abstract Factory design pattern is used in the paper to illustrate the approach.
In Model-Driven Development (MDD) projects, one can expect design models
to evolve as developers explore design spaces for high quality solutions. Class
models are among the most popular models used in practice and given their
pivotal roles, there is a need to manage their evolution. Software refactoring
[
The model on which a refactoring is performed is called the source model, and the model produced by the refactoring is called the refactored model. A refactoring that involves making changes to operation specifications is called a behavioral refactoring. In this paper, we present an approach to analyzing behavioral refactorings to check that changes to operation specifications preserve the net effect of the operation (i.e., its essential behavior) as specified in the source model. The net effect of an operation can be expressed using the OCL pre-/post-conditions.
As an example, consider a case in which the operation F lightM anager :: bookF light() in a flight reservation system class model is refactored into the following four operations in the refactored model: Airline :: getAvailableF lights() returns all flights that are available on a given day and airport, F light :: getAvaila− bleSeats() returns all seats that are available on the flight on a given day and airport, F light :: reserveSeat() reserves a seat on the flight, and F lightM anager :: bookF light() books a flight by calling the previous three operations. The net effect of the F lightM anager :: bookF light() operation in the source model is specified using an OCL pre-/post-condition stating that if there exists available flight seats, at the end of the operation execution a seat will be reserved by a flight manager. The behavioral refactoring performed on the source model redistributes the functionality of F lightM anager :: bookF light() across different classes (i.e., Airline, F light, and F lightM anager). It is tedious to manually determine if the above behavioral refactoring preserves the net effect of the original operation because it involves manually building a description of the global net effect of a behavior by composing operation specifications that define subbehaviors in local contexts (i.e., classes in which the operations are located).
The above motivates the need for an automated analysis technique that supports rigorous analysis of behavioral refactorings. In the approach described in this paper, an analysis of a behavioral refactoring involves determining whether a sequence of operations in the refactored model preserves the net effect of an operation in the source model. The net effect of a source model operation is preserved by a sequence of refactored operations if the sequence starts in all the states that satisfy the pre-condition of the source model operation, and leaves the system in a state that satisfies the post-condition of the source model operation. The analysis approach requires the software modeler who performed the behavioral refactoring to provide a sequence diagram that describes the sequence of refactored operations. The approach takes the sequence of refactored operations, applies all the states that satisfy the pre-condition of the source model operation, and checks if the sequence of refactored operations produces any state that does not satisfy the post-condition of the source model operation. The net effect of the source model operation is not preserved by a sequence of refactored model operations if the sequence of refactored model operations starts in a state that satisfies the pre-condition of the source operation and produces a state that does not satisfy the post-condition of the source model operation.
The Alloy Analyzer [
The approach described in the paper is lightweight in that (1) it does not expose the modeler to any formal notation other than the OCL, and (2) the net effect preservation analysis is checked within a bounded domain. More heavyweight formal analysis techniques are needed in a setting where the net effect preservation checking requires more exhaustive analysis.
The rest of the paper is organized as follows. Section 2 provides an overview of the approach and Section 3 illustrates its use on a small example. Section 4 presents a research prototype to support the analysis approach. Section 5 describes related work, and Section 6 concludes the paper. 2
The analysis approach is used to determine whether the net effect associated with a behavior specified in a source model can be preserved by distributed behaviors specified in a refactored class model. The net effect preservation property that is checked is defined as follows:
Definition 1: Net Effect Preservation. A sequence of operation invocations, OpSeq, in a refactored model is said to preserve the net effect of an operation, Op0, in the source model if the set of net effects (i.e., start and end system states associated with an operation invocation) characterized by the specification of Op0 is included in the set of net effects (i.e., start and end system states associated with a sequence of operation invocations) characterized by the sequence OpSeq. More precisely, a set of operations specified in a refactored model, {Op1, Op2, ..., OpN }, is said to preserve the net effect of an operation Op0 specified in the source model if there exists an invocation sequence of the refactored model operations, OpSeq = [Op1; Op2; ...; OpN ], such that the following holds: 1. OpSeq starts in all the states that satisfy the pre-condition of Op0. 2. If OpSeq starts in a state that satisfies the pre-condition of Op0 then the sequence of operation invocations leaves the system in a state that satisfies the post-condition of Op0.
The analysis approach requires a software modeler to provide the following as inputs: 1. The specification of the source model operation, Op0, that is refactored. 2. The result of a refactoring (i.e., a refactored class model), and a sequence diagram that describes how Op0’s redistributed behavior is used. The sequence diagram provides the sequence of refactored operations that will be analyzed against the source model specification of Op0.
The intermediate output of the approach is an analyzable model that can be used to check the net effect preservation property between Op0 and OpSeq. In this approach, the analyzable model takes the form of an Alloy model that is produced from (1) the refactored class model, and (2) a sequence diagram that describes OpSeq.
The specifications for Op0 and the operations involved in OpSeq are also included in the Alloy model. The inclusion of Op0 in an Alloy model produced from the refactored class model can be problematic when Op0 refers to elements not included in the refactored model. For this reason the first step of the approach checks that the elements referenced in the Op0 operation specification also appear in the refactored model.
The second step of the approach generates the base Alloy model that is
extended in following steps to check the preservation property. We use a
UMLto-Alloy transformation that builds upon our previous work on rigorous analysis
of UML class models [
The third step of the approach takes as input the specification of Op0 and a sequence diagram, and produces an Alloy assertion (or predicate) that is used to determine whether the sequence described in the sequence diagram (OpSeq) preserves the net effect of Op0. The assertion (or predicate) is added to the Alloy model generated in the second step of the approach. If a check of the assertion (or predicate) by the Alloy Analyzer produces an Alloy instance then the net effect specified by Op0 cannot be preserved by the operation sequence.
More details on the major steps of the approach can be found in [
A maze game class model from [
The operation createBombedMaze() in class M azeGame is used to create a bombed maze that consists of four walls. Its net effect in the form of OCL specification is given below:
// Pre-condition: no maze has been created
// Post-condition: a bombed maze has been created, and it includes a room
// with four walls
Post: result.oclIsNew() and self.maze.bRooms→size() = 1 and
self.maze.bRooms→forAll(r : RoomWithBomb | r.bwalls→size() = 4)
If a new type of maze, maze room, door or wall were added, the structure of the
class model would need to be changed significantly. Incorporating the Abstract
F actory pattern [
Fig. 1: Maze Game Class Model
Fig. 2: Refactored Maze Game Class Model createM aze(f : M azeF actory) : M aze operation, that uses a factory to create a specific type of maze. The net effects of the original operations in M azeGame need to be preserved by the behavioral refactoring. The analysis approach described in this paper can be used to check if the net effect of createBombedM aze is preserved by relevant operations in the refactored model.
The OCL specifications for createM aze and addRoom are given below:
// Pre-condition: a maze factory has been associated with a maze game
Post: true
// Pre-condition: a room has not been associated with a maze
// Post-condition: a room has been associated with a maze
Unlike the createBombedM aze operation, the createM aze operation
delegates its responsibility to other operations (i.e., makeM aze, makeRoom,
addRoom, makeW all, and addW all) in the refactored class model. Due to space
limitations, only the specifications of createM aze and addRoom are given in the
paper (see above). More operation specifications can be found in [
The analysis showed that if we removed an operation (e.g., addRoom) from the operation sequence in Fig. 3, the net effect of createBombedM aze cannot be preserved by the rest of operations in Fig. 3. We also used the same analysis approach to check if the net effects of other source model operations are preserved by refactored model operations. Our analysis results showed that all the operations in the source model (e.g., createEnchantedM aze, createRoomW ithBomb, createEnchantedRoom, createOrdinaryW all and createBombedW all) can be preserved by relevant operations in the refactored model. 4
We developed a research prototype to investigate the feasibility of developing tool
support for the approach. The prototype consists of an Eclipse OCL parser, an
Ecore/OCL transformer and an Alloy Analyzer. The Ecore/OCL transformer is
developed using Kermeta [
The inputs are automatically transformed to an Alloy model consisting of signatures and predicates. The prototype then uses the APIs provided by the Alloy Analyzer to pass the Alloy model to the Alloy SAT solver. The result returned by the Alloy SAT solver is interpreted by the prototype. The interpreted result provides the net effect preservation property between Op0 and OpSeq.
The prototype implementation uses a visitor pattern to transform a class
model with operation specifications into an Alloy model. The traditional
visitor design pattern keeps the separation of the structure (i.e., the metamodel
elements) and the behavior (i.e., the visitor) by using a specific class for the
visitor, and thus results in ping-pong calls between the objects of the structure
and the objects of the visitor. The Kermeta [
Two broad categories of related work are discussed in the section: work on model refactoring and work on UML-to-Alloy transformation. 5.1
Model Refactoring
Refactoring has attracted much attention from the MDE community since it
was first introduced by Opdyke in his PhD dissertation [
Both Sunye et al. [
France et al. [
Straeten et al. [
However, based on our knowledge, none of the above approaches can be used to analyze operation-based model refactoring that involves changes to operation specifications. 5.2
UML to Alloy Transformation
Georg et al. [
Dennis et al. [
Anastasakis et al. [
Maoz et al. [
We presented an approach to rigorously analyzing a behavioral refactoring that involves making changes to operation specifications expressed in the OCL. The behavioral refactoring analysis involves checking whether relevant operations in the refactored model can preserve the net effects of the operations targeted by the refactoring in the source model. The net effect preservation checking technique described in the paper builds upon the Alloy Analyzer and thus requires a translation from UML class models and OCL operation specifications to Alloy models. We developed a prototype for transforming UML+OCL models to Alloy models with traces to support the net effect preservation check. We applied the approach to a pattern-based model refactoring to demonstrate how software modelers can use the approach to analyze a behavioral refactoring.
We plan to extend the behavioral refactoring analysis approach by providing support for more complex OCL operators. Specifically we are currently investigating how we can use SMT solvers (e.g., Microsoft Z3) at the back-end to analyze the OCL specifications. Our future work will also explore how mappings between equivalent source and refactored forms can be used to support the net effect preservation checking.
The work described in this report was supported by the National Science Foundation grant CCF-1018711.