User Tools

Site Tools


Sidebar

*[[start|Home]] *[[research|Research]] *[[fuzzy_semantic_petri_nets|Fuzzy Semantic Petri]] *[[is_security_risk_assesment|IT Security Risk]] *[[papers|Publications]] *[[projects|Projects]] *[[ontologies|Ontologies]] *[[software|Software]] *[[archi_to_owl|Archimate to OWL]] *[[archi_to_nusmv|Archimate to nuSMV]]

archi_to_nusmv

===== 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]]. <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: [[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]] <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 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 # 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 </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>

archi_to_nusmv.txt · Last modified: 2020/07/12 23:49 by pszwed