Archimate to NuSMV (nuXmv)

Archimate to NuSMV is a plugin to popular 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

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 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: http://www.archimatetool.com/dev/import-export

  1. Download the compiled plugin (JAR)

controlling the model generation

  1. Copy it to the plugins directory of Archi installation
  2. Restart Archi
  3. A new menu item FileExportModel 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.

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 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 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. 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 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"
}
 
archi_to_nusmv.txt · Last modified: 2016/05/21 00:58 by pszwed     Back to top
Recent changes RSS feed Creative Commons License Donate Powered by PHP Valid XHTML 1.0 Valid CSS Driven by DokuWiki Design by LouisWolf