- Tytuł:
-
Weryfikacja procesów biznesowych metodą dedukcyjną z wykorzystaniem logiki temporalnej
Deduction-based Formal Verification of Business Models using Temporal Logic - Autorzy:
- Klimek, R.
- Powiązania:
- https://bibliotekanauki.pl/articles/274553.pdf
- Data publikacji:
- 2011
- Wydawca:
- Sieć Badawcza Łukasiewicz - Przemysłowy Instytut Automatyki i Pomiarów
- Tematy:
-
modele biznesowe
BPMN
SOA
wzorce projektowe
logika temporalna
wnioskowanie dedukcyjne
metoda tablic semantycznych
generowanie specyfikacji
business models
workflow design patterns
temporal logic
deductive reasoning
semantic tableaux method
generating specifications - Opis:
-
Praca dotyczy formalnej analizy i weryfikacji modeli biznesowych wyrażonych w notacji BPMN. Weryfikacja oparta jest na wnioskowaniu dedukcyjnym. Jako metodę wnioskowania dla modeli biznesowych zaproponowano metodę tablic semantycznych, która cechuje się apagogicznością oraz analitycznością. Została przedstawiona metoda translacji podstawowych wzorców projektowych BPMN do formuł logiki temporalnej, stanowiących logiczną specyfikację analizowanegomodelu. Zarówno logiczna specyfikacja, jak i właściwości badanych procesów są wyrażone formułami tzw. najmniejszej logiki temporalnej. Formuły te są następnie przetwarzane z wykorzystaniem metody tablic semantycznych. Innowacyjność proponowanego podejścia może istotnie wpłynąć na redukcję kosztów wytwarzania oprogramowania, ze względu na możliwość wykrycia błędów oprogramowania już w fazie jego modelowania, wyprzedzając tym samym znacznie fazy implementacji i testowania.
The paper concerns formal analysis and verification of business models expressed in BPMN. This verification is based on a deductive reasoning. As a method of inference for business models semantic tableaux method is proposed. Automatic trans- formations of the basic BPMN workflow patterns to temporal logic formulas are proposed. These formulas constitute a logical specification of the analyzed model. Both the logical specification and the desired system properties are expressed as formulas of the smallest linear temporal logic. These formulas are later processed using semantic tableaux method. Applying this innovative concept might result in software development costs reduction as some errors might be addressed in the modeling phase not in implementation or testing phase. - Źródło:
-
Pomiary Automatyka Robotyka; 2011, 15, 12; 190-193
1427-9126 - Pojawia się w:
- Pomiary Automatyka Robotyka
- Dostawca treści:
- Biblioteka Nauki
Artykuł