PL
 |
EN
Preferencje help
Polish version English version Język
Widoczny [Schowaj] Abstrakt
Liczba wyników

Znaleziono wyników: 4

Liczba wyników na stronie
first rewind previous Strona / 1 next fast forward last
Wyniki wyszukiwania
Wyszukiwano:
w słowach kluczowych:  weryfikacja systemów
help Sortuj według:

help Ogranicz wyniki do:
first rewind previous Strona / 1 next fast forward last
1
Content available A Note on Analysis of BPMN Diagrams
Ligęza A.
Pomiary Automatyka Robotyka
|
2011
|
R. 15, nr 12
210-212
EN
BPMN has recently become a de facto standard for modeling and design of complex software intensive processes. It is widely used not only in the Business Process domain. Numerous tools supporting visual edition have been developed. Despite its unquestionable advantages the semantic analysis of logical properties seems to be one of the weaknesses of this formalism. In order to assure reliable process execution the overall structure of the graph and its logical operation should be verified.
PL
BPMN staje się powoli standardem de facto w modelowaniu i projektowaniu procesów zawierających istotne komponenty programowe. Jest powszechnie stosowany nie tylko dla modelowania procesów biznesowych. Zaimplementowano wiele narzędzi wspomagających wizualne projektowanie diagramów BPMN. Niestety, pomimo niezaprzeczalnych sukcesów semantyka BPMN i analiza własności logicznych stanowią ciągle słabe strony. Aby zapewnić niezawodną pracę systemów, należy przeprowadzić formalną analizę systemu.
2
Content available Modeling BPMN diagrams within XTT2 framework. A critical analysis
Ligęza A., Maślanka T., Kluza K., Nalepa G. J.
Automatyka / Akademia Górniczo-Hutnicza im. Stanisława Staszica w Krakowie
|
2011
|
T. 15, z. 2
299-306
EN
This paper presents preliminary results of the research concerning integration of Business Processes designed with BPMN models with Business Rules represented with the use of an expressive rule language XTT2. The presented solution allows for translation of BPMN diagram restricted to main control flow objects to XTT2. Business Rules. The translated rules can be executed using HeaRT, a rule engine for XTT2. The main goal of the research is to build a logical declarative model of BPMN-modeled process suitable for formal analysis.
PL
W pracy przedstawiono wstępne wyniki badań możliwości integracji narzędzi opisu procesów biznesowych z narzędziami do modelowania reguł. Proponowane podejście pozwala na translację bazowych diagramów BPMN do postaci regułowej w modelu XTT2, oraz na analizę i wykonanie otrzymanych reguł za pomocą silnika regułowego HeaRT. Badania ukierunkowane są na budowę logicznego, deklaratywnego modelu procesów BPMN, który pozwalałby na ich formalną analizę.
3
Content available remote Bounded Model Cheking for Interpreted Systems
Penczek W., Lomuscio A.
Prace Instytutu Podstaw Informatyki Polskiej Akademii Nauk
|
2002
|
Nr 946
1-8
EN
We present an extension of a bounded model checking algorithm to deal with temporal epistemic formulas. We use the algorithm to solve a variant of the bit transmission problem
PL
W pracy przedstawiamy rozszerzenie algorytmu ograniczonej weryfikacji modelowej do temporalnych formuł epistemicznych. Algorytm jest zastosowany do weryfikacji pewnego wariantu problemu transmisji bitów.
4
Content available remote Branching Time Bounded Model Checking for Elementary Net Systems
Penczek W., Woźna B., Zbrzezny A.
Prace Instytutu Podstaw Informatyki Polskiej Akademii Nauk
|
2001
|
Nr 940
1-16
EN
Bounded Model Checking (BMC) has been recently introduced as an efficient verification method for reactive systems. BMC based on SAT methods consists in searching for a counterexample of a particular lenght and generating a propositional formula that is satisfiable iff such a counterexample exists. This new technique has been introduced by E.Clarke et al. for model checking of the linear time temporal logic (LTL). Our paper shows how the concept of bounded model checking can be extended to ACTL (the universal fragment of CTL). The implementation of the algorithm for Elementary Net Systems is described together with the experimental results.
PL
Ograniczona weryfikacja Modelowa, bazująca na metodach SAT, została wprowadzona jako uzupełniająca technika do Symbolicznej Weryfikacji Modelowej opartej na BDD. Podstawową ideą tej metody jest poszukiwanie kontrprzykładów o długości ograniczonej przez pewne całkowite k>0 oraz generowanie formuły zadaniowej, która jest spełnialna wtedy i tylko wtedy, gdy taki kontrprzykład istnieje. Ta nowa technika została po raz pierwszy wprowadzona przez E.Clarka, A.Biera, A. Cimatti'ego i Y.Zhu i zastosowana do weryfikacji modelowej formuł liniowej logiki temporalnej. Celem tej pracy jest przedstawienie koncepcji ograniczonej weryfikacji modelowej dla formuł logiki ACTL (uniwersalnego fragmentu CTL). Ponadto prezentujemy implementację algorytmu BCM dla Sieci Elementarnych wraz z wynikami eksperymentalnymi.
first rewind previous Strona / 1 next fast forward last
JavaScript jest wyłączony w Twojej przeglądarce internetowej. Włącz go, a następnie odśwież stronę, aby móc w pełni z niej korzystać.