Verification of ArchiMate Behavioral Elements by Model Checking

Abstract : In this paper we investigate the problem of verification of business processes specified with ArchiMate language. The proposed solution employs model checking techniques. As a verification platform the state of the art symbolic model checker NuSMV is used.We describe a method of fully automated translation of behavioral elements embedded in ArchiMate models into a representation in NuSMV language, which is then submitted to verification with respect to requirements expressed in CTL. The requirements specification can be entered by user, but we also propose to derive some of them automatically, based on analysis of control flows within business processes. The solution was implemented as a plugin to Archi, a popular ArchiMate modeling tool. Application of the method is presented on an example of a small business process.
Complete list of metadatas

Cited literature [20 references]  Display  Hide  Download

https://hal.inria.fr/hal-01444460
Contributor : Hal Ifip <>
Submitted on : Tuesday, January 24, 2017 - 10:40:11 AM
Last modification on : Thursday, October 4, 2018 - 10:12:02 PM
Long-term archiving on : Tuesday, April 25, 2017 - 2:22:16 PM

File

978-3-319-24369-6_11_Chapter.p...
Files produced by the author(s)

Licence


Distributed under a Creative Commons Attribution 4.0 International License

Identifiers

Citation

Piotr Szwed. Verification of ArchiMate Behavioral Elements by Model Checking. 14th Computer Information Systems and Industrial Management (CISIM), Sep 2015, Warsaw, Poland. pp.132-144, ⟨10.1007/978-3-319-24369-6_11⟩. ⟨hal-01444460⟩

Share

Metrics

Record views

179

Files downloads

164