UML2ALLOY | |||||||||
|
What is
UML2Alloy
UML2Alloy is the outcome of a research which attempts to formalise UML using Alloy. UML is the De Facto modelling language that is used by the industry to model mainly software systems. UML is diagram based. OCL is a textual notation that is used to impose constraints over the UML model. However users of those notations are not able to reason about the soundness of their models, before the model is implemented. This happens because of the semi-formal nature of UML. On the other hand users who are acquainted with formal methods are able to specify models in a formal notation (e.g. Z) and reason about certain properties. The drawback of formal methods is the fact that they are not easy to learn and understand. UML2Alloy bridges this gap between the popularity and semi-formalism of UML. Using UML2Alloy users are able to use two critical functionalities of the Alloy Analyzer simulation and verification. Simulation increases the confidence of the validity of a model and verification enables modellers to reason that certain critical properties of the model are satisfied. Technical InformationThere is a diversity of UML CASE software in the market. In order to enable modellers use the CASE tool of their preference, UML2Alloy can import a UML model from an XMI file. However in order to reduce the development time, the ArgoUML Model Facade was used in order to parse XMI files. This means that UML2Alloy is only able to parse XMI 1.0 format files at the moment. For the parsing of OCL statement the Dresden OCL compiler was used. For the development of the skeleton of the program from the UML model, OCL Environment 2.0 was used. User ManualThe verification is accomplished in the simple way that is depicted in Figure 1. The modeller generates the UML model in a UML CASE tool and exports it in XMI format. The file that contains the XMI format is passed to the UML2Alloy core engine, which generates a representation in the Alloy language. Then Alloy Analyzer is used to perform analysis (simulation and verification).
Figure 1: Steps required to accomplish verification.
In the main screen of UML2Alloy, users can select the XMI file that contains a representation of their UML model and the path of the Alloy file that will contain the Alloy model after the parsing of the XMI file has finished.
During the process of translation users are required to enter some more information. In Alloy there are two main categories of expressions, Facts and Predicates. Facts are statements that have to always hold for every instance of the model. Predicates are expressions which can be simulated. For more information please consult the Alloy reference manual. By default UML2Alloy translates operations that contain pre and post conditions to predicates and invariants to Facts. However users are allowed to change it. Users must also specify which operation of the model will be used for simulation or verification. Finally users have to specify whether the predicate selected in the previous screen contains expressions that are used for simulation or verification. Moreover the number of instances of the model elements that will be created has to be specified. In the context of a simulation this is the number of instances of each model element that users will be able to see. In the context of verification it is the number of instances that will be searched by Alloy in order to find if the expression of the predicate is satisfied. If the expression is not satisfied a counter example will be presented (an instance of the model that does not satisfied the assertion).
After the parsing procedure has been finished the Alloy Analyzer tool is used in order to "build" and "execute" the model.
LimitationsThis first release of UML2Alloy has some limitations.
DownloadThe compressed file can be downloaded from here (uml2alloy.tar.gz 6,2 MB). UML2Alloy distribution is a large file because of the external libraries that are used. For example ArgoUML is about 5,5 MB. InstallationUnpack the compressed file of the distribution to a folder. Depending on the platform edit the run_windows.bat or run_linux.sh files and make the necessary changes to the path variables. The program can be started by executing the run_windows or run_linux files respectively. LicenseUML2Alloy is distributed free of charge are supplied "as is", without
expressed or ExampleUML2Alloy has been used to model an industrial Discrete Event System. DescriptionConsider a system consisting of two independently driven, independently controlled axes; a Drum and a Slider. Bottles are delivered into the Drum from another section of the machine. The Drum which has a rotational movement carries the bottles into the Slider, which caps each bottle. After capping a bottle, it is delivered out of the system.
A model of the system has been created using UML. The model has then been translated to Alloy and checked using Alloy Analyzer. UML Model The Drum has one attribute position of type enumeration d_pos, which is defined as a separate “Custom Data Type” class. The Drum carries the bottles by rotating D.position = D_Rot and when a bottle is at a suitable position to be capped the Drum goes stationary D.position = D_Sta. For the capping to take place, the drum must remain stationary (Stationary Committed) D.position = D_Sta_Com. Following that state, a rotating phase is completed: D.position = D_rotate_complete. Similarly, the Slider has an attribute position. A cycle of movement of the Slider starts by its approaching to the Drum S.position = S_App. To achieve the maximum output of the system, the Slider approaches the Drum with maximum speed. If the slider and Drum are synchronised, i.e. if a bottle is at its suitable position D.position = D_Sta_Com, the slider proceeds its movements and caps the bottle. This is modelled as the S.position = S_insert. However, if the Slider and the Drum are not synchronised, when the Slider arrives at decision point (S.position = S_Dpos), which considering the momentum of the movement of the Slider, is the last point that the Slider can abort its movement. At the decision point, if insert is not possible, the Slider aborts (S.position = S_abort) and waits for the Drum to catch up. Then when the Drum and Slider are syncronised, the Slider can insert S.position = S_insert. Following the insert, the approach phase is complete (S.position = S_approach_complete). Then the Drum and the Slider get engaged, i.e. the bottle is capped. This is followed by a reverse movement of the Slider, resulting in the Slider being clear of the drum S.position = S_cod (clear of drum). At this stage the motion of the Slider has completed (S.position = S_motion_complete)
The UML model of the system in ArgoUML (version 0.16) format can be found here. Alloy Model Simulation The following picture shows the first two states of a simulation of the model by Alloy. The first state (State_0) shows the values of the attributes of the system according to our initial condition and the second state (State_1) shows how the system evolves from the original state.
The produced Alloy for the simulation can be found here. Safety The automatically generated Alloy code that checks the safety property is the following one (in a future version of UML2Alloy pretty printing functionality will be intergraded): assert safety
{
(
no s: State |((
( (
( (
s.syn.controls_s.position= s_insert
) ) && ( (
s.syn.controls_d.position= d_Rot
) )
) )
)
) )
}
The produced Alloy model can be found here. Liveness In order to check the liveness property of the system we tried to check if a statement that falsifies that property is correct. In particular we asserted that there is no state of the system where the slider is inserting. A counter-example was presented verifying that our assertion is wrong (i.e. there is a state where the slider is going to insert the drum) The automatically generated Alloy code is the following: assert liveness
{
(
no s: State |((
( (
( (
s.syn.controls_s.position= s_insert
) )
) )
)
) )
}
The following picture shows the counter-example presented by Alloy. It is clear that in State_4 there is a snapshot of a slider inserting the Drum. The produced Alloy model can be found here.
|
