Wyniki wyszukiwania - BazTech

1

A system for deduction-based formal verification of workflow-oriented software models

Klimek R.

International Journal of Applied Mathematics and Computer Science

|

2014

|

Vol. 24, no. 4

941--956

EN

The work concerns formal verification of workflow-oriented software models using the deductive approach. The formal correctness of a model’s behaviour is considered. Manually building logical specifications, which are regarded as a set of temporal logic formulas, seems to be a significant obstacle for an inexperienced user when applying the deductive approach. A system, along with its architecture, for deduction-based verification of workflow-oriented models is proposed. The process inference is based on the semantic tableaux method, which has some advantages when compared with traditional deduction strategies. The algorithm for automatic generation of logical specifications is proposed. The generation procedure is based on predefined workflow patterns for BPMN, which is a standard and dominant notation for the modeling of business processes. The main idea behind the approach is to consider patterns, defined in terms of temporal logic, as a kind of (logical) primitives which enable the transformation of models to temporal logic formulas constituting a logical specification. Automation of the generation process is crucial for bridging the gap between the intuitiveness of deductive reasoning and the difficulty of its practical application when logical specifications are built manually. This approach has gone some way towards supporting, hopefully enhancing, our understanding of deduction-based formal verification of workflow-oriented models.

2

From workflow design patterns to logical specifications

Klimek R.

Automatyka / Automatics

|

2013

|

Vol. 17, no. 1

59--63

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.

3

Weryfikacja procesów biznesowych metodą dedukcyjną z wykorzystaniem logiki temporalnej

Klimek R.

Pomiary Automatyka Robotyka

|

2011

|

R. 15, nr 12

190-193

PL

Praca dotyczy formalnej analizy i weryfikacji modeli biznesowych wyrażonych w notacji BPMN. Weryfikacja oparta jest na wnioskowaniu dedukcyjnym. Jako metodę wnioskowania dla modeli biznesowych zaproponowano metodę tablic semantycznych, która cechuje się apagogicznością oraz analitycznością. Została przedstawiona metoda translacji podstawowych wzorców projektowych BPMN do formuł logiki temporalnej, stanowiących logiczną specyfikację analizowanegomodelu. Zarówno logiczna specyfikacja, jak i właściwości badanych procesów są wyrażone formułami tzw. najmniejszej logiki temporalnej. Formuły te są następnie przetwarzane z wykorzystaniem metody tablic semantycznych. Innowacyjność proponowanego podejścia może istotnie wpłynąć na redukcję kosztów wytwarzania oprogramowania, ze względu na możliwość wykrycia błędów oprogramowania już w fazie jego modelowania, wyprzedzając tym samym znacznie fazy implementacji i testowania.

EN

The paper concerns formal analysis and verification of business models expressed in BPMN. This verification is based on a deductive reasoning. As a method of inference for business models semantic tableaux method is proposed. Automatic trans- formations of the basic BPMN workflow patterns to temporal logic formulas are proposed. These formulas constitute a logical specification of the analyzed model. Both the logical specification and the desired system properties are expressed as formulas of the smallest linear temporal logic. These formulas are later processed using semantic tableaux method. Applying this innovative concept might result in software development costs reduction as some errors might be addressed in the modeling phase not in implementation or testing phase.

4

Formal analysis of use case diagrams

Klimek R., Szwed P.

Computer Science

|

2010

|

Vol. 11

115-131

EN

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.

PL

Diagramy przypadków użycia odgrywają znaczącą rolę w modelowaniu systemów z wykorzystaniem UML. Staranne i dokładne modelowanie ma zasadnicze znaczenie w postępowaniu umożliwiającym uzyskanie poprawnej i efektywnej architektury systemu. Artykuł odnosi się do formalnej analizy diagramów przypadków użycia. Został zaproponowany model formalny przypadku użycia, a także opisano odpowiednie konstrukcje dla relacji występujących pomiędzy przypadkami użycia. Zostały przedstawione dwie formalne metody ich analizy i weryfikacji. Pierwsza oparta jest na eksploracji stanów i reprezentuje podejście nazwane weryfikacją modelową. Druga odwołuje się do wnioskowania symbolicznego z wykorzystaniem logiki temporalnej. Został pokazany prosty i reprezentatywny przykład weryfikacji pewnego scenariusza przypadku użycia.

5

Weryfikacja procesów biznesowych metodą tablic semantycznych

Klimek R., Skrzyński P., Turek M.

Automatyka / Akademia Górniczo-Hutnicza im. Stanisława Staszica w Krakowie

|

2010

|

T. 14, z. 3/2

905-914

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.

6

Weryfikacja aktywności systemów modelowanych na bazie architektury SOA - prowadzona w oparciu o wymagania zadane diagramami przypadków użycia

Klimek R., Skrzyński P., Turek M.

Automatyka / Akademia Górniczo-Hutnicza im. Stanisława Staszica w Krakowie

|

2010

|

T. 14, z. 3/2

893-903

PL

Artykuł porusza zagadnienia formalnej weryfikacji wymagań dla tzw. systemów biznesowych, wyrażonych przez model przypadków użycia oraz scenariuszy przypadków użycia UML. Zaproponowana została metodologia opisująca przejście od diagramów przypadków użycia do diagramów aktywności. Do specyfikacji żądanych własności systemu została wykorzystana logika temporalna. Własności tak zakodowane mogą być następnie poddawane procesom weryfikacji z wykorzystaniem wnioskowania dedukcyjnego metodą tablic semantycznych. Zaproponowane zostały metody pozyskiwania formuł logiki temporalnej bezpośrednio ze scenariuszy przypadków użycia zapisanych w diagramach czynności UML.

EN

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.

7

Rozszerzenie języka BPQL na potrzeby interaktywnego modelowania i formalnej weryfikacji diagramów aktywności UML

Klimek R., Skrzyński P., Turek M.

Automatyka / Akademia Górniczo-Hutnicza im. Stanisława Staszica w Krakowie

|

2010

|

T. 14, z. 3/2

915-924

PL

Artykuł opisuje wyniki prac będących kontynuacją badań na temat przetwarzania procesów biznesowych metodami półformalnymi i formalnymi. Autorzy, proponując system transformacji diagramów aktywności do postaci zadanych formalnie i możliwych do weryfikowania reguł, napotkali problem ograniczeń w możliwościach szybkiego i interaktywnego projektowania procesów biznesowych - będących materiałem dla proponowanych przez siebie metod przetwarzania. Zaproponowali rozwiązanie w postaci rozszerzenia funkcjonalnego języka zapytań dla procesów biznesowych, określanego akronimem BPQL (Business Process Query Language). Język ten, definiując zestawy instrukcji strukturalnych, opisuje przebieg procesu biznesowego, nawiązując składnią do wielu współcześnie stosowanych języków programowania. Powstały pseudokod BPQL można wykorzystać jako podstawę do określenia zachowania elementarnego procesu w zadanej wartościami parametrów sytuacji. W języku nie jest jednak możliwe definiowanie formuł modyfikujących już istniejący proces, lub przetwarzanie przepływów sterowania pomiędzy tzw. procesami elementarnymi. Proponowane wysoko poziomowe rozszerzenie BPQL pozwoli na rozbudowę modelu procesów biznesowych w trybie interaktywnym. Innowacje będą polegały na adaptacji wspomnianego języka do wyrażania komend modyfikujących treść logiczną już istniejących procesów. Sprowadzą się do zaproponowania nowego języka typu Structured Query, operującego na procesach biznesowych oraz tak zwanych wzorcach procesowych i zdefiniowanego pod roboczą nazwą Business Process Structured Query Language. Wyrażony za pomocą skryptu język będzie określał operacje na przepływach sterowania w modelu procesu w sposób analogiczny jak języki typu SQL określają operacje modyfikujące strukturę baz danych dla modelowanych systemów. Struktura procesu wyrażana za pośrednictwem tzw. notacji BPMN będzie także możliwa do wyrażenia za pośrednictwem zbioru formuł logiki temporalnej. Wykonanie zapytania BPSQL będzie powiązane z modyfikacją tych formuł. Procedura walidacji poprawności formuły po modyfikacjach pozostanie bez zmian, co umożliwi zastosowanie metod walidacji osiągniętych jako wyniki wcześniejszych prac autorów. Takie podejście otworzy drogę do projektowania systemów, które umożliwią interaktywne modelowanie procesów biznesowych z jednoczesną walidacją poprawności procesów - realizowaną analogicznie do procedur kontroli więzów integralności w bazie danych, prowadzonej przez Systemy Zarządzania Bazami Danych.

EN

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.

8

Zakład Odsalania przy kopalni Dębieńsko - bezodpadowa utylizacja zasolonych wód kopalniach

Piecha J., Klimek R.

Wiadomości Górnicze

|

1998

|

nr 9

379-384

PL

Autorzy przedstawili nową, działającą od 1994 r. przy Kopalni Węgla Ka-miennego 'Dębieńsko' instalację odsalającą wody słone z kopalń 'Dębieńsko', 'Budryk', 'Bolesław Śmiały', zaprojektowaną przez Biuro Projektów Energe-tycznych i Ochrony Środowiska 'Encrgotechnika', w oparciu o technologię szwedzka i amerykańską. Przedstawiono także, dla porównania, pracującą już przy tej kopalni od 1975 r. inną instalację odsalającą, zaprojektowaną w oparciu o technologię Głównego Instytutu Górnictwa. W artykule przedstawiono skalę ekonomiczną problemu, obejmującą swo-im zakresem porównanie wysokości stosownych opłat ekologicznych, jakie wy-mienione tu kopalnie musiałyby zapłacić w przypadku bezpośredniego zrzutu soli do środowiska.

EN

The authors have presented a new, operating from 1994, installation for de-salination of saline waters from ..Dcbiensko', ,,Budryk', ..Bolestaw Smialy' mi-nes located at ' Debiensko' hard coal mine and designed by Power Projects and Environment Protection Office ' Energotechnika' on the basis of Swedish and US technology. It also presents, for comparison reasons, desalination installation operating from 1975 at the mine and designed on the basis of technology by the Central Mining Institute. The economic scale of the problem has also been shown in the article cove-ring with its scope comparison of the value of ecological fees that should be paid by the mines mentioned herein in case of disposing of the salt into the natural environment.