Application of deductive reasoning to the verification of ArchiMate behavioral elements
PBN-AR
Instytucja
Wydział Zarządzania (Akademia Górniczo-Hutnicza im. Stanisława Staszica w Krakowie)
Informacje podstawowe
Główny język publikacji
EN
Czasopismo
Prace Naukowe Uniwersytetu Ekonomicznego we Wrocławiu. Informatyka Ekonomiczna
ISSN
1507-3858
EISSN
2450-0003
Wydawca
Wydawnictwo Akademii Ekonomicznej
DOI
Rok publikacji
2013
Numer zeszytu
3
Strony od-do
76--97
Numer tomu
Link do pełnego tekstu
Identyfikator DOI
Liczba arkuszy
1.57
Autorzy
(liczba autorów: 3)
Pozostali autorzy
+ 2
Słowa kluczowe
EN
semantic tableaux method
ArchiMate
deductive temporal reasoning
software verification
Linear Temporal Logic
PL
metoda tablic semantycznych
ArchiMate
wnioskowanie dedukcyjne
weryfikacja oprogramowania
liniowa logika temporalna
Streszczenia
Język
EN
Treść
The formal verification of business models has recently become an intensively researched area. It is expected that the application of formal tools may bring such benefits to organizations as the improved quality of products and services and a lower ratio of operational errors. In this paper we discuss the application of a deduction-based method for the verification of the behavioral aspects of ArchiMate models. The first step in our method consists in the translation of the ArchiMate model into Linear Temporal Logic (LTL) formulas. The resulting LTL formulas are then verified to check the expected temporal properties. The verification process is based on the semantics tableaux method and is conducted with an LTL prover. The method is discussed using an example of a business process implemented within a surveillance system.
Język
PL
Treść
Formalna weryfikacja modeli biznesowych stała się ostatnio przedmiotem intensywnych badań. Oczekuje się, że zastosowanie metod formalnych może przynieś takie korzyści, jak zwiększenie jakości produktów i usług oraz zmniejszenie liczby błędów operacyjnych. W pracy omówiono zastosowanie metody wykorzystującej wnioskowanie dedukcyjne do weryfikacji elementów behawioralnych w modelach języka ArchiMate. Pierwszy krok zaproponowanej metody polega na translacji modelu ArchiMate do postaci formuł liniowej logiki temporanej (LTL). Następnie weryfikuje się, czy spełniają one założone własności temporalne. W procesie weryfikacji używane jest narzędzie dowodzenia, w którym zastosowano technikę tablic semantycznych. Opisując metodę weryfikacji, wykorzystano przykład procesu biznesowego zaimplementowanego w systemie nadzoru.
Cechy publikacji
original article
peer-reviewed
Inne
System-identifier
idp:080195