From workflow design patterns to logical specifications

• Autorzy: Klimek R.

Warianty tytułu

PL

Odwzorowanie wzorców projektowych w specyfikację logiczną systemu

• Języki publikacji: EN

Abstrakty

EN

This work concerns issues related to automatic generation of logical specifications. Logical specifications can be extracted directly from developed software models. Received specification can be used in the process of a system formal verification using a deductive approach. The generated logical specification is just a set of temporal logie fonnulas as well as verified system properties are expressed in temporal logie. The extraction process is based on the idea of organizing the whole analyzed model as a set of certain design patterns of control flows. A method of automatic transformation of workflow design patterns to temporal logie formulas is proposed. These formulas constitute a logical specification and may be the first step towards a formal verification of system correctness using any method of the deduction-based reasoning. Applying the presented concepts enables bridging the gap between naturalness and intuitive of the deductive inference and the difficulty of its practical application in the case of software models.

PL

Praca dotyczy zagadnień związanych z automatyczną generacją i modelowaniem specyfikacji logicznej. Specyfikacja logiczna może być wygenerowana bezpośrednio z modeli oprogramowania. Tak uzyskana specyfikacja następnie może być wykorzystana w procesie formalnej weryfikacji przy wykorzystaniu podejścia dedukcyjnego. Wygenerowana specyfikacja reprezentowana jest przez zbiór formuł logiki temporalnej, również weryfikowane własności systemu mogą i powinny być wyrażone w logice temporalnej. Proces ekstrakcji opiera się na założeniu, aby cały analizowany model oprogramowania został zbudowany w oparciu o przyjęte, dowolne, ale najlepsze dla danej klasy zastosowań, wzorce projektowe. Została zaproponowana metoda automatycznej translacji wzorców projektowych (przepływów) do postaci formuł logiki temporalnej. Formuły te składają się na logiczną specyfikację i mogą stanowić pierwszy krok w kierunku formalnej weryfikacji poprawności systemów z wykorzystaniem dowolnej metody wnioskowania dedukcyjnego. Zastosowanie przedstawionych koncepcji umożliwia połączenie naturalności i intuicyjności samego wnioskowania logicznego oraz praktycznego zastosowania tych metod w przypadku modeli oprogramowania.

Słowa kluczowe

EN

formal verification; temporal logic; deduction; semantic tableaux; design patterns; generating logical specification

PL

weryfikacja formalna; logika temporalna; dedukcja; tablice semantyczne; wzorce projektowe; generowanie specyfikacji logicznej

• Wydawca: Wydawnictwa AGH
• Czasopismo: Automatyka / Automatics
• Rocznik: 2013
• Tom: Vol. 17, no. 1
• Strony: 59--63
• Opis fizyczny: Bibliogr. 3 poz., rys.

Twórcy

autor

Klimek R.

• AGH University of Science and Technology, Krakow, Poland

Bibliografia

• [1] Chellas B.F., Modal Logic. Cambridge University Press, 1980.
• [2] Emerson E.A., Handbook of Theoretical Computer Science, vol. B, chapter Temporal and Modal Logic, pp. 995-1072. Elsevier, MIT Press, 1990.
• [3] Aalst W.M.P. van der, ter Hofstede A.H.M., Kiepusewski B., Barros A.P. Workflow patterns. Distributed and Parallel Databases, 4(1), 2003, pp. 5-51.