Browsing by Subject "logika temporalna"

Now showing 1 - 3 of 3

Access status: Open Access ,
Formal analysis of use case diagrams
(Wydawnictwa AGH, 2010) Klimek, Radosław; Szwed, Piotr
Use case diagrams play an important role in modeling with UML. Careful modeling is crucial in obtaining a correct and efficient system architecture. The paper refers to the formal analysis of the use case diagrams. A formal model of use cases is proposed and its construction for typical relationships between use cases is described. Two methods of formal analysis and verification are presented. The first one based on a states' exploration represents a model checking approach. The second one refers to the symbolic reasoning using formal methods of temporal logic. Simple but representative example of the use case scenario verification is discussed.
Access status: Open Access ,
From workflow design patterns to logical specifications
(Wydawnictwa AGH, 2013) Klimek, Radosław
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.
Access status: Open Access ,
Weryfikacja aktywności systemów modelowanych na bazie architektury SOA - prowadzona w oparciu o wymagania zadane diagramami przypadków użycia
(Wydawnictwa AGH, 2010) Klimek, Radosław; Skrzyński, Paweł; Turek, Michał
The article discusses the issue of f formal requirements verification for so-called 'business systems' - expressed through an UML Use-Case model and Use-Case scenarios. A methodology for transformation of UML Use-Case diagrams to Activity diagrams has been described. To specify advanced system requirements a temporal logic notation was used. These requirements (encoded in such way) could be verified with a deductive inference based on semantic tables. The methods for obtaining temporal logic formulas directly from Use-Case scenarios stored in the UML Activity diagrams have also been introduced.