Case Study: PersonCar

System structure

Figure 1 show the class diagram of a very simple system with two classes: Person and Car. A person owns the operation drive(). A car owns two attributes: started : Boolean and passengers : Person[*] that specify when a car is started list of passengers in the car, respectively. On the other hand, it is possible to get into a car, by calling the operation getOn(person) and start it (start()).

Figure 1 : Class diagram PersonCar

The classes are defined in Maude as follows:

Code 1 : Fragment of the code generated by the mapping.

Code 1 is a fragment of the code generated for the class diagram of the example PersonCar. The translation do not keep the generated constructors ordered. That is, though the code is readable, is possibly does not match the order in which a human programmer would have written them. That is due to the fact that in Maude the order of rules in Maude is not relevant and thus is not defined in the Maude metamodel. In the order of the constructors is not defined in the metamodel, a model has not information about the order and is impossible to generate the corresponding code ordered.

For the attributes and associations the particular representation of mOdCL is used, using the OCL types. For each attribute or association, a constructor is generated:

where AttributeName is the name of that attribute or association in the class diagram. For the example PersonCar the following attributes and associations are defined:

Finally, the operations and its parameters are specified in a similar way. For the name of an operation, a constant of type OpName is created and each argument is specified as a constant of type Arg:

For the example PersonCar and the operations defined in it, the following operations are automatically generated:

System behavior

As a case study, the operation Person::drive() will be specified.

Figure 2 : Sequence diagram of the operation drive.

In the sequence diagram shown in Figure 2, the association person_owns_car is defined and two lifelines are defined: PPers and CCar. Both lifelines correspond to the classes Person and Car, respectively.

The first message of the sequence, with the signature shown in Figure 2, (the signature with which the operation has been defined in the class diagrams), and with name "1:getOn", owns an argument corresponding to the parameter person. The argument's name is the parameter and its body is the instantiated variable, self.

The following Maude code must be generated for the operation Person::drive():

Code 2 : Code generated by the transformation from sequence diagram of the operation drive.

In order to represent the mapping between each element in the sequence diagram in Figure 2 and Code 2, in Figure 3 the main associations are shown.

Figure 3 : Correspondences between sequence diagram and code generated of the operation drive.

Figure 3 shows how a Maude rule is generated for each message. Both rules meet the skeleton shown in the description of the mapping:

The diagram must be complete for the code to be executable. Thus, each operation called by means of a synchronous call must be specified in its corresponding diagram. For example, Figure 4 show the specification of operation getOn and Figure 5 shows the specification of operation start.

Figure 4 : Sequence diagram of the operation getOn.
Figure 5 : Sequence diagram of the operation start.
Figure 6 : Sequence diagram of the operation setC.

Modifying attributes by OCL expressions

Both the semantics of the operation Car::getOn(Person) and of the operation Car::start() require the object state to be modified. For both operations, a Message Found must be created to defined the called being created. In this Message Found there must an argument for each modified attribute. Each argument will be an object of type OpaqueExpression with the attribute to be modified as name and the required mOdCL expression as body.

These arguments will be mapped to expressions of type eval, whose result will be stored in the corresponding attribute of the object Self present in each rule.

Figures 4 and 5 can be taken as examples, where the diagrams for operations Car::getOn(Person) and Car::start() are shown.

Running the case study

For the example PersonCar, an initial state could be the following one:

Code 3 : Initial state PersonCar.

As many invariants as you may wish can be defined on a class diagram. This way, the following invariant could be defined to check that if a car is started, it must have some passengers:

The previous invariant can be checked over the initial state of Code 3 with the following call:

reduce in PERSONCAR-VALIDATION-TEST : eval(CarEmptyStopped, init-state) .
rewrites: 87 in 1924028793ms cpu (0ms real) (0 rewrites/second)
result Bool: true

This way, it is possible to complete the specification restricting certain states that should be unreacheable. If all those invariants are added to the equation inv, the evaluator will check those invariants in all the system states.

To execute the initial state of Code 3 over the Maude specification of operation Person::drive() it is necessary to add the message call. Next, the initial code that starts the execution of the operation Person::drive() is shown (take into account that the state specified in Code 3 is used):

To check the correctness of the model, the inital state of Code 3 can be executed in order to achieve the next state:

{ resume(drive, null) < stack : Stack | state : nil > < jane : Person | none > < tony : Person | car : ferrari > < paul : Person | none > < ferrari : Car | started : true,passengers : Set{tony} >}


Maude codes
Papyrus project

Last modification: 3rd September, 2013