Klimek, Radosław
Loading...
Email Address
Employee
aktywny
Alternative name
Discipline
informatyka techniczna i telekomunikacja
Author Profiles
Systemy AGH
5 results
Search Results
Now showing 1 - 5 of 5
Item type:Article, Access status: Open Access , Weryfikacja procesów biznesowych metodą tablic semantycznych(Wydawnictwa AGH, 2010) Klimek, Radosław; Skrzyński, Paweł; Turek, Michał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.Item type:Article, Access status: Open Access , From workflow design patterns to logical specifications(Wydawnictwa AGH, 2013) Klimek, RadosławPraca 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.Item type:Article, Access status: Open Access , Formal analysis of use case diagrams(Wydawnictwa AGH, 2010) Klimek, Radosław; Szwed, PiotrUse 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.Item type:Article, 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.Item type:Article, Access status: Open Access , Rozszerzenie języka BPQL na potrzeby interaktywnego modelowania i formalnej weryfikacji diagramów aktywności UML(Wydawnictwa AGH, 2010) Klimek, Radosław; Skrzyński, Paweł; Turek, MichałThe article describes the results of up study on business processes modeling with semi-formal and formal methods. A new method for transformations of activity diagrams to set of formulas has been proposed in a previous work. That enables designer tools to automatically evaluate process models correctness. It could also be possible to dynamically modify process flow structure in an interactive way - with a 'on the run' validation. To achieve that point a new language has been developed and described in this article. Solution assumes an expansion for a business processes language, referred to the acronym BPQL (Business Process Query Language). This language syntax is very basic, and can oly be used for variables definition and processing (inside a basic process symbols). lt is not possible to use BPQL formulas for interactive modification of an existing process structure or a control flow between processes. Proposed high-level extension for BPQL will allow these modifications to be made - also in a scripting or an interactive mode. The main goal for a solution development is to reduce a set of language statements - only to those possible for interactive processing. Each statement should also have a proper processing algorithm established. Each query, defined with an analogy to a typical Structured Query Language component is executed and must leave a BPMN process model intact - with validation constraints fulfilled. BPMN diagram is possible to express through a set of temporal logic formulas for validation purposes. Any execution of BPSQL query will result in a modification of these formulas. The procedure for validating the modifications to the formula remains unchanged, thus enabling the validation methods achieved as a result of earlier work. A scripting language, composed from SQL and BPSQL statements will enable quick and concurrent data structure and process behavior modeling and for future system - with a common interpreter and very similar validation system. Proposed approach will open a way to design tools enabling interactive modeling of business processes with simultaneous validation of the processes correetness. Implemented control procedures will be similar to referential database integrity checking applied by Database Management Systems while processing classical SQL data definition queries.