===== Archimate to NuSMV (nuXmv) =====
:!: Updated to Archi 4.7.0 (12.07.2020)
//Archimate to NuSMV// is a plugin to popular [[http://www.archimatetool.com/|Archi editor]].
The plugin examines business processes embeded within the Business layer and builds a model suitable for model checking with NuSMV or nuXmv.
Example Archimate process
{{::archimate_preparation.png|}}
{{:archimate_finalization.png|}}
Generated code NuSMV (nuXmv). In the following example FSM (interleaving) semantics is used for processes and synchronous for other elements. This kind of options can be configured by editing the [[archi_to_nusmv#controlling_model_generation|properties file]].
-----------------------------------------------------------------------------------
-- Automatically generated NuSMV specification from ArchiMate model: Agreement
-- ArchiMate to NuSMV (c) 2015 Piotr Szwed
-- http://home.agh.edu.pl/~pszwed/en/doku.php
-----------------------------------------------------------------------------------
MODULE main
VAR
And_Junction : andFork(Acceptance.outflag);
Rejection : event(Acceptance.excptflag2);
AndJunction_Before_And_Junction_0 : andJoin(Signing_by_Sales.outflag,Signing_by_Client.outflag);
Timeout : event(Acceptance.excptflag1);
And_Junction_1 : andJoin(Scan_Signed_Contract.outflag,Implementation.outflag);
Start : event(Start_trigger);
Acceptance : atomicProcess2(Junction.output);
Signing_by_Sales : atomicProcess(And_Junction.outflag);
And_Junction_0 : andFork(AndJunction_Before_And_Junction_0.outflag);
Prepare_Contract : atomicProcess(Terms_Negotiation.outflag);
Contract_Prepared : event(Scan_Proposal.outflag);
Implementation : atomicProcess(And_Junction_0.outflag);
Stop : event(And_Junction_1.outflag);
Terms_Negotiation : atomicProcess(Junction_Before_Terms_Negotiation.output);
Junction : xorJoin(Contract_Prepared.outflag,Reminder.outflag);
Scan_Proposal : atomicProcess(Prepare_Contract.outflag);
Signing_by_Client : atomicProcess(And_Junction.outflag);
Reminder : atomicProcess(Timeout.outflag);
Junction_Before_Terms_Negotiation : xorJoin(Present_Product.outflag,Rejection.outflag);
Scan_Signed_Contract : atomicProcess(And_Junction_0.outflag);
Present_Product : atomicProcess(Start.outflag);
Start_trigger : boolean;
ASSIGN
init(Start_trigger) := FALSE;
next(Start_trigger) := {FALSE,TRUE};
--------- Automatically generated SPECs -------------
SPEC
AG( Start.outflag -> AF( Stop.outflag & Timeout.outflag & Rejection.outflag))
SPEC
AG( Start.outflag -> AF( Stop.outflag | Timeout.outflag | Rejection.outflag))
SPEC
AG( Start.outflag -> EF( Stop.outflag & Timeout.outflag & Rejection.outflag))
SPEC
AG( Start.outflag -> EF( Stop.outflag | Timeout.outflag | Rejection.outflag))
SPEC
EG( Start.outflag -> AF( Stop.outflag & Timeout.outflag & Rejection.outflag))
SPEC
EG( Start.outflag -> AF( Stop.outflag | Timeout.outflag | Rejection.outflag))
SPEC
EG( Start.outflag -> EF( Stop.outflag & Timeout.outflag & Rejection.outflag))
SPEC
EG( Start.outflag -> EF( Stop.outflag | Timeout.outflag | Rejection.outflag))
-------------- MODULES -------------------------
MODULE andFork(trigger)
VAR
outflag : boolean;
INVAR
(trigger <-> outflag)
MODULE event(trigger)
VAR
outflag:boolean;
INVAR
outflag = trigger
MODULE andJoin( trigger1, trigger2)
VAR
outflag : boolean;
INVAR
(trigger1 & trigger2<-> outflag)
MODULE atomicProcess2(trigger)
VAR
state : {idle, started, finished, interrupted1, interrupted2};
outflag : boolean;
excptflag1 : boolean;
excptflag2 : boolean;
ASSIGN
init(state) := idle;
next(state) :=
case
state = idle & trigger: {started};
state = started : {started, finished, interrupted1, interrupted2};
state = finished : {finished, idle};
state = interrupted1 : {interrupted1, idle};
state = interrupted2 : {interrupted2, idle};
TRUE : state;
esac;
INVAR
(state = finished <-> outflag = TRUE)
INVAR
(state = interrupted1 <-> excptflag1 = TRUE)
INVAR
(state = interrupted2 <-> excptflag2 = TRUE)
FAIRNESS
state = finished
FAIRNESS
state = interrupted1
FAIRNESS
state = interrupted2
MODULE atomicProcess(trigger)
VAR
state : {idle, started, finished};
outflag : boolean;
ASSIGN
init(state) := idle;
next(state) :=
case
state = idle & trigger: {started};
state = started : {started, finished};
state = finished : {finished, idle};
TRUE : state;
esac;
INVAR
(state = finished <-> outflag = TRUE)
FAIRNESS
state = finished
MODULE xorJoin(input1, input2)
VAR
output : boolean;
INVAR
(input1 | input2 <-> output)
==== General description ====
==== Installation ====
Following the instructions in: [[https://github.com/archimatetool/archi/wiki/Developing-Import-and-Export-Plug-ins]]
- Download the [[http://home.agh.edu.pl/~pszwed/archi/pl.edu.agh.kis.pszwed.archi.nusmvexport_1.0.0.202007122336.jar|compiled plugin (JAR)]] controlling the model generation
- Copy it to the //dropins// directory
- Restart Archi
- A new menu item //File//->//Export//->//Model to NuSMV// should appear.
This is a quote from [[https://github.com/archimatetool/archi/wiki/Developing-Import-and-Export-Plug-ins]]
Note:
The default "dropins" folder is located in the following places:
Windows: %user.home%/AppData/Roaming/Archi4/dropins
Mac: %user.home%/Library/Application Support/Archi4/dropins
Linux: %user.home%/.archi4/dropins
("%user.home%" denotes your home directory.)
Or you can manually create a "dropins" folder alongside the Archi installation's "plugins" folder.
==== Controlling model generation ====
Model genetration is controlled by the properties file named ''NuSMVExport.properties''.
The file should be placed in a location depending on the platform. However, when you use Archi to NuSMV option for the first time, the plugin reports missing properties file and creates it in a recommended location. User is notified of the file creation with a message box similar to the one below.
{{:archi_to_nusmv-properties.png|Notification on creation default properties file (Windows platform)}}
*Please take a note, where the ''NuSMVExport.properties'' was placed, in the case you wish to edit it.
*Downolad example properties file [[http://pszwed.kis.agh.edu.pl/code/2015/archi/NuSMVExport.properties|NuSMVExport.properties]]
specification.generate=true # generate CTL specification
specification.generate.ctl.universal=true # generate AG / AF specifications
specification.generate.ctl.existential=true # generate EG / EF specifications
specification.generate.reachable.or=true # responsible for OR, as in AG( Start.outflag -> AF( Stop.outflag | Timeout.outflag | Rejection.outflag))
specification.generate.reachable.and=true # responsible for AND, as in AG( Start.outflag -> AF( Stop.outflag & Timeout.outflag & Rejection.outflag))
specification.generate.module=false # generate specification for modules
# For the below elements there is a choice between synchronous and interleaving implementation
# interleaving implementation: FSM model is used for a given element, i.e. there are intermediary states between an input occurrence and output
# synchronous: output is generated synchronously with the input
semantcis.event=synchronous
semantcis.process=interleaving
#semantcis.process=synchronous
semantcis.xorfork=synchronous
semantcis.xorjoin=synchronous
semantcis.andfork=synchronous
semantcis.andjoin=synchronous
#semantcis.event=interleaving
#semantcis.process=interleaving
#semantcis.xorfork=interleaving
#semantcis.xorjoin=interleaving
#semantcis.andfork=interleaving
#semantcis.andjoin=interleaving
refactoring.remove.process=false # a process with one input and one output can be removed
==== References ====
*Piotr Szwed, Verification of ArchiMate Behavioral Elements by Model Checking, Computer Information Systems and Industrial Management: 14th IFIP TC 8 International Conference, CISIM 2015, Warsaw, Poland, September 24-26, 2015 [[https://www.researchgate.net/publication/284901129_Verification_of_ArchiMate_Behavioral_Elements_by_Model_Checking|PDF on researchgate]]
*Piotr Szwed, Efficiency of formal verification of ArchiMate business processes with NuSMV model checker, Federated Conference on Computer Science and Information Systems (FedCSIS),2015. [[https://www.researchgate.net/publication/284900873_Efficiency_of_formal_verification_of_ArchiMate_business_processes_with_NuSMV_model_checker|PDF on researchgate]]
*Piotr Szwed, Evaluating Efficiency of ArchiMate Business Processes Verification with NuSMV, Information Technology for Management: Federated Conference on Computer Science and Information Systems, ISM 2015 and AITM 2015, Revised Selected Papers, LNBIP 243, 2016 [[https://www.researchgate.net/publication/303383111_Evaluating_efficiency_of_ArchiMate_business_processes_verification_with_NuSMV|PDF on researchgate]]
@Inbook{Szwed2015,
author="Szwed, Piotr",
editor="Saeed, Khalid
and Homenda, Wladyslaw",
chapter="Verification of ArchiMate Behavioral Elements by Model Checking",
title="Computer Information Systems and Industrial Management: 14th IFIP TC 8 International Conference, CISIM 2015, Warsaw, Poland, September 24-26, 2015, Proceedings",
year="2015",
publisher="Springer International Publishing",
address="Cham",
pages="132--144",
isbn="978-3-319-24369-6",
doi="10.1007/978-3-319-24369-6_11",
url="http://dx.doi.org/10.1007/978-3-319-24369-6_11"
}
@INPROCEEDINGS{7321614,
author={Piotr Szwed},
booktitle={Computer Science and Information Systems (FedCSIS), 2015 Federated Conference on},
title={Efficiency of formal verification of ArchiMate business processes with NuSMV model checker},
year={2015},
pages={1427-1436},
doi={10.15439/2015F44},
month={Sept},}
@Inbook{Szwed2016,
author="Szwed, Piotr",
editor="Ziemba, Ewa",
chapter="Evaluating Efficiency of ArchiMate Business Processes Verification with NuSMV",
title="Information Technology for Management: Federated Conference on Computer Science and Information Systems, ISM 2015 and AITM 2015, Lodz, Poland, September 2015, Revised Selected Papers",
year="2016",
publisher="Springer International Publishing",
address="Cham",
pages="179--196",
isbn="978-3-319-30528-8",
doi="10.1007/978-3-319-30528-8_11",
url="http://dx.doi.org/10.1007/978-3-319-30528-8_11"
}