Piotr Szwed

====== Differences ====== This shows you the differences between two versions of the page.

--- archi_to_nusmv [2016/05/18 15:30]
pszwed [Archimate to NuSMV]
+++ archi_to_nusmv [2020/07/12 23:49] (current)
pszwed
@@ Line 1: / Line 1: @@
 ===== Archimate to NuSMV (nuXmv) =====
-//Archimate to SMV// is a plugin to popular [[http://www.archimatetool.com/|Archi editor]].
+:!: 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]].
+<code>
+-----------------------------------------------------------------------------------
+-- 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)
+</code>
 ==== General description ====
@@ Line 10: / Line 152: @@
 ==== Installation ====
-Following the instructions in: [[http://www.archimatetool.com/dev/import-export]]
+Following the instructions in: [[https://github.com/archimatetool/archi/wiki/Developing-Import-and-Export-Plug-ins]]
-   - Download the [[http://pszwed.kis.agh.edu.pl/code/2015/archi/com.archimatetool.nusmvexport_1.0.0.201605181456.jar|compiled plugin (JAR)]]
+   - 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
-   - Downolad properties file [[http://pszwed.kis.agh.edu.pl/code/2015/archi/NuSMVExport.properties|NuSMVExport.properties] controlling the model generation
+   - Copy it to the //dropins// directory
-   - Copy them to the //plugins// directory of Archi installation (not sure about properties)
    - Restart Archi
-   - A new menu item //File//->//Export//->//Model to OWL// should appear.
+   - 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]]
+<code>
+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.
+</code>
 ==== Controlling model generation ====
-Model genetration is controlled by the properties file. You may edit it (hash sign starts a comment till the end of line).
+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]]
 <code>
 specification.generate=true # generate CTL specification
-specification.generate.ctl.universal=true
+specification.generate.ctl.universal=true  # generate AG / AF specifications
-specification.generate.ctl.existential=true
+specification.generate.ctl.existential=true # generate EG / EF specifications
-specification.generate.reachable.or=true
+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
+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
+specification.generate.module=false # generate specification for modules
 # For the below elements there is a choice between synchronous and interleaving implementation
@@ Line 51: / Line 216: @@
-refactoring.remove.process=false  #a process with one input and one output can be removed
+refactoring.remove.process=false  # a process with one input and one output can be removed
+</code>
+==== 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]]
+<code>
+@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"
+}
 </code>

Piotr Szwed

User Tools

Site Tools

Page Tools