Behavioral Analysis of UML2 Activity Diagrams (IBM WebSphere Business Modeler process models) with LoLA. We describe how to combine our UML-to-Petri Nets compiler UML2oWFN and our model checker LoLA: A Low Level Petri Net Analyzer in a tool chain for verifying soundness of processes modeled in IBM WebSphere Business Modeler.
Our example is the process model of a coffee machine and its interaction with a customer. You can download the process model in IBM WebSphere Business Modeler .xml format here (file
service-tech.xml). The model contains the following two, almost identical, processes.
You can re-import
service-tech.xml into your IBM WebSphere Business Modeler if you want to, our tools will work directly on the .xml file.
1. Create a directory for setting up the tool chain, e.g.
mkdir uml-analysis cd uml-analysis
2. Download lola-1.15.tar.gz into
uml-analysis/, then unpack, rename, and configure LoLA as follows
tar xzf lola-1.15.tar.gz mv lola-1.15 lola cd lola ./configure cd ..
LoLA is now prepared to be used with UML2oWFN.
3. Download uml2owfn-2.00.tar.gz into
uml-analysis/, then unpack, renaming is optional, configure and compile UML2oWFN as follows.
tar xzf uml2owfn-2.00.tar.gz mv uml2owfn-2.00 uml2owfn cd uml2owfn ./configure make cd ..
make call in
uml-analysis/uml2owfn/ will also invoke
make for LoLA in
uml-analysis/lola/ to build four dedicated LoLA binaries that are needed for analyzing processes. If everything was setup correctly, you will find files
uml-analysis/uml2owfn/lola/. When building under Cygwin, these files will have the
4. Make all created binaries available on the command-line for your analysis. For this example, we propose to set up an analysis directory
uml-analysis/coffeeMachine/ as follows.
mkdir coffeeMachine cp uml2owfn/src/uml2owfn coffeeMachine/ cp uml2owfn/lola/lola-* coffeeMachine/ cd coffeeMachine
Under Cygwin, you will have to add the
.exe extension for the
cp comand. Now the tool chain is ready for use. Download the example file service-tech.xml to
uml-analysis/coffeeMachine/ to begin with the analysis.
This tool chain begins with translating the original process model into Petri nets with UML2oWFN. Invoke the following command:
./uml2owfn -i service-tech.xml -f lola -a soundness -a safe -a orJoin -p ctl -o
You will get a line saying
2 of 2 processes have been translated. and you will see 6 new files
.lola files are Petri nets that have the same behavior as the original process models, the
.task files describe correctness properties these nets have to fulfill.
If you want to inspect the Petri nets, you can either use our editor Seda or use UML2oWFN to generate a
.png file that shows the Petri net (this requires GraphViz dot to be available on your system). Invoke
./uml2owfn -i service-tech.xml -f dot -a soundness -a safe -a orJoin -o
to get the two graphical representations of the processes as shown on the right.
There are more output formats available, see the Manual for details.
In the last step, we generated files that are a compatible input for LoLA. The
.lola files describe a Petri net in LoLA syntax. The
.task files describe behavioral properties of the net.
.lola.fin.task describes that the process must always be able to reach a valid final state, i.e. that it has no deadlock. The
.lola.safe.task describes that the process must not reach a state that allows him to execute the same task twice, i.e. that the process has no lack of synchronization. In Petri net terms, we require that no place of the net may have more than one token, i.e., that the Petri net is safe. Both properties are checked separately by LoLA with dedicated routines.
To check all of these properties for all of the nets, invoke
sh ./check_service-tech.sh ./ &> ./results_service-tech.log
which will call for each process and each property the respective LoLA binaries. Note the parameter
./ to the shell script which points to the location of the LoLA binaries.
All output is written to the file
./results_service-tech.log. From there, analysis results can be parsed and interpreted. We now explain in detail how LoLA is invoked for each analysis and how the analysis results are interpreted. A method for automatically running this tool chain with translation, analysis and result interpretation is explained in the UML2oWFN manual.
To verify that a process can always terminate, we use
./lola-mc service-tech.Prcsss__coffeeMachine_sound.lola \ -aservice-tech.Prcsss__coffeeMachine_sound.lola.fin.task -P
to verify the first coffee machine process. (Note that between parameter switch
-a and the subsequent file name is no space.) As a result you will get the following print out
44 Places 36 Transitions 35 significant places Formula with 48 subformulas and 2 temporal operators. result: true >>>>> 159 States, 475 Edges, 159 Hash table entries NO PATH
result: true tells us that the process indeed can always reach a valid final state.
If you verify the second coffee machine process with
./lola-mc service-tech.Prcsss__coffeeMachine_unsound.lola \ -aservice-tech.Prcsss__coffeeMachine_unsound.lola.fin.task -P
then you will get
41 Places 35 Transitions 34 significant places Formula with 45 subformulas and 2 temporal operators. result: false >>>>> 44 States, 55 Edges, 44 Hash table entries PATH process.Prcsss##coffeeMachine_unsound.inputCriterion.Input_Criterion fork.Fork.activate.Input_Branch_ fork.Fork.fire.Output_Branch_1 fork.Fork.fire.Output_Branch_2 task.insert_coin.inputCriterion.Input_Criterion task.insert_coin.outputCriterion.Output_Criterion task.await_coin.inputCriterion.Input_Criterion task.await_coin.outputCriterion.Output_Criterion decision.beverage_selection.activate.Input_Branch_ decision.beverage_selection.fire.Output_Branch_2 decision.choose_beverage.activate.Input_Branch_ decision.choose_beverage.fire.Output_Branch_1
which tells that the process is not sound and provides an error trace in the Petri net to a state from which on it is impossible to reach a valid final state.
To verify that a process has no lack of synchronization, we use
./lola-sp service-tech.Prcsss__coffeeMachine_sound.lola \ -aservice-tech.Prcsss__coffeeMachine_sound.lola.sound.task -P
The resulting print out should read like this.
44 Places 36 Transitions 35 significant places Formula with 3 subformula. predicate is not satisfiable! >>>>> 42 States, 48 Edges, 42 Hash table entries
predicate is not satisfiable! tells us that the process has no lack of synchronization as LoLA tries to find a state that witnesses the violation of that property. You will get the same result for the unsound coffee machine.
The error trace which we obtained in the the deadlock verification can be mapped back to the original model based on the Petri net transitions mentioned in the trace and their originating tasks in the original process model. This mapping has to be done manually; the following figure illustrates the above error trace (only solid red lines) in the original model.
The problem can be solved by replacing the independent XOR-choice of the coffee machine by a choice that depends on the input from the customer. In UML, this requires using input pinsets and output pinsets on the choosing task. This has been done in the sound coffee machine for task
beverage selection as follows:
tea orderand the control-flow link activate the output
tea orderand the upper control-flow link
coffee orderand the control-flow link activate the output
coffee orderand the lower control-flow link.
This yields the Petri net pattern on the right. With this process logic, the coffee machine process is sound.