Weryfikacja procesów biznesowych metodą tablic semantycznych

Abstract

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. 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.