Szczegóły publikacji
Opis bibliograficzny
Verification of ArchiMate process specifications based on deductive temporal reasoning / Radosław KLIMEK, Piotr SZWED // W: FedCSIS : abstracts of the Federated Conference on Computer Science and Information Systems : September 8–11, 2013, Kraków, Poland. — [Piscataway : IEEE], [2013]. — Opis częśc. wg okł. — ISBN: 978-1-4673-4471-5. — S. 88. — Pełny tekst na dołączonym Dysku Flash. — S. 1135–1142. — Wymagania systemowe: Adobe Reader. — Bibliogr. s. 1142, Abstr. — W bazie Web of Science wersja drukowana: 2013 Federated Conference on Computer Science and Information Systems (FEDCSIS). — ISBN 978-1-4673-4471-5. — S. 1109–1116
Autorzy (2)
Dane bibliometryczne
| ID BaDAP | 76765 |
|---|---|
| Data dodania do BaDAP | 2013-10-23 |
| Rok publikacji | 2013 |
| Typ publikacji | materiały konferencyjne (aut.) |
| Otwarty dostęp |  |
| Konferencja | Federated Conference on Computer Science and Information Systems |
Abstract
Formal verification of business models has become recently an intensively researched area. Application of formal methods in this field necessities in overcoming several problems. Firstly, business analyst. and designers rarely have enough skills and motivation to manually build abstract and formal specifications, hence, it arises the need to provide tools for an automated translation of business models into a suitable form ready for formal verification. Moreover, notations and languages used to describe enterprises usually have no clear semantics. Finally, the verification itself mist be supported by an efficient tool. In this paper we investigate an application of formal and deduction-based techniques to automated verification of behavioral description embedded within ArchiMate models. We describe a set of rules that governs translation of processes specified in ArchiMate language into Linear Temporal Logic (LTL) formulas. The translation step is achieved with the developed software, as a plugin into a popular the Archi modeler. Formal verification of a business process properties is achieved with another tool, the LTI, prover based on the semantic tableaux technique. Application of the method is discussed on a small, yet illustrative, example of a taxi service.
