Piotr Szwed

This page is read only. You can view the source, but not change it. Ask your administrator if you think this is wrong.
===== Archimate to NuSMV (nuXmv) =====

//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). 

<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 ====


==== Installation ====

Following the instructions in: [[http://www.archimatetool.com/dev/import-export]]

   - Download the [[http://pszwed.kis.agh.edu.pl/code/2015/archi/pl.edu.agh.kis.pszwed.archi.nusmvexport_1.0.0.201605202317.jar|compiled plugin (JAR)]]
controlling the model generation 
   - Copy it to the //plugins// directory of Archi installation 
   - Restart Archi
   - A new menu item //File//->//Export//->//Model to NuSMV// should appear. 

==== 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 created, 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
specification.generate.ctl.existential=true  
specification.generate.reachable.or=true 
specification.generate.reachable.and=true 
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
</code>
Piotr Szwed

User Tools

Site Tools

Page Tools
