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

Znaleziono wyników: 19

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

help Ogranicz wyniki do:
first rewind previous Strona / 1 next fast forward last
1
Content available Comparing sat-based bounded model checking rtectl and ectl properties
Zbrzezny A. M.
Technical Sciences / University of Warmia and Mazury in Olsztyn
|
2017
|
nr 20(2)
131--147
EN
We compare two SAT-based bounded model checking algorithms for the properties expressed in the existential fragment of a soft real-time computation tree logic (RTECTL) and in the existential fragment of computation tree logic (ECTL). To this end, we use the generic pipeline paradigm (GPP) and the train controller system (TC), the classic concurrency problems, which we formalise by means of a finite transition system. We consider several properties of the problems that can be expressed in both RTECTL and ECTL, and we present the performance evaluation of the mentioned bounded model checking methods by means of the running time and the memory used.
2
Content available remote Verification of Linear-Time Temporal Properties for Reaction Systems with Discrete Concentrations
Męski A., Koutny M., Penczek W.
Fundamenta Informaticae
|
2017
|
Vol. 154, nr 1/4
289--306
EN
Reaction systems are a formal model for computational processes inspired by the functioning of the living cell. This paper introduces reaction systems with discrete concentrations, which are an extension of reaction systems allowing for quantitative modelling. We demonstrate that although reaction systems with discrete concentrations are semantically equivalent to the original qualitative reaction systems, they provide much more succinct representations in terms of the number of entities being used. We define a variant of Linear Time Temporal Logic interpreted over models of reaction systems with discrete concentrations. We provide its suitable encoding in SMT, together with bounded model checking, and present experimental results demonstrating the scalability of the verification method for reaction systems with discrete concentrations.
3
Content available remote Towards SAT-based BMC for LTLK over Interleaved Interpreted Systems
Penczek W., Woźna-Szcześniak B., Zbrzezny A.
Fundamenta Informaticae
|
2012
|
Vol. 119, nr 3/4
373-392
EN
This paper makes two contributions to the verification of multi-agent systems modelled by interleaved interpreted systems. Firstly, the paper presents theoretical underpinnings of the SATbased bounded model checking (BMC) approach for LTL extended with the epistemic component (LTLK) over interleaved interpreted systems. Secondly, the BMC method has been implemented and tested on several benchmarks for MAS. The preliminary experimental results reveal advantages and disadvantages of our SAT-based BMC for LTLK and show that the method has a significant potential.
4
Content available remote A New Translation from ECTL* to SAT*
Zbrzezny A.
Fundamenta Informaticae
|
2012
|
Vol. 120, nr 3/4
375-395
EN
In this paper we present a new translation from ECTL* to SAT and show that the proposed translation substantially increases the efficiency of verifying temporal properties using the Bounded Model Checking method. We have implemented our new translation and made experimental results, which demonstrate the efficiency of the method.
5
Content available remote BDD-based Bounded Model Checking for Temporal Properties of 1-Safe Petri Nets
Męski A., Penczek W., Półrola A.
Fundamenta Informaticae
|
2011
|
Vol. 109, nr 3
305-321
EN
In the paper we present a bounded model checking for 1-safe Petri nets and properties expressed in LTL and the universal fragment of CTL, based on binary decision diagrams. The presented experimental results show that we have obtained a technique which performs better in some of the considered cases, in comparison with the existing SAT-based implementation. The results are also compared with standard BDD-based symbolic method.
6
Content available remote Bounded Parametric Verification for Distributed Time Petri Nets with Discrete-Time Semantics
Knapik M., Penczek W., Szreter M., Półrola A.
Fundamenta Informaticae
|
2010
|
Vol. 101, nr 1/2
9-27
EN
Bounded Model Checking (BMC) is an efficient technique applicable to verification of temporal properties of (timed) distributed systems. In this paper we show for the first time how to apply BMC to parametric verification of time Petri nets with discrete-time semantics. The properties are expressed by formulas of the logic PRTECTL - a parametric extension of the existential fragment of Computation Tree Logic (CTL).
7
Content available remote A New Approach to Model Checking of UML State Machines
Niewiadomski A., Penczek W., Szreter M.
Fundamenta Informaticae
|
2009
|
Vol. 93, nr 1-3
289-303
EN
The paper presents a new approach to model checking of systems specified in UML. All the executions of an UML system (unfolded to a given depth) are encoded directly into a boolean propositional formula, satisfiability of which is checked using a SAT-solver. Contrary to other UML verification tools we do not use any of the existing model checkers as we do not translate UML specifications into an intermediate formalism. The method has been implemented as the (prototype) tool BMC4UML and some experimental results are presented.
8
Content available remote Improving the Translation from ECTL to SAT
Zbrzezny A.
Fundamenta Informaticae
|
2008
|
Vol. 85, nr 1-4
513-531
EN
The objective of this paper is to offer an improvement to the translation from ECTL to SAT introduced in [14] and show that the improvement proposed substantially increases the efficiency of verifying temporal properties using the Bounded Model Checking method. We have implemented our new translation and made preliminary experimental results, which demonstrate the efficiency of the method.
9
Content available remote A Boolean Encoding of Arithmetic Operations
Zbrzezny A.
Prace Instytutu Podstaw Informatyki Polskiej Akademii Nauk
|
2007
|
Nr 999
1-35
EN
In this paper we present algorithms for a~Boolean encoding of four basic arithmetic operations on integer numbers: addition, subtraction, multiplication and division. Integer numbers are encoded in two's complement system as vectors of Boolean formulas and arithmetic operations are faithfully encoded as operations on vectors of Boolean formulas. In addition, we also provide an algorithm for a Boolean encoding of the operations of calculating integer square root and an algorithm for a Boolean encoding of the operation of exponentiation with nonnegative integer exponent.
PL
W pracy przedstawiamy algorytmy realizujące Boolowskie kodowanie czterech podstawowych operacji arytmetycznych: dodawania, odejmowania, mnożenia i dzielenia. Liczby całkowite są kodowane w systemie uzupełnieniowym do 2 jako wektory formuł Boolowskich a operacje arytmetyczne są zakodowane jako operacje na wektorach formuł Boolowskich. Dodatkowo przedstawiamy algorytmy realizujące Boolowskie kodowanie dla operacji obliczania całkowitego pierwiastka kwadratowego oraz dla operacji potęgowania.
10
Content available remote Bounded Model Checking for the Existential Fragment of TCTL-G and Diagonal Timed Automata
Woźna B., Zbrzezny A.
Fundamenta Informaticae
|
2007
|
Vol. 79, nr 1-2
229-256
EN
Bounded Model Checking (BMC) is one of the well known SAT based symbolic model checking techniques. It consists in searching for a counterexample of a particular length, and generating a propositional formula that is satisfiable iff such a counterexample exists. The BMC method is feasible for the various classes of temporal logic; in particular it is feasible for TECTL (the existential fragment of Time Computation Tree Logic) and Diagonal-free Timed Automata. The main contribution of the paper is to show that the concept of Bounded Model Checking can be extended to deal with TECTL-G properties of Diagonal Timed Automata. We have implemented our new BMC algorithm, and we present preliminary experimental results, which demonstrate the efficiency of the method.
11
Content available remote Comparing BDD and SAT based techniques for model checking Chaum's Dining Cryptographers Protocol
Kacprzak M., Lomuscio A., Niewiadomski A., Penczek W., Raimondi F., Szreter M.
Fundamenta Informaticae
|
2006
|
Vol. 72, nr 1-3
215-234
EN
We analyse different versions of the Dining Cryptographers protocol by means of automatic verification via model checking. Specifically we model the protocol in terms of a network of communicating automata and verify that the protocol meets the anonymity requirements specified. Two different model checking techniques (ordered binary decision diagrams and SAT-based bounded model checking) are evaluated and compared to verify the protocols.
12
Content available remote ACTL* properties and Bounded Model Checking
Woźna B.
Fundamenta Informaticae
|
2004
|
Vol. 63, nr 1
65--87
EN
The main contribution of the paper consists in showing that the bounded model checking (BMC) method is feasible for ACTL* (the universal fragment of CTLS) which subsumes both ACTL and LTL. The extension to ACTL* is obtained by redefining the function returning the sufficient number of executions over which an ACTL* formula is checked, and then combining the two known translations to SAT for ACTL and LTL formulas. The proposed translation of ACTL* formulas is essentially different from the existing translations of both ACTL and LTL formulas. Moreover, the formal treatment is the basis for the implementation of the technique in the symbolic model checker Verics.
13
Content available remote Reaching the limits for Bounded Model Checking
Woźna B.
Prace Instytutu Podstaw Informatyki Polskiej Akademii Nauk
|
2003
|
Nr 958
1-25
EN
The main contribution of the paper consists in showing that the BMC method is feasible for ACTL* (the universal fragment of CTL*) which subsumes both ACTL and LTL. The extension to ACTL* is obtained by redefining the function returning the sufficient number of executions over which an ACTL* formula is checked, and then by combining two known translations to SAT for ACTL and LTL formulas. The proposed translation of ACTL* formulas is essentially different from the existing translations of both ACTL and LTL formulas. Moreover, ACTL* seems to be the largest set of temporal properties which can be verified by means of BMC. We have implemented our new BMC algorithm for discrete timed automata and we have presented a preliminary experimental results, which prove the efficiency of the method. The formal treatment is the basis for the implementation of the technique in the symbolic model checker VerICS.
PL
Osiągnięcie granicy rozszerzalności metody ograniczonej weryfikacji modelowej. Głównym celem tej pracy jest wykazanie, że metoda ograniczonej weryfikacji modelowej (OWM) jest rozszerzalna do własności wyrażalnych w ACTL* (uniwersalnym fragmencie logiki CTL*), języku który zawiera zarówno ACTL i LTL. Rozszerzenie metody OWM do ACTL* polega na przedefiniowaniu funkcji zwracającej wystarczającą liczbę wykonań systemu, w zbiorze których formuła ACTL* jest sprawdzana, a następnie na zdefiniowaniu translacji będącej kombinacją translacji formuł LTL i ACTL. Zaproponowana translacja formuł ACTL* istotnie różni się od tych istniejących dla LTL i ACTL oraz wydaje się, że język ACTL* jest największym zbiorem własności temporalnych, które mogą być weryfikowane za pomocą metody OWM. Nasz nowy algorytm został zaimplementowany dla elementarnych sieci Petriego oraz dla dyskretnych automatów czasowych, a uzyskane wstępne wyniki eksperymentalne dowodzą efektywności naszej metody. Ponadto, zaproponowana translacja i wykonana implementacja będzie bazą dla nowego modułu w symbolicznym weryfikatorze Öerics.
14
Content available remote Checking Reachability Properties for Timed Automata via SAT
Woźna B., Zbrzezny A., Penczek W.
Fundamenta Informaticae
|
2003
|
Vol. 55, nr 2
223-241
EN
The paper deals with the problem of checking reachability for timed automata. The main idea consists in combining the well-know forward reachability algorithm and the Bounded Model Checking (BMC) method. In order to check reachability of a state satisfying some desired property, first the transition relation of a timed automaton is unfolded iteratively to some depth and encoded as a propositional formula. Next, the desired property is translated to a propositional formula and the satisfiability of the conjunction of the two defined above formulas is checked. The unfolding of the transition relation can be terminated when either a state satisfying the property has been found or all the states of the timed automaton have been searched. The efficiency of the method is strongly supported by the experimental results.
15
Content available remote SAT-Based Bounded Model Checking for the Universal Fragment of TCTL
Penczek W., Woźna B., Zbrzezny A.
Prace Instytutu Podstaw Informatyki Polskiej Akademii Nauk
|
2002
|
Nr 947
1-26
EN
Bounded Model Checking (BMC) based on SAT methods consists in searching for a counterexample of a particular length and to generate a propositional formula that is satisfiable iff such a counterexample exists. Our paper shows how the concept of bounded model checking can be extended to deal with \TACTL\ (the universal fragment of \TCTL ) properties of a network of concurrent Timed Automata.
PL
Ograniczona Weryfikacja Modelowa, bzaująca na metodach SAT, polega na poszukiwaniu kontrprzykładów o długości ograniczonej przez pewną liczbę całkowitą k > 0 oraz generowanie formuły zdaniowej, która jest spełniana wtedy i tylko wtedy, gdy taki kontrprzykład istnieje. Celem tej pracy jest przedstawienie koncepcji ograniczonej weryfikacji modelowej dla automatów czasowych reprezentowanych przez siec współbieżnych i wzajemnie komunikujących się komponentów oraz własności wyrażanych w języku logiki TACTL (uniwersalnego fragmentu TCTL).
16
Content available remote Checking Reachability Properties for Timed Automata via SAT
Woźna B., Penczek W., Zbrzezny A.
Prace Instytutu Podstaw Informatyki Polskiej Akademii Nauk
|
2002
|
Nr 949
1-19
EN
The paper deals with the problem of checking reachability for timed automata. The main idea consists in combining the well-know forward reachability algorithm and the Bounded Model Checking (BMC) method. In order to check reachability of a state satisfying some desired property, first the transition relation of a timed automaton is unfolded to the depth k Î N and encoded as a prepositional formula. Next the desired property is translated to a prepositional formula and the satisfiability of the conjunction of the two above defined formulas is checked. The unfolding of the transition can be terminated when either a state satisfying the property has been found or all the states of the timed automaton have been searched. The efficiency of the method is strongly supported by the experimental results. Keywords : Reachability problem, bounded model checking, translation to SAT, Timed Automata, Augmented Region Graphs, discretization.
PL
Testowanie osiągalności automatów czasowych z wykorzystaniem SAT. Praca opisuje nowe podejście do problemu osiągalności dla automatów czasowych. Główna idea polega na połączeniu znanego algorytmu przeszukującego przestrzeń stanów wszerz metodą BFS oraz metody ograniczonej weryfikacji modelowej. Aby sprawdzić, czy stan spełniający daną własność jest osiągalny w modelu dla rozważanego automatu czasowego postępujemy następująco. Rozwijamy stopniowo relację przejścia dla automatu, aż do głębokości k Î N i kodujemy ją jako formułę zdaniową. Następnie, za pomocą formuły zdaniowej kodowana jest rozważana własność i sprawdzana jest spełnialność koniunkcji obydwu zdefiniowanych formuł zdaniowych. Rozwijanie relacji przejścia może zostać zakończone jeśli poszukiwany stan został znaleziony lub wszystkie stany danego automatu czasowego zostały przeszukane.
17
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.
18
Content available remote Bounded Model Checking for the Universal Fragment of CTL
Penczek W., Woźna B., Zbrzezny A.
Fundamenta Informaticae
|
2002
|
Vol. 51, nr 1,2
135-156
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 length 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 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.
19
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ć.