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

Znaleziono wyników: 17

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

help Ogranicz wyniki do:
first rewind previous Strona / 1 next fast forward last
1
Content available Cooperation of multiple autonomous robots and analysis of their swarm behawior
Czejdo B., Daszczuk W. B., Grabski W., Bhattacharya S.
Autobusy : technika, eksploatacja, systemy transportowe
|
2018
|
R. 19, nr 12
872--879
EN
In this paper, we extended previous studies of cooperating autonomous robots to include situations when environmental changes and changes in the number of robots in the swarm can affect the efficiency to execute tasks assigned to the swarm of robots. We have presented a novel approach based on partition of the robot behavior. The sub-diagrams describing sub-routs allowed us to model advanced interactions between autonomous robots using limited number of state combinations avoiding combinatorial explosion of reachability. We identified the systems for which we can ensure the correctness of robots interactions. New techniques were presented to verify and analyze combined robots’ behavior. The partitioned diagrams allowed us to model advanced interactions between autonomous robots and detect irregularities such as deadlocks, lack of termination etc. The techniques were presented to verify and analyze combined robots’ behavior using model checking approach. The described system, Dedan verifier, is still under development. In the near future, timed and probabilistic verification are planned.
PL
W artykule opisano kontynuację wcześniejszych badań dotyczących współpracy autonomicznych robotów wewnątrz budynku. Obejmują one obejmują sytuacje, w których zmiany środowiska i zmiana liczby robotów w roju mogą poprawić lub pogorszyć efektywność wykonywania zadań przypisanych do roju robotów. Zaprezentowaliśmy nowatorskie podejście z wykorzystaniem dzielenia zachowań robota na zachowania składowe. Poddiagramy opisujące kładowe podmarszruty pozwoliły nam modelować zaawansowane interakcje między autonomicznymi robotami w oparciu o ograniczoną liczbę kombinacji zachowań, unikając eksplozji kombinatorycznej przestrzeni osiągalności. Opisano systemy, dla których możemy zapewnić poprawność interakcji robotów i zaprezentowano techniki weryfikacji i analizy zachowań połączonych robotów. Diagramy podzielone na partycje pozwoliły nam modelować zaawansowane interakcje pomiędzy autonomicznymi robotami i wykrywać nieprawidłowości, takie jak zakleszczenia, brak terminacji itp. Przedstawiono techniki weryfikacji i analizy złożonych zachowań robotów za pomocą techniki weryfikacji modelowej. Opisany system weryfikacji, Dedan, jest wciąż rozwijany. W niedalekiej przyszłości planowana jest weryfikacja z czasem rzeczywistym i probabilistyczna.
2
Content available Model Checking Temporal Properties of Reaction Systems
Męski A., Penczek W., Rozenberg G.
Prace Instytutu Podstaw Informatyki Polskiej Akademii Nauk
|
2014
|
Nr 1028
1--28
EN
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. Finally, model checking for RSTL is proved to be PSPACE-complete.
PL
Praca wprowadza logikę temporalną dla systemów reakcyjnych (RSTL), która jest interpretowana w modelach dla systemów reakcyjnych z ograniczeniami kontekstów. Systemy te uogólniają standardowe systemy reakcyjne przez wprowadzenie ograniczeń kontrolujących dopuszczalne konteksty. Ponadto, przedstawiono translację z systemów reakcyjnych z ograniczeniami kontekstów do formuł boolowskich, która umożliwia symboliczną weryfikację modelową dla tych systemów oraz RSTL. Wykazano również, że problem weryfikacji modelowej dla RSTL jest problemem PSPACE-zupełnym.
3
Content available Weryfikowanie specyfikacji wymagań sterownika logicznego za pomocą diagramów aktywności UML, logiki temporalnej LTL i środowiska NuSMV
Grobelna I., Grobelny M.
Pomiary Automatyka Robotyka
|
2013
|
R. 17, nr 10
188--192
PL
W artykule przedstawiono ideę zastosowania diagramów aktywności UML do specyfikacji wymagań dotyczących zachowania sterownika logicznego. Lista wymagań podlegających weryfikacji zwykle definiowana jest bezpośrednio za pomocą formuł logiki temporalnej. Użycie przyjaznych dla użytkownika, powszechnie znanych i wykorzystywanych diagramów pozwala na prostsze i bardziej intuicyjne zapisanie wymagań. Diagramy są następnie formalnie przekształcane do formuł liniowej logiki temporalnej (LTL).
EN
The article introduces an idea to use UML activity diagrams [1-5] for specification of requirements regarding logic controller behavior. Requirements list to be verified [14] (using model checking technique [6, 7]) is usually directly defined using temporal logic formulas [12, 15]. Using user-friendly, commonly known and practiced diagrams allows to easier and more intuitively write down the requirements easier and more intuitively. Activity diagrams are then formally transformed into linear temporal logic (LTL) formulas. In this paper some sample UML activity diagrams which specify global properties are presented, together with their interpretation using LTL logic. To perform model checking process, model description (based i.e. on a control interpreted Petri net [8] or indirectly on an UML activity diagram [11]), and requirements list are needed. Afterwards it is checked, whether defined properties are satisfied in specified model description. If a requirement cannot be fulfilled, appropriate counterexample is generated allowing to localize error source. The article is structured as follows. Section 1 is an introduction. Background of a logic controller specification and its verification is presented in section 2. A novel approach to logic controller requirements definition using activity diagrams is shown in section 3. The paper ends with a short summary.
4
Content available Weryfikacja modelowa hierarchicznej specyfikacji sterownika logicznego
Grobelna I., Grobelny M.
Pomiary Automatyka Kontrola
|
2013
|
R. 59, nr 8
796--798
PL
Specyfikacja zachowania projektowanego urządzenia powinna uwzględniać wszystkie elementy behawioralne. Z uwagi na złożoność projektowanych systemów szczególnie istotną rolę odgrywa możliwość dekompozycji. Z wykorzystaniem hierarchii można podzielić specyfikację na logiczne elementy połączone ze sobą na diagramach wyższego poziomu. W artykule przedstawiono zagadnienia związane z formalną weryfikacją hierarchicznych specyfikacji sterownika logicznego wyrażonych za pomocą interpretowanych sieci Petriego oraz diagramów aktywności języka UML.
EN
Specification of a designed logic controller should include all behavioral aspects. By complex systems design decomposition is especially valuable. Specification can be divided into parts using hierarchy. Logical elements are joined together at higher-level diagrams. The paper focuses on formal verification [1] of logic controller hierarchical specification by means of UML activity diagrams and interpreted Petri nets. Although hierarchy itself is presented in the considered specification techniques in different ways (complex activities by UML activity diagrams and macro-places/ macrotransitions by Petri nets), it is possible to use both techniques together in one project and to transform anytime one diagram into the another [5, 9, 10] (example in Figs. 1 and 2). In the transformation process, UML activity diagram actions correspond to Petri net transitions [7, 8]. Model checking [2, 3] of hierarchical specification can be performed step by step, e.g. by means of the NuSMV tool [11]. Rule-based specification (based on a Petri net) can be checked against behavioral properties [12, 13] expressed by temporal logic formulas [4]. Macroplaces can be verified separately (Fig. 3 considering local properties) and/or concurrently (Fig. 4, Fig. 5 considering mutual correlation and global properties). Next, the whole Petri net with macroplaces can be checked (Fig. 6). Sometimes it is convenient to verify a complete net (not hierarchical), like in [14]. Formal verification of specification can significantly increase its quality, and the support for hierarchy simplifies complex systems verification.
5
Content available Weryfikacja modelowa interpretowanych sieci Petriego sterowania
Grobelna I.
Pomiary Automatyka Kontrola
|
2011
|
R. 57, nr 6
666-670
PL
Artykuł przedstawia oryginalne podejście do weryfikacji modelowej interpretowanych sieci Petriego sterowania. Sieci Petriego są powszechnie wykorzystywane w przemyśle. Najczęściej jednak weryfikowane są pod kątem właściwości strukturalnych, a właściwości behawioralne (mimo ich dużego znaczenia) są pomijane. Technika weryfikacji modelowej pozwala na weryfikację właściwości opisujących zachowanie projektowanego systemu. Model logiczny otrzymany na podstawie istniejącej sieci Petriego sterowania przedstawiany jest na poziomie RTL w taki sposób, że nadaje się zarówno do formalnej weryfikacji, jak i do syntezy logicznej jako rekonfigurowalny sterownik logiczny lub PLC.
EN
The paper introduces a novel approach to model checking with Control Interpreted Petri Nets [15]. Petri Nets [9, 11, 12, 13] are commonly used in the industry. However, they are mostly verified against structural properties, and behavioral properties are out of scope. The model checking technique [3, 7, 8, 21, 22] allows verifying properties which describe behavior of the designed system. Properties to be verified are expressed in temporal logic [16, 17, 18, 19, 20]. The logical model (Fig. 1) derived from existing Petri net is presented at RTL level (Register Transfer Level) in such a way, that it is easy to be formally verified as well as to logical synthesized as a reconfigurable logic controller or PLC (Programmable Logic Controller). It operates on variables which correspond to places, input and output signals of the Control Interpreted Petri Net (Section 3). The variables change their values according to some specified rules. The logical model is afterwards transformed into input format of the NuSMV model checker [23] and formally verified (Section 4). Control Interpreted Petri Net (Fig. 2) is divided into elementary subnets (Fig. 3). Each elementary subnet consists of a single place and its input and output transitions. Each elementary subnet is interpreted as a single segment of model description in the NuSMV tool. Each elementary subnet represents a two-states state machine which is usually realized as a single macrocell (Fig. 4) in the FPGA circuit. The properties to be verified are expressed in LTL or CTL logic. If any of them is not satisfied in the described system model, the appropriate counterexample is generated (Fig. 6). In the example in the paper the verification finds a subtle error resulting from incorrect / incomplete specification (Fig. 5) and allows the user to localize the error source.
6
Content available Regułowa reprezentacja interpretowanych sieci Petriego sterowania dla potrzeb syntezy i weryfikacji
Grobelna I.
Pomiary Automatyka Kontrola
|
2011
|
R. 57, nr 8
942-944
PL
Artykuł proponuje regułowy sposób reprezentacji interpretowanych sieci Petriego sterowania w logice temporalnej. Sposób ten jest przydatny zarówno do formalnej weryfikacji modelowej, jak i do automatycznej syntezy logicznej z wykorzystaniem języków opisu sprzętu (Verilog, VHDL) jako rekonfigurowalny sterownik logiczny lub PLC. Sieci Petriego weryfikowane są zwykle tylko pod kątem właściwości strukturalnych. Technika weryfikacji modelowej pozwala na weryfikację właściwości behawioralnych opisujących zachowanie projektowanego systemu.
EN
The paper presents a novel idea of Control Interpreted Petri Nets representation in temporal logic. The proposed logic representation is suitable both for formal model checking and automatic synthesis using hardware description languages (Verilog, VHDL). Petri Nets [1, 2, 3] are currently used in industry, i.e. by logic controller design [4]. Dedicated tools for creating Petri Nets support verification against structural properties. Behavioral properties are also of great importance, however they are rarely considered. Model checking technique [5] allows for verification of properties describing behavior of designed system. So far, there have been some approaches to verify (validate) specification by means of Petri Nets [6, 7, 8, 9], by means of UML diagrams [10] or logic controller programs in ST language [11]. However, none of them have addressed Control Interpreted Petri Nets focused on RTL level. The proposed rule-based representation of Control Interpreted Petri Nets (logical model in Figs. 2-5) is easy to formally verify (model description for NuSMV model checker [13] in Fig. 6-10), as well as to synthezise (VHDL model in Figs. 11-13) as a reconfigurable logic controller or PLC. Verified behavioral specification in temporal logic [14] is an abstract program of matrix reconfigurable logic controller functionality, and logic controller program (implementation) satisfies its primary specification. The logical model built from Control Inter-preted Petri Net describes it in a strict and short form.
7
Content available Petri nets and activity diagrams in logic controller specification – transformation and verification
Grobelna I., Grobelny M., Adamski M.
Zeszyty Naukowe. Telekomunikacja i Elektronika / Uniwersytet Technologiczno-Przyrodniczy w Bydgoszczy
|
2010
|
z. 13
79--91
EN
The paper presents formal verification method of logic controller specification taking into account user-specified properties. Logic controller specification may be expressed as Petri net or UML 2.0 Activity Diagram. Activity Diagrams seem to be more user-friendly and easy-understanding that Petri nets. Specification in form of activity diagram may afterwards be transformed into Petri net, which may then be formally verified and used to automatically generate implementation (code). A new transformation method dedicated for event-driven systems is proposed. Verification process is executed automatically by the NuSMV model checker tool. Model description based on specification and properties list is being built. Model description derived from Petri net is presented in RTL-level and easy to synthesize as reconfigurable logic controller or PLC. Properties are defined using temporal logic. In model checking process, verification tool checks whether requirements are satisfied in attached system model. If this is not the case, appropriate counterexamples are generated.
PL
Praca prezentuje metodę formalnej weryfikacji specyfikacji sterownika logicznego uwzględniającą właściwości podane przez użytkownika. Specyfikacja sterownika logicznego może być przedstawiona m.in. w postaci sieci Petriego lub diagramu aktywności języka UML. Diagramy aktywności wydają się być bardziej przyjazne i zrozumiałe dla użytkownika niż sieci Petriego. Specyfikacja w postaci diagramu aktywności może zostać przekształcona do sieci Petriego, która następnie może być formalnie zweryfikowana i wykorzystana do automatycznej generacji implementacji (kodu). Węzły diagramu aktywności konsekwentnie interpretowane są jako tranzycje sieci Petriego, w odróżnieniu od klasycznego podejścia (w starszych wersjach UML) gdzie odwzorowywało się je jako miejsca sieci Petriego. Proces weryfikacji wykonywany jest automatycznie przez narzędzia weryfikacji modelowej. Tworzony jest opis modelu bazujący na specyfikacji oraz lista wymagań. Nowatorskim podejściem jest przedstawienie sieci Petriego na poziomie RTL w taki sposób, że łatwo jest przeprowadzić syntezę logiczną sieci w postaci współbieżnego rekonfigurowalnego sterownika logicznego lub sterownika PLC bez konieczności przekształcania modelu. Wymagania określone są przy użyciu logiki temporalnej. W procesie weryfikacji modelowej narzędzie weryfikujące NuSMV sprawdza, czy model systemu spełnia stawiane mu wymagania. Jeżeli tak nie jest, generowany jest odpowiedni kontrprzykład.
8
Content available Diagramy aktywności języka UML i sieci Petriego w systemach sterowania binarnego - od transformacji do weryfikacji
Grobelny M., Grobelna I.
Pomiary Automatyka Kontrola
|
2010
|
R. 56, nr 10
1154-1158
PL
Język UML jest technologią powszechnie stosowaną w świecie naukowym oraz w przemyśle. Sieci Petriego są modelem matematycznym ogólnego zastosowania ugruntowanym od wielu lat. Obie te techniki doskonale nadają się do specyfikacji procesów sterowania. Jednakże jako odmienne, każda z nich posiada unikatowe właściwości. Technika weryfikacji modelowej jest jedną z metod formalnej weryfikacji specyfikacji pozwalającą na zdiagnozowanie błędów w specyfikacji wymagań albo w opisie modelu. Artykuł przedstawia metodę transformacji pomiędzy obiema wymienionymi technikami specyfikacji w celu formalnej weryfikacji projektu sterowania opisanego w języku UML.
EN
Unified Modeling Language (UML) [1-3, 5, 6-8] is commonly used in scientific and industrial world. Petri nets [9] are mathematical model used for a long period of time. Both techniques are well suited for control processes specification. However, they are quite different. Each technique has its own unique properties. Model checking technique [14-17] is one of formal verification methods [18] for specifications. It allows detecting errors either in requirements specification or in model description. The paper presents the method for transformation between both mentioned specification techniques - from UML activity diagram (Fig. 1) to Petri net (Fig. 4), using some defined rules [10, 11]. Mapping of particular elements is presented in Table 1. Petri net after direct transformation may include redundant places which can be after-wards removed. Then, it is possible to formally verify control process described in UML. The proposed model checker tool is NuSMV [20]. NuSMV (Fig. 5) compares model description (Fig. 6 - 8) and requirements (Fig. 9) which have to be fulfilled. The requirements are defined using temporal logic. If a specified requirement may not be fulfilled, appropriate counterexamples are generated (Fig. 10) which allow detecting an error source. Then, the specification can be corrected and model checking process can start again, sometimes including only the particular part of a designed system.
9
Content available Formal analysis of use case diagrams
Klimek R., Szwed P.
Computer Science
|
2010
|
Vol. 11
115-131
EN
Use case diagrams play an important role in modeling with UML. Careful modeling is crucial in obtaining a correct and efficient system architecture. The paper refers to the formal analysis of the use case diagrams. A formal model of use cases is proposed and its construction for typical relationships between use cases is described. Two methods of formal analysis and verification are presented. The first one based on a states' exploration represents a model checking approach. The second one refers to the symbolic reasoning using formal methods of temporal logic. Simple but representative example of the use case scenario verification is discussed.
PL
Diagramy przypadków użycia odgrywają znaczącą rolę w modelowaniu systemów z wykorzystaniem UML. Staranne i dokładne modelowanie ma zasadnicze znaczenie w postępowaniu umożliwiającym uzyskanie poprawnej i efektywnej architektury systemu. Artykuł odnosi się do formalnej analizy diagramów przypadków użycia. Został zaproponowany model formalny przypadku użycia, a także opisano odpowiednie konstrukcje dla relacji występujących pomiędzy przypadkami użycia. Zostały przedstawione dwie formalne metody ich analizy i weryfikacji. Pierwsza oparta jest na eksploracji stanów i reprezentuje podejście nazwane weryfikacją modelową. Druga odwołuje się do wnioskowania symbolicznego z wykorzystaniem logiki temporalnej. Został pokazany prosty i reprezentatywny przykład weryfikacji pewnego scenariusza przypadku użycia.
10
Content available remote Towards Scenarios of External Attacks upon Security Protocols
Dembiński P., Jakubowska G., Penczek W.
Prace Instytutu Podstaw Informatyki Polskiej Akademii Nauk
|
2008
|
nr 1012
1-24
EN
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 in order to look for an attack upon a protocol in the process of verification or simulation. We show that our algorithms generate scenarios of attacks upon all the protocols, classified within our taxonomy, which are known to susceptible to these attacks. We exemplify the results of our algorithms for several protocols from \cite{SPORE} and \cite{CJ}.
PL
Rozważamy taksonomię zewnętrznych ataków na protokoły kryptograficzne w terminach nazwy wysyłającego i odbierającego wiadmość oraz numeru kroku i sesji. Używamy tej taksonomii do zaprojektowania algorytmów, które dla zadanego typu ataku i parametrów protokołu, zwracają scenariusze ataku tego typu. W ten sposób bardzo istotnie redukujemy liczbę przebiegów protokołu, które mają byc wygenerowane w celu poszukiwania ataku na protokół w procesie weryfikacji lub symulacji W Raporcie jest pokazane, że nasze alorytmy generują scenariusze ataków na protokoły, sklasyfikowane w naszej taksonomii, na które istnieją ataki tego typu. Wyniki zastosowania algorytmów prezentujemy na przykładzie kilku protokołów z \cite{SPORE} i \cite{CJ}.
11
Content available remote Timed automata based model checking of timed security protocols
Kurkowski M., Penczek W.
Prace Instytutu Podstaw Informatyki Polskiej Akademii Nauk
|
2008
|
nr 1010
1-36
EN
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 BMC of the tool VerICS.
PL
W pracy przedstawiono nową metodę weryfikacji czasowych protokołów kryptograficznych. Sko\'nczona liczba użytkowników sieci oraz ich wiedza podczas wykonywania protokołu są modelowane przy pomocy automatów czasowych. Sieć automatów w pełni odzwierciedla zachowania podczas wykonywania protokołu niezbędne do weryfikowania założonych własności. Weryfikacja przeprowadzana jest za pomocą modułu BMC narzędzia VerICS.
12
Content available remote Semantyka operacyjna wybranych diagramów UML
Niewiadomski A., Penczek W. W., Szreter M.
Prace Instytutu Podstaw Informatyki Polskiej Akademii Nauk
|
2008
|
nr 1009
1-64
PL
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 definiowana za pomocą diagramu klas i obiektów, podczas gdy zachowanie systemu jest modelowane za pomocą maszyn stanowych. Wykonania zdefiniowanego w pracy systemu tranzycyjnego odpowiadają zachowaniu systemu opisanego za pomocą diagramów UML. Formalnie zdefiniowana semantyka umożliwia przejście do następnego etapu pracy, czyli zakodowania systemu specyfikowanego w UML jako formuły boolowskiej.
EN
The paper presents a semantics of a subset of UML in terms of a labelled transition system. Our further aim is to develop a symbolic model checker for UML based on this semantics. The UML fragment considered consists of class diagrams, object diagrams and state machine diagrams. A system specified in such a subset of UML consists of a set of objects and a set of communication and time events. The static structure of the system is defined by class and object diagrams, whereas its behaviour is determined by state machines. The behaviour of the labelled transition system corresponds to the behaviour of the system specified in UML. A global state consists of an active configuration of each object's statemachine, a valuation of all the variables, a content of event queues and a time component. The transition function defines the state changes corresponding to UML transitions and the time flow. The operational semantics defined as transition system is the starting point to the next stage of the work - a symbolic encoding of the system.
13
Content available remote Verifying Security Protocols Modeled by Networks of Automata
Kurkowski M., Penczek W.
Prace Instytutu Podstaw Informatyki Polskiej Akademii Nauk
|
2007
|
Nr 998
1-38
EN
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 proving either reachability or unreachability of an undesired state. We exemplify all our notions on the Needham Schroeder Public Key Authentication Protocol (NSPK) and show experimental results for checking authentication using the verification tool VerICS.
PL
Praca prezentuje nowa metodę modelowania wykonań protokołów kryptograficznych za pomocą sieci synchronizujacych się automatów. Problem badania własności protokołów został sprowadzony do problemu testowania osiagalności odpowiednich stanów globalnych w sieci. Do badań wykorzystuje się algorytmy SAT i narzędzie VerlCS. Jako przykład opisano budowę sieci automatów dla protokołu Needhama Schroedera (NSPK). Przedstawiono również pierwsze wyniki eksperymentalne oraz pierwsze porównania z wynikami uzyskanymi przy użyciu narzędzia SAT-MC (AVISPA).
14
Content available remote Model checking security protocols : a multi-agent system approach
Lomuscio A., Penczek W.
Prace Instytutu Podstaw Informatyki Polskiej Akademii Nauk
|
2007
|
Nr 1000
1-23
EN
We present a formalism for the automatic verification of security protocols based on multi-agent systems semantics. We give syntax and semantics of a temporal-epistemic security-specialised logie and provide a lazy-intruder model for the protocol rules that is arguably particularly suitable for verification purposes. We exemplify the techniąue by finding a (known) bug in the traditional NSPK protocol
PL
Praca prezentuje nowe podejście do automatycznej weryfikacji protokołów kryptograficznych, bazujące na semantyce systemów wieloagentowych. Podajemy składnię i semantykę temporalno-epistemicznej logiki dla protokołów kryptograficznych oraz model intruza typu "lazy", który jest szczególnie właściwy dla celów weryfikacji. Nasza technika jest przedstawiona na przykladzie protokołu NSPK, dla którego znajdujemy znany atak.
15
Content available Timed concurrent state machines
Daszczuk W. B.
Computer Science
|
2007
|
Vol. 8, Spec. Ed
23-36
EN
Timed Concurrent State Machines are an application of Alur Timed Automata concept to coincidence-based (rather than interleaving) CSM modeling technique. TCSM support the idea of testing automata, allowing to specify time properties easier than temporal formulas. Also, calculation of a global state space in real-time domain (Region Concurrent State Machines) is defined, allowing to storę a verified system in ready-to-verification form, and to multiply it by various testing automata.
PL
Współbieżne maszyny stanowe z czasem TCSM są aplikacją automatów czasowych Alura w środowisku koincydencyjnym współbieżnych maszyn czasowych CSM (w przeciwieństwie do środowisk przeplotowych). TCSM pasują do idei automatów testujących, które pozwalają wyspecyfikować zależności czasowe łatwiej niż poprzez formuły temporalne. Ponadto zdefiniowano sposób wyznaczania globalnej przestrzeni stanów w dziedzinie czasu (współbieżne maszyny stanowe regionów RCSM), co pozwala przechowywać badany system w postaci gotowej do weryfikacji i mnożyć go przez różne automaty testujące.
16
Content available remote Verifying Timed Properties of Security Protocols
Jakubowska G., Penczek W.
Prace Instytutu Podstaw Informatyki Polskiej Akademii Nauk
|
2006
|
Nr 991
1-38
EN
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 the specification to a timed automaton (or their networks). Moreover, we generalise the correspondence property so that attacks can be also discovered when some time constraints are not satisfied. Then, one can use each of the verification tools for timed automata (e.g., Kronos, UppAal, or Yerics) for model checking generalised time authentication of security protocols. As a case study we verify generalised (timed) authentication of KERBEROS, TMN, Neuman Stubblebine, and Andrew Secure Protocol.
PL
Weryfikacja własności zależnych od czasu dla protokołów uwierzytelniania stron. Proponujemy metodologię weryfikacji poprawności (czasowych) protokołów kryptograficznych, których akcje parametryzowane są czasem. W tym celu do modelu protokołu wprowadzone zostały opóźnienia, oczekiwania na tranzycjach oraz ustalone zostały ograniczenia czasowe dla akcji. Nasze podejście polega na specyfikacji protokołu (mogącego zawierać znaczniki czasu) w języku wysokiego poziomu i automatycznej translacji tej specyfikacji do automatu czasowego (lub do sieci automatów czasowych). Ponadto uogólniamy własność "correspondence" w taki sposób, by umożliwić wykrycie ataków, gdy pewne czasowe ograniczenia nie będą spełnione. Dzięki temu, korzystając z dowolnego narzędzia do weryfikacji automatów' czasowych (np. Kronos, UppAal, Yerics) możliwe jest sprawdzenie czy w modelu spełniona jest uogólniona czasowa własność uwierzytelnienia dla protokołów kryptograficznych. Jako przykłady przedstawiamy weryfikację protokołów KERBEROS, TMN, Neuman Stubblebine i Andrew Secure Protocol
17
Content available remote Unbounded Model Checking for Knowledge and Time
Kacprzak M., Lomuscio A., Penczek W.
Prace Instytutu Podstaw Informatyki Polskiej Akademii Nauk
|
2003
|
Nr 966
1-27
EN
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 systems literature. We give details of the technique and show howit can be applied to the well known train, gate and controller problem.
PL
Nieograniczona weryfikacja modelowa dla systemów z wiedzą i czasem. Praca dotyczy problemu weryfikacji epistemicznych własności systemów wieloagentowych za pomocą symbolicznej weryfikacji modelowej. Pokazujemy jak poszerzyć technikę zwaną nieograniczoną weryfikacją modelową stosowaną do badania temporalnych własności systemów tak, aby można było ją wykorzystać również do analizowania epistemicznych własności. W tym celu bazujemy na interpretowanych systemach - popularnej semantyce szeroko opisywanej w literaturze dotyczącej systemów wieloagentowych. Podajemy szczegóły techniki oraz demonstrujemy zastosowanie jej do znanego problemu kontroli przejazdów kolejowych.
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ć.