The Infona portal uses cookies, i.e. strings of text saved by a browser on the user's device. The portal can access those files and use them to remember the user's data, such as their chosen settings (screen view, interface language, etc.), or their login data. By using the Infona portal the user accepts automatic saving and using this information for portal operation purposes. More information on the subject can be found in the Privacy Policy and Terms of Service. By closing this window the user confirms that they have read the information on cookie usage, and they accept the privacy policy and the way cookies are used by the portal. You can change the cookie settings in your browser.
Model checking is an approach commonly applied for automated verification of reachability properties. Given a system and a property $p$, reachability model checking consists in an exploration of the state space of $S$, checking whether there exists a state where holds. Since concrete state spaces (models) of timed systems are usually infinite, they cannot be directly applied to model checking...
We present an approach to the problem of verification of epistemic properties in multi-agent systems by means of symbolic model checking. In particular, it isshown how to extend the technique of unbounded model checking from a purely temporal setting to a temporal-epistemic one. In order to achieve this, we baseour discussion on interpreted systems semantics, a popular semantics used in multi-agent...
In this paper we offer a methodology for verifying correctness of (timed) security protocols whose actions are parametrised with time. To this aim the model of a protocol involves delays and timeouts on transitions, and sets time constraints on actions to be executed. Our approach consists in specifying a security protocol, possibly with timestamps, in a higher-level language and translating automatically...
In this paper we show a novel method for modelling behaviours of security protocols using networks of communicating autornata in order to verify them with SAT-based bounded model checking. These autornata correspond to executions of the participants as well as to their knowledge about letters. Given a bounded number of sessions, we can verify both correctness or incorrectness of a security protocol...
Praca przedstawia semantykę operacyjną wybranego podzbioru UML w postaci etykietowanego systemu tranzycyjnego. Semantyka jest podstawą opracowywanego weryfikatora modelowego dla UML. Rozważany fragment UML zawiera diagramy klas, diagramy obiektów i diagramy maszyn stanowych. System modelowany za pomocą tych diagramów składa się ze zbioru obiektów oraz zbioru zdarzeń. Statyczna struktura systemu jest...
A new approach to verification of timed security protocols is given. The idea consists in modelling a finite number of users (including an intruder) of the computer network and their knowledge about secrets by timed automata. The runs of the product automaton of the above automata correspond to all the behaviours of the protocol for a fixed number of sessions. Verification is performed using the module...
In this paper we consider a taxonomy of external attacks on security protocols in terms of a message origin and destination in addition to a session and step number. We use this taxonomy for designing algorithms, which for a given type of attack and parameters of the protocol return a scenario of an attack of this type. This way we can dramatically reduce the number of protocol runs to be generated...
This paper defines a temporal logic for reaction systems (RSTL). The logic is interpreted over the models for the context restricted reaction systems that generalize standard reaction systems by controlling context sequences. Moreover, a translation from the context restricted reaction systems into boolean functions is defined in order to be used for a symbolic model checking for RSTL over these systems...
We investigate the correspondence between model checking of af-AMCi and ATLir , on the example of reachability. We identify some of the reasons for the fact that these logics are of uncomparable expressivity. These observations form the basis for a novel method for underapproximating ATLir by means of fixed-point calculations. We introduce a special version of the next-step operator, called Persistent...
Set the date range to filter the displayed results. You can set a starting date, ending date or both. You can enter the dates manually or choose them from the calendar.