archi_to_nusmv
====== 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:57] pszwed |
archi_to_nusmv [2020/07/12 23:49] (current) pszwed |
||
|---|---|---|---|
| Line 1: | Line 1: | ||
| ===== Archimate to NuSMV (nuXmv) ===== | ===== 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]]. | //Archimate to NuSMV// is a plugin to popular [[http://www.archimatetool.com/|Archi editor]]. | ||
| Line 11: | Line 13: | ||
| {{:archimate_finalization.png|}} | {{:archimate_finalization.png|}} | ||
| - | Generated code NuSMV (nuXmv). | + | 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> | <code> | ||
| Line 150: | 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 ==== | ||
| Line 167: | Line 183: | ||
| - | *Please take a note, where the ''NuSMVExport.properties'' was created, in the case you wish to edit it. | + | *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]] | *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 | + | 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 199: | 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> | </code> | ||
| Line 205: | Line 222: | ||
| - | *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 | + | *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. | + | *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, 2016 | + | *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]] |
| Line 227: | Line 244: | ||
| url="http://dx.doi.org/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, | @Inbook{Szwed2016, | ||
| Line 241: | Line 269: | ||
| url="http://dx.doi.org/10.1007/978-3-319-30528-8_11" | url="http://dx.doi.org/10.1007/978-3-319-30528-8_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},} | ||
| </code> | </code> | ||
| - | |||
archi_to_nusmv.1463781451.txt.gz · Last modified: 2016/05/20 23:57 by pszwed
Page Tools
Except where otherwise noted, content on this wiki is licensed under the following license: CC Attribution-Share Alike 4.0 International
