====== Differences ====== This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision | ||
archi_to_nusmv [2016/05/20 23:21] pszwed [Installation] |
archi_to_nusmv [2020/07/12 23:49] (current) pszwed |
||
---|---|---|---|
Line 1: | Line 1: | ||
===== Archimate to NuSMV (nuXmv) ===== | ===== 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. | 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 ==== | ==== General description ==== | ||
Line 10: | Line 152: | ||
==== Installation ==== | ==== 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/pl.edu.agh.kis.pszwed.archi.nusmvexport_1.0.0.201605202317.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 |
- | controlling the model generation | + | - Copy it to the //dropins// directory |
- | - Copy it to the //plugins// directory of Archi installation | + | |
- Restart Archi | - Restart Archi | ||
- A new menu item //File//->//Export//->//Model to NuSMV// 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 ==== | ==== 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> | <code> | ||
specification.generate=true # generate CTL specification | 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 | # 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> | </code> |