Preferencje help
Widoczny [Schowaj] Abstrakt
Liczba wyników

Znaleziono wyników: 15

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

help Ogranicz wyniki do:
first rewind previous Strona / 1 next fast forward last
1
EN
In the paper we present the current theoretical base of the J2FADD tool, which translates a Java program to a network of finite automata with discrite data (FADDs).The reason for building the tool is that to model check a concurrent program writ-ten in Java by means of the tools like Uppaal or VerICS (the module VerICS ), an automata model of the Java program must be build first. This is because these tools verify only systems modeled as networks of automata, in particular, systems modeled as networks of FADDs. We also make an attempt to evaluate the J2FADD tool by comparison of it with the two well known Java verification tools: Bandera and Java PathFinder.
2
Content available remote A Translator of Java Programs to TADDs
EN
The model checking tools Uppaal and VerICS accept a description of a network of Timed Automata with Discrete Data (TADDs) as input. Thus, to verify a concurrent programwritten in Java by means of these tools, first a TADD model of the program must be build. Therefore, we have developed the J2TADD tool that translates a Java program to a network of TADDs; the paper presents this tool. The J2TADD tool works in two stages. The first one consists in translation of a Java code to an internal assembly language (IAL). Then, the resulting assembly code is translated to a network of TADDs. We exemplify the use of the translator by means of the following well-known concurrency examples written in Java: race condition problem, dining philosophers problem, single sleeping barber problem and readers and writers problem.
3
Content available remote VerICS 2007 - a Model Checker for Knowledge and Real-Time
EN
The papers presents the current stage of the development of VerICS - a model checker for real-time and multi-agent systems. Depending on the type of a system considered, it enables to test various classes of properties - from reachability to temporal, epistemic and deontic formulas. The model checking methods used to this aim include both SAT-based and enumerative ones. In the paper we focus on new features of the verifier: SAT-based model checking for multi-agent systems and several extensions and improvements to real-time systems' verification.
4
Content available remote Towards Verification of Java Programs in VerICS
EN
VerICS is a tool for the automated verification of timed automata and protocols written in both the Intermediate Language and the specification language Estelle. Recently, the tool has been extended to work with Timed Automata with Discrete Data and with multi-agent systems. This paper presents a prototype Timed Automata with Discrete Data model of Java programs. In addition, we show how to use the model together with the verification core of VerICS to validate the well-known alternating bit protocol written in Java. # Greedy Algorithm for Attribute Reduction
5
Content available remote Verification of the Tesla protocol in Mcmas-x
EN
We use Mcmas-x to verify authentication properties in the Tesla secure stream protocol. Mcmas-xis an extension to explicit and deductive knowledge of the Obdd-based model checker Mcmas a verification tool for multi-agent systems.
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.
7
Content available remote Towards verification of Java programs in VerICS
EN
VerICS has been designed as a tool for automated verification of timed automata, and protocols written in both Intermediate Language and a specification language Estelle. Recently, the tool has been extended to work with so called Timed Automata with Discrete Data and multi-agent systems. The paper presents a prototype of a translator from a subset of the Java programming language to Intermediate Language and Time Automata with Discrete Data, the modeling languages of the VerICS model checker.
PL
Verics został zaprojektowany jako narzędzie do automatycznej weryfikacji automatów czasowych oraz protokołów zapisanych zarówno w języku pośrednim jaki i języku Estelle. Ostatnimi czasy Verics został rozbudowany i obecnie pozwala również na automatyczną weryfikację systemów wieloagentowych oraz protokołów zapisanych za pomocą formalizmu rozszerzonych automatów czasowych. Praca ta opisuje translator z pewnego podzbioru Javy, popularnego ostatnio języka programistycznego, do rozszerzonych automatów czasowych i do języka pośredniego, formalizmów będących językami wejściowymi dla werifikatora Verics.
8
Content available remote ACTL* properties and Bounded Model Checking
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.
9
Content available remote Reaching the limits for Bounded Model Checking
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.
10
Content available remote Checking Reachability Properties for Timed Automata via SAT
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.
11
Content available remote SAT-Based Bounded Model Checking for the Universal Fragment of TCTL
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).
12
Content available remote Checking Reachability Properties for Timed Automata via SAT
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.
13
Content available remote Bounded Model Checking for the Universal Fragment of CTL
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.
14
Content available remote Branching Time Bounded Model Checking for Elementary Net Systems
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ć.