Informacja

Drogi użytkowniku, aplikacja do prawidłowego działania wymaga obsługi JavaScript. Proszę włącz obsługę JavaScript w Twojej przeglądarce.

Tytuł pozycji:

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

Tytuł:
A system for deduction-based formal verification of workflow-oriented software models
Autorzy:
Klimek, R.
Powiązania:
https://bibliotekanauki.pl/articles/330429.pdf
Data publikacji:
2014
Wydawca:
Uniwersytet Zielonogórski. Oficyna Wydawnicza
Tematy:
formal verification
deductive reasoning
temporal logic
semantic tableaux
workflow pattern
logical primitive
generating logical specification
business model
BPMN
formalna weryfikacja
wnioskowanie dedukcyjne
logika temporalna
tablica semantyczna
wzorzec przepływu pracy
generowanie specyfikacji logicznej
model biznesowy
Źródło:
International Journal of Applied Mathematics and Computer Science; 2014, 24, 4; 941-956
1641-876X
2083-8492
Język:
angielski
Prawa:
CC BY-NC-ND: Creative Commons Uznanie autorstwa - Użycie niekomercyjne - Bez utworów zależnych 3.0 PL
Dostawca treści:
Biblioteka Nauki
Artykuł
  Przejdź do źródła  Link otwiera się w nowym oknie
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.

Ta witryna wykorzystuje pliki cookies do przechowywania informacji na Twoim komputerze. Pliki cookies stosujemy w celu świadczenia usług na najwyższym poziomie, w tym w sposób dostosowany do indywidualnych potrzeb. Korzystanie z witryny bez zmiany ustawień dotyczących cookies oznacza, że będą one zamieszczane w Twoim komputerze. W każdym momencie możesz dokonać zmiany ustawień dotyczących cookies