@misc{Klimek_Radosław_Application_2013,
 author={Klimek, Radosław and Szwed, Piotr and Jędrusik, Stanisław},
 year={2013},
 rights={Wszystkie prawa zastrzeżone (Copyright)},
 publisher={Wydawnictwo Uniwersytetu Ekonomicznego we Wrocławiu},
 description={Informatyka Ekonomiczna = Business Informatics, 2013, Nr 3 (29), s. 76-97},
 language={eng},
 abstract={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},
 title={Application of deductive reasoning to the verification of ArchiMate behavioral elements},
 type={artykuł},
 keywords={Deductive temporal reasoning, software verification, ArchiMate, semantics tableaux method, Linear Temporal Logic, wnioskowanie dedukcyjne, weryfikacja oprogramowania, metoda tablic semantycznych, liniowa logika temporalna},
}