Lightweight Verification of Executable Models

Tweet about this on TwitterShare on FacebookBuffer this pageShare on RedditShare on LinkedInShare on Google+Email this to someone

Related to the previous post on the static verification of transformations, now Elena explains how to check the quality of your executable UML models for instance written using the recent “Foundational Subset for Executable UML Models” (fUML) standard we have presented  and summarized here before

Given the increasing importance of executable models, the existence of methods to verify the correctness of such models is becoming crucial (specially when you think that one of the MDD goals is to be able to generate code from those models so if the models are wrong, then, well the code would be useless) .

We have developed some lightweight verification techniques (check this paper , to be presented at ER 2011 conference and co-authored by Elena Planas, Jordi Cabot and Cristina Gómez) for executable models. Why lightweight? Simply we believe it’s better to provide some useful information today than a more complete one in two years (time that takes to verify your model using other dynamic approaches for non-trivial scenarios 🙂 )

Our method focuses on the verification of the strong executability correctness property of action-based operations specified in Alf Action Language. We consider an operation is strongly executable if it is always successfully executed, i.e. if every time we execute the operation (whatever values are given as arguments for its parameters), the effect of the actions included in the operation evolves the initial state of the system to a new system state that satisfies all integrity constraints of the structural model. This is one of the most fundamental correctness properties for behavioural specifications. When we know that all operations are strongly executable, we can avoid checking at the end of each operation execution if all constraints are satisfied which improves the efficiency of the system.

As an example, consider the operation “newProduct” (which creates a new product in the system) according to the class diagram and integrity constraints showed in Figure 1:


(1) activity newProduct (in code:String, in price:Real, in specialPrice:Real, 
     in description:String, in substitutedProducts:Product[0..*]){
(2)   p = new Product();
(3)   p.code = code;
(4)   p.price = price;
(5)   p.specialPrice = specialPrice;
(6)   p.description = description;
(7)   for (i in 1.. substitutedProducts->size()) {
(8)     CanBeSubstitutedBy.createLink(p1=>self,p2=>substitutedProducts[i]);
(9)   }
(10) }

Operation “newProduct” is not strongly executable since, every time it is executed, several errors may arise:

  • Error 1: The productPrimaryKey constraint may be violated when the attribute code of the new product is initialized (line (3) of “newProduct”).
  • Error 2: The specialPrice constraint may be violated when the attribute specialPrice is initialized with a value greater than price (line (5) of “newProduct”).
  • Error 3: The symmetricAssociation constraint may be violated if the symmetric link between the product and the substituted product is not created.

A relevant feature of our method is the feedback it provides: it returns either a positive answer (meaning that the operation is strongly executable) or a corrective feedback otherwise. This corrective feedback consists in a set of actions and conditions that should be added to the operation in order to make it strongly executable.

For instance, the feedback provided when verifying the operation “newProduct” is:

  • To avoid violate the Error 1, the operation must satisfy one of these conditions:
    • Option 1: Must exist a guard (i.e. conditional structure) which ensures the initialization of the attribute code will only be executed when there is not another product with the same code.
    • Option 2: Must exist a product with the same code and its value is modified.
    • Option 3: Must exist a product with the same code and this product is destroyed.
  • To avoid violate the Error 2, must exist a guard which ensures the initialization of the attribute specialPrice will only be executed when specialPrice<price.
  • To avoid violate the Error 3, must exist a creation of the symmetric link of type CanBeSubstitutedBy between objects substitutedProducts[i] and self.

In the following we show the repaired operation “newProduct” once one possible reparation of the feedback provided by our method has been integrated (the added sentences are colored in green):


(1) activity newProduct (in code:String, in price:Real, in specialPrice:Real, 
           in description:String, in substitutedProducts:Product[0..*] sequence){
(2)   if ( not Product::allInstances()->exists(p|p.code=code) ) {
(3)     if ( specialPrice  price) { 
(4)       p = new Product();
(5)       p.code = code;
(6)       p.price = price;
(7)       p.specialPrice = specialPrice;
(8)       p.description = description;
(9)       for (i in 1.. substitutedProducts->size()) {
(10)        CanBeSubstitutedBy.createLink(p1=>self,p2=>substitutedProducts[i]);
(11)        CanBeSubstitutedBy.createLink(p1=>substitutedProducts[i],p2=>self);
(12)      }
(13)    }
(14)  }
(15) }

Another relevant feature of our method its efficiency: our method performs an static analysis without any need to execute/simulate the operations in order to determine its executability. For more information about how our method computes strong executability property in a static way, please, read the complete paper

Tweet about this on TwitterShare on FacebookBuffer this pageShare on RedditShare on LinkedInShare on Google+Email this to someone
Comments
  1. Bruel
  2. jordi
    • jordi

Reply

Your email address will not be published. Required fields are marked *