Weryfikacja procesów biznesowych metodą tablic semantycznych

• Autorzy: Klimek R. , Skrzyński P. , Turek M.

Warianty tytułu

EN

Automated process verification with a semantic tables approach

• Języki publikacji: PL

Abstrakty

PL

Artykuł opisuje wyniki prac nad ustabilizowaniem metodyki umożliwiającej formalne weryfikowanie poprawności procesów zapisanych za pomocą zbioru wzorców procesowych w notacji BPMN. Główną ścieżką rozwiązania jest prowadzenie konwersji modelu BPMN do postaci zbioru specjalnie opracowanych formuł logiki temporalnej. Następnie - formalnie zadana weryfikacja poprawności zbioru formuł z zastosowaniem opracowanego przez autorów rachunku. W procesie weryfikacji została wykorzystana metoda wnioskowania bazująca na zastosowaniu tablic semantycznych. Może ona przebiegać automatycznie i jest ciekawą alternatywą dla tradycyjnego podejścia - umożliwiając m.in. względnie łatwe wskazanie błędów w specyfikacji procesu.

EN

This paper describes the results of work on stabilizing the methodology for formal correctness verification of processes recorded in a process model with BPMN notation. The main path of a solution is to carry out the conversion of BPMN model to set of specially designed logic formulas. Afterwards - to formal verify the correctness of formulas using the calculation provided by the authors. A semantic table method has been applied in the verification process. The approach could provide interesting alternative to the traditional approach, allowing relatively easy errors identification in the specification process.

Słowa kluczowe

PL

weryfikacja; notacja BPMN; dedukcja; metoda tablic semantycznych; wzorce procesowe; ekstrakcja formuł

EN

verification; BPMN notation; deduction; semantic tables method; procedural patterns; extraction of formulas

• Wydawca: Wydawnictwa AGH
• Czasopismo: Automatyka / Akademia Górniczo-Hutnicza im. Stanisława Staszica w Krakowie
• Rocznik: 2010
• Tom: T. 14, z. 3/2
• Strony: 905--914
• Opis fizyczny: Bibliogr. 9 poz., rys.

Twórcy

autor

Klimek R.

• Katedra Automatyki, Akademia Górniczo-Hutnicza w Krakowie

autor

Skrzyński P.

• Katedra Automatyki, Akademia Górniczo-Hutnicza w Krakowie

autor

Turek M.

• Katedra Automatyki, Akademia Górniczo-Hutnicza w Krakowie

Bibliografia

• [1] van der Aalst W.M.P., ter Hofstede A.H.M., Kiepusewski B., Barros A.P., Workflow Patterns. Distributed and Parallel Databases, 4(1), 2003, 5-51.
• [2] D'Agostino M., Gabbay D.M., Hahnie R., Posegga i. (eds), Handbook ofTableau Methods. Kluwer Academic Publishers, 1999.
• [3] van Benthem J., Temporal Logic. Handbook of Logic in Artificial Intelligence and Logic Programming, vol. 4, Clarendon Press, 1993-95, 241-350.
• [4] Clarke E.M. Jr., Grumberg O., Peled D.A., Model Checking. MIT Press, 1999.
• [5] Clarke E.M., "Wing J.M. et al., Formal methods: State of the art and future directions. ACM Computing Surveys, vol. 28, No. 4, 1996, 626-643.
• [6] Emerson E.A., Temporal and Modal Logic. Handbook of Theoretical Computer Science, vol. B: Formal Models and Semantics, Elsevier, MIT Press, 1990, 995-1072.
• [7] Gamma E., Hełm R., Johnosn R., Vlissides J., Design Patterns: Elements of Reusable Object-Oriented Software. Addison-Wesley, 1995.
• [8] Riehle D., Zullighoven H., Understanding and Using Patterns in Software Development. Theory and Practice of Object Systems, 1996, 2(1 ):3 13.
• [9] Wolper P., The Tableau Method for Temporal Logic: An Overview. Logique et Analyse, vol. 28, 1985, 119-136.