Modern design of hardware and software relies on abstraction to deal with the increasing complexity of systems. Formal models are used as abstract descriptions of the system which provide a precise specification that can already be checked for errors early in the design process. This significantly reduces the costs of correcting these errors. Modeling languages such as the Unified Modeling Language (UML) together with the Object Constraint Language (OCL) provide a broad variety of description means to model the structure and the behavior of a system.
In the following, we will focus on behavioral descriptions by means of class diagrams enriched with OCL constraints.
Here, behavior is modeled in terms of contracts using socalled pre- and postconditions. Although very expressive, these descriptions frequently leave ambiguities about which model properties are supposed to be changed when executing an operation (known as the frame problem). Although first solutions (based on so-called invariability clauses) have been proposed, no automatic approach for the evaluation of the corresponding description means using an interpretation semantic is available yet.
In this work-in-progress report, we propose an idea to address this problem. We first review the problem and discuss related work in the remainder of this section. In order to in 1[T2]h.isInmthoidsewlhoarks, owriegianraelluysibnegena spirmoppolisfieedd ivner[s1i]onanwdhwicahs isfusruthffiercireenfitnfeodr keep the descriptions simple, we avoid a formal definition but the purposes considered here.
In a UML/OCL design flow, class diagrams are used to represent structure. They consist of several classes, which are respectively composed of attributes (representing the information that is stored in the class) and operations (representing possible actions that can be executed in order to change the system state).
The behavior of the system is restricted by OCL statements.
Invariants state general restrictions over the whole system and have to be satisfied in all system states. The behavior of operations is restricted by pre- and postconditions. An operation can only be invoked, if all preconditions evaluate to true; in the following system state, all postconditions must be satisfied.
Example 1: We make use of the running example that is shown in Fig. 1. The model represents an access control system which grants access to buildings for authorized persons.1 The authorization is based on the ID of a magnetic card each person receives. Each building is equipped with turnstiles and card readers to check the card upon entry or exit.
In the following, we focus on the operation checkCard.
This operation models the authentication process using the magnetic card. If an authentication was successful (i. e., the card holder is allowed to get access to a building), access is granted which is indicated by a green light at the turnstile.
Otherwise, no access is granted which is indicated by a red light. Who has access to a building is stored in the attribute authorized; additionally, it is constantly updated who is currently in a building (using the attribute inside). An authentication process can only be started, if no other authentication process is currently running (i. e., both greenLightOn and redLightOn are false). This is accordingly realized in the post- and preconditions.
Turnstile greenLightOn: Boolean redLightOn: Boolean currentlyAuthorized: Integer timeOpen: Integer entry: Boolean goThrough() advanceTime() checkCard(card : MagneticCard)
Although very abstract, UML/OCL models can be used
for validation and verification tasks in early stages of the
design flow. Since implementation details are hidden, these
tasks target common issues at the specification level such as
consistency of models (see, e. g., [
However, in order to validate or verify a certain behavior based on a UML/OCL model, a comprehensive and deterministic description has to be available. This is usually not provided by pre- and postconditions – in particular due to the fact that only changes are described explicitly in the postconditions. What is not restricted in OCL is usually assumed to remain unchanged. However, this is not obvious to the respective approaches for validation and verification.
Example 2: Consider the operation checkCard in the running example. From a designer’s perspective, it may be obvious that this operation is supposed to modify greenLightOn together with currentlyAuthorized or redLightOn only. But from a formal perspective, arbitrary changes may seem valid as well – even critical ones such as changes in the attribute authorized storing who has access to which building. This is, because no postcondition is explicitly restricting the values of these attributes.
Focusing on relevant model properties of course is useful
to maintain comprehensibility of the model. Nevertheless, as
soon as approaches for validation and verification shall be
applied, these ambiguities must be addressed explicitly. It
is essential to know which model properties are eligible to
changes even if these changes are not specified in detail. This
problem is known as the frame problem [
In order to address this problem, further OCL conditions, so-called frame conditions, defining the variability of model properties can be added to the model. In a naïve fashion, this can be conducted by simply adding terms such as model_property = model_property@pre as postcondition for every model property that shall not be changed during the operation call. But obviously this is not practicable for large models undergoing continuous changes during the design process.
Instead, it is often much more elegant to specify model
properties that may change [
Example 3: Consider the model in Fig. 1. As stated before, the designer’s intention is to change only currentlyAuthorized, greenLightOn, and redLightOn when executing the operation checkCard. The following terms ensure this behavior when added to the OCL specification: modi es : self::greenLightOn modi es : self::redLightOn modi es : self::currentlyAuthorized
The application of the modifies (only) construct as given in Example 3 directly leads to another severe problem: In many cases, attribute values only change depending on a particular system state. However, the modifies (only)-construct does not take this into consideration and applies unconditionally.
Example 4: Consider the operation checkCard in Fig. 1. The modifies (only) clauses from Example 3 clearly reduce the ambiguities, but open questions remain. In fact, greenLightOn and redLightOn are restricted by an implication. If the premise of this implication evaluates to false, both attributes can be set arbitrarily.
Consequently, a more sophisticated definition about what
changes are allowed in an operation call is required. Similar
to the modifies (only) clauses, first solutions how to evaluate
and describe that have been proposed in [
Example 5: In the considered example, all postconditions
are implications (i. e., defined using the OCL operator implies).
According to the heuristic interpretation semantics from [
In order to automatically generate constraints that enforce
given interpretation semantics, we propose an approach which
is based on the analysis of the Abstract Syntax Tree (AST)
of a given OCL constraint. Each node of the AST represents
an OCL expression and may have subtrees as successors
(representing the corresponding sub-expressions). This structure
allows us to explicitly employ the heuristics suggested in [
For this purpose, our approach introduces two auxiliary Boolean variables for each node, namely 1) 'i which represents whether the currently considered sub-expression (represented by the AST node) evaluates to true or false, and 2) i which represents whether the model properties used in the currently considered sub-expression (represented by the subtree of the AST node) are supposed to change or not.
Using the AST and these variables, the interpretation semantics can automatically be enforced as sketched in the following example.
Example 6: Consider again the example in Fig. 1. Fig. 2 provides the AST of the postcondition for the operation checkCard.2 This AST is divided into subtrees for every node whose expression relies on an OperationCallExp with Boolean operands.3
2Since a valid call of this operation has to satisfy all postconditions, the single postconditions are combined using an and-operator.
3Other expressions are not handled in this work. But for a complete set of
rules issues such as navigation chains have to be considered as well. Ideas
for such rules have already been proposed in [
Using this AST, the first auxiliary variables are added, e. g., 'i with i = 1; 2; 3. Additional constraints ensure that the assignment of 'i is in-line with the evaluation of the respectively considered expression (with respect to the currently considered system state), e. g., '1 represents the evaluation of the root and-operation and, hence, '1 , '2^'3. Similarly, '2 , J '2 K and '3 , J '3 K are enforced where J 'i K represents the evaluation of the corresponding subtree of the AST.
Next, the i-variables representing the variability of the
model properties contained in the (sub)tree are added.
According to the heuristics from [
For example, for the root node of AST, '1 , 1 has to be satisfied, because the values of model properties should be modified only when the specific operation is called and the operation call is valid – indicated by '1 , true.
As another example (discussed before in Example 5), consider the implies sub-expression, which is marked by '2; 2 in Fig. 2. The left side, marked by '4; 4, represents the premise, which is normally not intended to be changed. This means, that 4 , false and also i , false is propagated to all subtrees, as none of them is supposed to change. The other side of the implication, marked with '5; 5, is only supposed to be changed, if the premise holds, i. e., '4 , true. This means 5 , true iff '4 , true and sets generally greenLightOn, currentlyAuthorized and card.id changeable. However, card.id is a parameter which shall not be changed and currentlyAuthorized saves the authorized id which should be changeable. The variables for all other nodes are set analogously.
Following the sketched scheme, constraints are generated which avoid undesired changes during an operation call. However, this does not entirely solve the task. In fact, so far only the dependencies between 'i and i have been considered, but their connection to the model properties is still missing. In order to do that, two cases have to be considered, namely the given model does not provide any further information or the model is enriched by frame conditions using the modi es (only) scheme reviewed in Section I-B.
If no frame conditions are given, a simple “nothing-elsechanges” heuristic is applied for all model properties that do not occur in the AST. For the remaining model properties m which do occur in the expression, the statement
0 1 is added, where (m) is the set of all i-variables which have to be taken into account for the model property m. It includes all i-variables which correspond to the smallest subtrees containing the respective model property m (and only those ones).
'7; 7 includes authorized building self id card entry self inside building self includes
and greenLightOn self true currentlyAuthorized self id card self
true authorized building self id card In case of given modi es (only) statements, only the model properties mentioned in these statements, which are additionally found to be changeable by our analysis, have to be taken into account.
Example 7: Consider again the AST from Fig. 2. With no additional information, the following set of i and the respective constraints are derived by the analysis, e. g., for card.id:
(card.id) = f 7; 8; 10; 11g :( 7 _ 8 _ 10 _ 11) ) card.id=card.id@pre
This means, that card.id can only be modified, if at least one of the respective i allows for this modification. In case that at least one i allows the modification, the premise evaluates to false due to the negation and card.id stays changeable.
If additionally the modi es (only) constructs are given as introduced in Example 3 for greenLightOn, currentlyAuthorized, and redLightOn, only (m)-sets for these three model properties have to be considered (all other can be ignored). For example, card.id is directly enforced to be unchangeable by adding the respective constraints. This results in the following i-sets and respective constraints: (greenLightOn) = f 9g (currentlyAuthorized) = f 10g (redLightOn) = f 12g
By design, it is impossible that both premises of the two implications evaluate to true. Consequently, either 9 and 10 or 12 can evaluate to true. In the first case, greenLightOn and currentlyAuthorized are changeable while redLightOn is not changeable, and vice versa for the second case. This behavior better fits the designer’s intention, as opposed to an undesired change of greenLightOn and redLightOn within one call.
We extended existing approaches for the generation of frame
conditions (such as [
In this concept, only basic operators were covered, but
some as, e. g., iterator expressions are still missing. However,
these operators can and will be covered by transforming them
into the basic operators. Currently we are implementing this
approach on top of the verification approach proposed in [
Possible direction for future work is to enable the designer to inspect the annotated AST for changing propagations and evaluations of the 'i; i-variables on demand. Besides that, a thorough evaluation of the proposed automatic generation scheme is left for future work.