Temat: model checking - Katalog OPAC zbiorów

Skocz do pozycji: 1.

Tytuł:: Translation of probabilistic games in J2TADD
Translacja gier probabilistycznych w J2TADD
Autorzy:: Rataj, A.
Powiązania:: https://bibliotekanauki.pl/articles/375653.pdf
Data publikacji:: 2013
Wydawca:: Polska Akademia Nauk. Czytelnia Czasopism PAN
Tematy:: model checking
Java
probabilistic game
Opis:: A new version of J2TADD - a translator from Java to automatons- is described, which adds support for a translation of Markov processes with non-dcterministic players, that can form coalitions, which in turn strive for different aims. In order to ease the definition of a probabilistic game using a plain Java application, several new constructs, and also a special library, are supported within the input language.Ranges on variables or on expressions can be defined, what helps in checking the self-consistency of a model, and can also make the solving of the model faster.
Artykuł prezentuje nową wersję translatora J2TADD. Dodane zostało tłumaczenie procesów markowowskich z niedelerministycznymi graczami, mogącymi formować koalicje mające różne cele. By ułatwić pisanie gier probabilistycznych dodane zostało kilka specyficznych dla gier konstrukcji, jak również specjalna biblioteka. Aktualnej wersja posiada również kilka innych usprawnień: ● wybory, które są zwykłymi wyrażeniami języka Java, jednak hc tłumaczy je na specyficzne dla automatów rozgałęzienia probabilistyczne lub niedeterministyczne; ● można definiować dopuszczalne wartości zmiennych, co pomaga w sprawdzaniu wewnętrznej spójności modelu, a także może przyspieszyć jego rozwiązanie; ● różne metody specyfikacji niezmienników i warunków zegarowych. Artykuł prezentuje jako przykład prostą grę probabilistyczną, modelującą rynek lokalnego dostawcy energii elektrycznej. W ramach przykładu omawiane są wersje automatów do rozwiązywania metodą analityczną i symulacyjną.
Źródło:: Theoretical and Applied Informatics; 2013, 25, 3-4; 157-182
1896-5334
Pojawia się w:: Theoretical and Applied Informatics
Dostawca treści:: Biblioteka Nauki

Artykuł

Zmień widok

na półce

Skocz do pozycji: 2.

Tytuł:: The modal mu-calculus: a survey
Autorzy:: Lenzi, G.
Powiązania:: https://bibliotekanauki.pl/articles/1964197.pdf
Data publikacji:: 2005
Wydawca:: Politechnika Gdańska
Tematy:: mu-calculus
fixed points
model checking
Opis:: The modal mu-calculus is an extension of modal logic with two operators mu and ni, which give the least and greatest fixpoints of monotone operators on powersets. This powerful logic is widely used in computer science, in the area of verification of correctness of concurrent systems. In this survey we review both the theoretical aspects of the modal mu-calculus and its applications to computer science.
Źródło:: TASK Quarterly. Scientific Bulletin of Academic Computer Centre in Gdansk; 2005, 9, 3; 293-316
1428-6394
Pojawia się w:: TASK Quarterly. Scientific Bulletin of Academic Computer Centre in Gdansk
Dostawca treści:: Biblioteka Nauki

Artykuł

Zmień widok

na półce

Skocz do pozycji: 3.

Tytuł:: Underapproximating ATL with Imperfect Information and Imperfect Recall
Dolna Aproksymacja Bezpamięciowego ATL o Niepełnej Informacji
Autorzy:: Jamroga, W.
Knapik, M.
Powiązania:: https://bibliotekanauki.pl/articles/182675.pdf
Data publikacji:: 2015
Wydawca:: Polska Akademia Nauk. Instytut Podstaw Informatyki PAN
Tematy:: ATL
model checking
approximation
weryfikacja
aproksymacja
Opis:: 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 Imperfect Next-Step Operator h_iF and show how it can be used to define a new version of reachability that carries to ATLir.
W pracy badane są związki pomiędzy weryfikacją modelową Bezpamięciowej Logiki Temporalnej Czasu Alternującego z Niepełną Informacją ATLir i Epistemicznego Alternującego Mu-Rachunku af-AMCi. Jak pokazano, naturalne uogólnienia pojęcia osiągalności z ATLir -a do af-AMCi nie przynoszą dobrych efektów: osiągalność w af-AMCi nie pociąga za sobą osiągalności w ATLir . Po zidentyfikowaniu części powodów, dla których tak się dzieje, zaproponowano nową wersję operatora następnego kroku, który pozwala na przybliżanie osiągalności w ATLir przy pomocy obliczeń stałopunktowych.
Źródło:: Prace Instytutu Podstaw Informatyki Polskiej Akademii Nauk; 2015, 1032; 1-16
0138-0648
Pojawia się w:: Prace Instytutu Podstaw Informatyki Polskiej Akademii Nauk
Dostawca treści:: Biblioteka Nauki

Artykuł

Zmień widok

na półce

Skocz do pozycji: 4.

Tytuł:: Modelling CTMC with a standard programming language and using conventions from computer networking
Modelowanie łańcuchów Markowa z czasem ciągłym przy użyciu standardowego języka programowania i z zastosowaniem konwencji z dziedziny sieci komputerowych
Autorzy:: Rataj, A.
Nowak, M.
Pecka, P.
Powiązania:: https://bibliotekanauki.pl/articles/375742.pdf
Data publikacji:: 2011
Wydawca:: Polska Akademia Nauk. Czytelnia Czasopism PAN
Tematy:: Markov chain
continuous time
model checking
Java
Opis:: Continuous time Markov chains (CTMC) are one of the formalisms for building models. This paper discusses expressing these models in a standard programming language – Java. Using such a language as a model description allows for a partially common implementation of the production software and of the description of the model, for a greater flexibility in comparison to model-checker specific languages that often do not employ features of an object-oriented programming. Using Java also makes the parsing of models relatively fast, using optimised Java runtime environment. Our approach aims at using typical mechanisms of the Java language when implementing the model, and at the same time, following closely the concepts from computer networking and from formalisms based on it, like the queueing systems. These assumption result in techniques like plain object fields constituting the state vector, or negotiation between nodes to decide if an event happens.
Łańcuchy Markowa czasu rzeczywistego są jednym z formalizmów używanych do budowy modeli. Artykuł ten omawia wyrażanie takich modeli w standardowym języku programowania - Javie. Użycie takiego języka umożliwia częściowo wspólną implementację oprogramowania użytkowego i opisu modelu, większą elastyczność w porównaniu do często nie używających obiektowych konwencji programistycznych języków stosowanych przez oprogramowanie weryfikujące, oraz szybką budowę modelu z użyciem zoptymalizowanego środowiska czasu wykonania Javy. Nasze podejście miało na celu wykorzystanie typowych mechanizmów języka Java przy opisie modelu i jednoczesnie trzymanie się konwencji z dziedziny sieci komputerowych i pokrewnych formalizmóm typu systemy kolejkowe. Dlatego używamy technik takich jak zastosowanie pól obiektów jako elementów wektora stanu czy negocjacja pomiędzy węzłami, czy dane zdarzenie ma mieć miejsce.
Źródło:: Theoretical and Applied Informatics; 2011, 23, 3-4; 229-243
1896-5334
Pojawia się w:: Theoretical and Applied Informatics
Dostawca treści:: Biblioteka Nauki

Artykuł

Zmień widok

na półce

Skocz do pozycji: 5.

Tytuł:: Comparing sat-based bounded model checking rtectl and ectl properties
Autorzy:: Zbrzezny, A. M.
Powiązania:: https://bibliotekanauki.pl/articles/297995.pdf
Data publikacji:: 2017
Wydawca:: Uniwersytet Warmińsko-Mazurski w Olsztynie
Tematy:: SAT
bounded model checking
ECTL
RTECTL
translation
Opis:: 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.
Źródło:: Technical Sciences / University of Warmia and Mazury in Olsztyn; 2017, 20(2); 131-147
1505-4675
2083-4527
Pojawia się w:: Technical Sciences / University of Warmia and Mazury in Olsztyn
Dostawca treści:: Biblioteka Nauki

Artykuł

Zmień widok

na półce

Skocz do pozycji: 6.

Tytuł:: UML Verification with Verics
Autorzy:: Niewiadomski, A.
Penczek, W.
Powiązania:: https://bibliotekanauki.pl/articles/92916.pdf
Data publikacji:: 2007
Wydawca:: Uniwersytet Przyrodniczo-Humanistyczny w Siedlcach
Tematy:: model checking
UML
unified modeling language
VerICS
Opis:: We show how to verify UML specifications against properties expressed by CTL-like formulas using the symbolic model checker Verics. Our method is illustrated with an example showing a verification of Alternating Bit Protocol.
Źródło:: Studia Informatica : systems and information technology; 2007, 1(8); 19-31
1731-2264
Pojawia się w:: Studia Informatica : systems and information technology
Dostawca treści:: Biblioteka Nauki

Artykuł

Zmień widok

na półce

Skocz do pozycji: 7.

Tytuł:: A GPGPU–based simulator for prism: statistical verification of results of PMC
Autorzy:: Copik, M.
Rataj, A.
Woźna-Szcześniak, B.
Powiązania:: https://bibliotekanauki.pl/articles/121899.pdf
Data publikacji:: 2017
Wydawca:: Uniwersytet Humanistyczno-Przyrodniczy im. Jana Długosza w Częstochowie. Wydawnictwo Uczelniane
Tematy:: GPGPU
symulacja Monte Carlo
pryzmat
probabilistyczny model statystyczny
Monte Carlo simulation
prism
probabilistic model checking
statistical model checking
probabilistic logics
Opis:: We describe a GPGPU–based Monte Carlo simulator integrated with Prism. It supports Markov chains with discrete or continuous time and a subset of properties expressible in PCTL, CSL and their variants extended with rewards. The simulator allows an automated statistical verification of results obtained using Prism’s formal methods.
Źródło:: Scientific Issues of Jan Długosz University in Częstochowa. Mathematics; 2017, 22; 85-97
2450-9302
Pojawia się w:: Scientific Issues of Jan Długosz University in Częstochowa. Mathematics
Dostawca treści:: Biblioteka Nauki

Artykuł

Zmień widok

na półce

Skocz do pozycji: 8.

Tytuł:: Unbounded Model Checking for ATL
Autorzy:: Kański, Michał
Niewiadomski, Artur
Kacprzak, Magdalena
Penczek, Wojciech
Nabiałek, Wojciech
Powiązania:: https://bibliotekanauki.pl/articles/2175150.pdf
Data publikacji:: 2021
Wydawca:: Uniwersytet Przyrodniczo-Humanistyczny w Siedlcach
Tematy:: ATL
temporal logics
model checking
SAT
SMT
QBF
Opis:: In this paper, we deal with verification of multi-agent systems represented as concurrent game structures. To express properties to be verified, we use Alternating-Time Temporal Logic (ATL) formulas. We provide an implementation of symbolic model checking for ATL and preliminary, but encouraging experimental results.
Źródło:: Studia Informatica : systems and information technology; 2021, 1-2(25); 5--22
1731-2264
Pojawia się w:: Studia Informatica : systems and information technology
Dostawca treści:: Biblioteka Nauki

Artykuł

Zmień widok

na półce

Skocz do pozycji: 9.

Tytuł:: Improving Dependability of Automation for Free Electron Laser FLASH
Autorzy:: Kosęda, B.
Szmuc, T.
Cichalewski, W.
Powiązania:: https://bibliotekanauki.pl/articles/384861.pdf
Data publikacji:: 2009
Wydawca:: Sieć Badawcza Łukasiewicz - Przemysłowy Instytut Automatyki i Pomiarów
Tematy:: automation
formal methods
model checking
expert system
Prolog
flash
Opis:: Free-electron laser FLASH (260-meter-long machine) is a pilot facility for the forthcoming XFEL (3 km). Along with growth of the experiment, service and maintenance are becoming so complex that certain degree of automation seems to be inevitable. The main purpose of the automation software is to facilitate operators with computer-aided supervision of several hardware/software subsystems. The efforts presented in this contribution concern elaboration of general framework for designing and development of automation software for the FLASH. The toolkit facilitates specification, implementation, testing and formal verification. The ultimate goal of the framework is to systematize the way of automation software development and to improve its dependability. At present usefulness of the tools is being evaluated by testing the automation software for single RF-power station of the FLASH.
Źródło:: Journal of Automation Mobile Robotics and Intelligent Systems; 2009, 3, 1; 33-39
1897-8649
2080-2145
Pojawia się w:: Journal of Automation Mobile Robotics and Intelligent Systems
Dostawca treści:: Biblioteka Nauki

Artykuł

Zmień widok

na półce

Skocz do pozycji: 10.

Tytuł:: Model checking processes specified in join-calculus algebra
Autorzy:: Maludziński, S.
Dobrowolski, G.
Powiązania:: https://bibliotekanauki.pl/articles/305715.pdf
Data publikacji:: 2014
Wydawca:: Akademia Górniczo-Hutnicza im. Stanisława Staszica w Krakowie. Wydawnictwo AGH
Tematy:: join-calculus
model checking
formal methods
automatic software verification
Opis:: This article presents a model checking tool used to verify concurrent systems specified in join-calculus algebra. The temporal properties of systems under verification are expressed in CTL logic. Join-calculus algebra, with its operational semantics defined by a chemical abstract machine, serves as the basic method for the specification of concurrent systems and their synchronization mechanisms, allowing for the examination of more complex systems. The described model checker is a proof of concept for the utilization of new methodologies of formal system specification and verification in software engineering practice.
Źródło:: Computer Science; 2014, 15 (1); 61-74
1508-2806
2300-7036
Pojawia się w:: Computer Science
Dostawca treści:: Biblioteka Nauki

Artykuł

Zmień widok

na półce

Skocz do pozycji: 11.

Tytuł:: Component Composition Validation
Autorzy:: Speck, A.
Pulvermuller, E.
Jerger, M.
Franczyk, B.
Powiązania:: https://bibliotekanauki.pl/articles/908508.pdf
Data publikacji:: 2002
Wydawca:: Uniwersytet Zielonogórski. Oficyna Wydawnicza
Tematy:: informatyka
composition verification
component composition
feature interaction
model checking
Opis:: Many approaches such as component technologies have been invented in order to support software reuse. Based on these technologies a large variety of techniques have been introduced to connect components. However, there is little experience concerning the validation of component systems. We know how to plug components together, but we do need ways to check whether that works. In this paper we introduce an approach to validating component compositions and showing how such a process can be supported by tools. We introduce a way to compare the interface specification of components automatically against the code. Furthermore, we demonstrate how compositions of components can be specified by logical formulas, allowing us to automatically validate these compositions.
Źródło:: International Journal of Applied Mathematics and Computer Science; 2002, 12, 4; 581-589
1641-876X
2083-8492
Pojawia się w:: International Journal of Applied Mathematics and Computer Science
Dostawca treści:: Biblioteka Nauki

Artykuł

Zmień widok

na półce

Skocz do pozycji: 12.

Tytuł:: Formalna weryfikacja maszyny stanów z wykorzystaniem logiki temporalnej
Formal verification of a state machine with use of temporal logic
Autorzy:: Grobelna, I.
Powiązania:: https://bibliotekanauki.pl/articles/154298.pdf
Data publikacji:: 2009
Wydawca:: Stowarzyszenie Inżynierów i Techników Mechaników Polskich
Tematy:: algorytmiczne maszyny stanów ASM
logika temporalna
technika Model Checking
algorithmic state machines ASM
temporal logic
formal verification of specification
Model Checking technique
Opis:: Artykuł przedstawia koncepcję specyfikacji współbieżnego procesu sterowania cyfrowego za pośrednictwem diagramów algorytmicznych maszyn stanów ASM w języku aprobowanym przez profesjonalne narzędzie model checker. Specyfikacja może zostać następnie formalnie zweryfikowana pod kątem wymagań stawianych projektowanemu systemowi. Lista wymagań tworzona jest przy wykorzystaniu liniowej logiki temporalnej LTL. Formalna weryfikacja Model Checking polega na sprawdzeniu, czy model systemu spełnia stawiane mu wymagania. W przypadku wykrycia niespóności generowany jest odpowiedni kontrprzykład.
The paper presents the formal specification method of concurrent control processes in form of algorithmic state machines ASM [5] in a language accepted by a professional model checker tool NuSMV. Basing on linear temporal logic LTL [7, 8, 9, 16] a requirement list (Fig. 6) for the system model is prepared. Formal verification Model Checking [17, 19] consists in comparison of the model description and the requirements list. If some requirements cannot be fulfilled, the appropriate counterexample is generated (Fig. 7), which allows localizing the error source. The ASM diagrams (Fig. 4) are fully determined, but they do not support modularity, that is why they are not well suited for specification of concurrent controlling processes. The paper includes a short introduction to the theory of algorithmic state machines ASM (Section 2), temporal logic (Section 3) and model checking technique (Section 4). The proposed solution is presented on an example (Section 5) of the process of controlling (partially concurrent) movements of two vehicles (Fig. 2). The formal verification method of the ASM diagrams with its advantages and disadvantages as well as the general conclusions are given at the end of the paper (Section 6).
Źródło:: Pomiary Automatyka Kontrola; 2009, R. 55, nr 7, 7; 457-460
0032-4140
Pojawia się w:: Pomiary Automatyka Kontrola
Dostawca treści:: Biblioteka Nauki

Artykuł

Zmień widok

na półce

Skocz do pozycji: 13.

Tytuł:: Tools and Methods for RTCP-Nets Modeling and Verification
Autorzy:: Szpyrka, M.
Biernacki, J.
Biernacka, A.
Powiązania:: https://bibliotekanauki.pl/articles/229254.pdf
Data publikacji:: 2016
Wydawca:: Polska Akademia Nauk. Czytelnia Czasopism PAN
Tematy:: RTCP-nets
Petri nets
model checking
coverability graphs
nuXmv
CADP
Opis:: RTCP-nets are high level Petri nets similar to timed colored Petri nets, but with different time model and some structural restrictions. The paper deals with practical aspects of using RTCP-nets for modeling and verification of real-time systems. It contains a survey of software tools developed to support RTCP-nets. Verification of RTCP-nets is based on coverability graphs which represent the set of reachable states in the form of directed graph. Two approaches to verification of RTCP-nets are considered in the paper. The former one is oriented towards states and is based on translation of a coverability graph into nuXmv (NuSMV) finite state model. The later approach is oriented towards transitions and uses the CADP toolkit to check whether requirements given as μ-calculus formulae hold for a given coverability graph. All presented concepts are discussed using illustrative examples.
Źródło:: Archives of Control Sciences; 2016, 26, 3; 339-365
1230-2384
Pojawia się w:: Archives of Control Sciences
Dostawca treści:: Biblioteka Nauki

Artykuł

Zmień widok

na półce

Skocz do pozycji: 14.

Tytuł:: Improving modified policy iteration for probabilistic model checking
Autorzy:: Mohagheghi, Mohammadsadegh
Karimpour, Jaber
Isazadeh, Ayaz
Powiązania:: https://bibliotekanauki.pl/articles/27312850.pdf
Data publikacji:: 2022
Wydawca:: Akademia Górniczo-Hutnicza im. Stanisława Staszica w Krakowie. Wydawnictwo AGH
Tematy:: probabilistic model checking
Markov decision processes
modified policy iteration
probabilistic reachability
Opis:: Along with their modified versions, value iteration and policy iteration are well-known algorithms for the probabilistic model checking of Markov decision processes. One challenge with these methods is that they are time-consuming in most cases. Several techniques have been proposed to improve the performance of iterative methods for probabilistic model checking; however, the running times of these techniques depend on the graphical structure of the utilized model. In some cases, their performance can be worse than the performance of standard methods. In this paper, we propose two new heuristics for accelerating the modified policy iteration method. We first define a criterion for the usefulness of the computations of each iteration of this method. The first contribution of our work is to develop and use a criterion to reduce the number of iterations in modified policy iteration. As the second contribution, we propose a new approach for identifying useless updates in each iteration. This method reduces the running time of the computations by avoiding the useless updates of states. The proposed heuristics have been implemented in the PRISM model checker and applied on several standard case studies. We compare the running time of our heuristics with the running times of previous standard and improved methods. Our experimental results show that our techniques yields a significant speed-up.
Źródło:: Computer Science; 2022, 23 (1); 63--80
1508-2806
2300-7036
Pojawia się w:: Computer Science
Dostawca treści:: Biblioteka Nauki

Artykuł

Zmień widok

na półce

Skocz do pozycji: 15.

Tytuł:: Modeling and analysis of probabilistic real-time systems through integrating event-b and probabilistic model checking
Autorzy:: Debbi, Hichem
Powiązania:: https://bibliotekanauki.pl/articles/27312896.pdf
Data publikacji:: 2022
Wydawca:: Akademia Górniczo-Hutnicza im. Stanisława Staszica w Krakowie. Wydawnictwo AGH
Tematy:: event-B
probabilistic event-B
real-time probabilistic model checking
PTA
PRISM
Opis:: Event-B is a formal method that is used in the development of safety-critical systems; however, these systems may introduce uncertainty and also need to meet real-time requirements, which make the modeling and analysis of such systems a challenging task. While some works exist that try to extend Event-B with probability and over time, they fail to address both in a single framework. Besides, these works mainly addressed extending the language itself, not integrating extended Event-B with verification. In this paper, we aim to represent both probability and time in the Event-B language, and we will show how such a representation can be automatically translated into the probabilistic timed automata (PTA) that are described in the language of the PRISM probabilistic model checker. This transformation approach would allow us to analyze the probabilistic and time-bounded probabilistic reachability properties of probabilistic real-time systems through probabilistic timed CTL (PTCTL) logic.
Źródło:: Computer Science; 2022, 23 (4); 545--570
1508-2806
2300-7036
Pojawia się w:: Computer Science
Dostawca treści:: Biblioteka Nauki

Artykuł

Zmień widok

na półce

Skocz do pozycji: 16.

Tytuł:: Model Checking Temporal Properties of Reaction Systems
Weryfikacja temporalnych własności systemów reakcyjnych
Autorzy:: Męski, A.
Penczek, W.
Rozenberg, G.
Powiązania:: https://bibliotekanauki.pl/articles/182724.pdf
Data publikacji:: 2014
Wydawca:: Polska Akademia Nauk. Instytut Podstaw Informatyki PAN
Tematy:: reaction systems
model checking
temporal logic
systemy reakcyjne
weryfikacja modelowa
logika temporalna
Opis:: 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.
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.
Źródło:: Prace Instytutu Podstaw Informatyki Polskiej Akademii Nauk; 2014, 1028; 1-28
0138-0648
Pojawia się w:: Prace Instytutu Podstaw Informatyki Polskiej Akademii Nauk
Dostawca treści:: Biblioteka Nauki

Artykuł

Zmień widok

na półce

Skocz do pozycji: 17.

Tytuł:: Code generation for CSM/ECSM models in COSMA environment
Generacja kodu programu na podstawie modelu CSM/ECSM w środowisku COSMA
Autorzy:: Grabski, W.
Nowacki, M.
Powiązania:: https://bibliotekanauki.pl/articles/305423.pdf
Data publikacji:: 2007
Wydawca:: Akademia Górniczo-Hutnicza im. Stanisława Staszica w Krakowie. Wydawnictwo AGH
Tematy:: weryfikacja
COSMA
generacja kodu
CSM
ECSM
automaty skończenie stanowe
model checking
code generation
FSM
Opis:: The COSMA software environment, developed in the Institute of Computer Science, WUT, was designed primarily for model checking of reactive systems specified in terms of Concurrent State Machines (CSM). However, COSMA supports also Extended CSM (ECSM). The extensions allow for using complex data types and pieces of C/C++ code, attributed to CSM states and/or transitions. Because of these extensions, ECSM models cannot be verifed by model checking, but they can be used as an intermediate step in code generation. The underlying CSM represent then the flow of control within cooperating components and the communication among them while the extensions specify the data structures and the details of their processing. The paper discusses the code generation from ECSM diagrams. The approach is illustrated with an example.
Środowisko COSMA, rozwijane w Instutycie Informatyki Politechniki Warszawskiej, powstało z myślą o weryfikacji modeli (model checking) systemów reaktywnych specyfikowanych przy pomocy automatów CSM (Concurrent State Machines) jak i ich rozszerzonej wersji (ECSM - Extended CSM). Rozszerzenie CSM o złożone struktury danych, atrybuty związane z przejściami i stanami oraz możliwość bezpośredniego użycia kody w C/C++ powodują, że model wyrażony w ECSM nie może być formalnie weryfikowany, a jedynie stanowić krok pośredni przy generacji kodu. W takim podejściu model CSM reprezentuje sterowanie i komunikację pomiędzy modułami systemu, podczas gdy ECSM - dane i szczegóły przetwarzania. Artykuł omawia generację kodu z modelu ECSM zilustrowaną przykładem.
Źródło:: Computer Science; 2007, 8, Spec. Ed; 49-59
1508-2806
2300-7036
Pojawia się w:: Computer Science
Dostawca treści:: Biblioteka Nauki

Artykuł

Zmień widok

na półce

Skocz do pozycji: 18.

Tytuł:: Regułowa reprezentacja interpretowanych sieci Petriego sterowania dla potrzeb syntezy i weryfikacji
Rule-based representation of Control Interpreted Petri Nets for synthesis and verification purposes
Autorzy:: Grobelna, I.
Powiązania:: https://bibliotekanauki.pl/articles/155260.pdf
Data publikacji:: 2011
Wydawca:: Stowarzyszenie Inżynierów i Techników Mechaników Polskich
Tematy:: weryfikacja modelowa
interpretowane sieci Petriego sterowania
synteza logiczna
model checking
control interpreted Petri nets
Opis:: 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.
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.
Źródło:: Pomiary Automatyka Kontrola; 2011, R. 57, nr 8, 8; 942-944
0032-4140
Pojawia się w:: Pomiary Automatyka Kontrola
Dostawca treści:: Biblioteka Nauki

Artykuł

Zmień widok

na półce

Skocz do pozycji: 19.

Tytuł:: Diagramy aktywności języka UML i sieci Petriego w systemach sterowania binarnego - od transformacji do weryfikacji
UML activity diagrams and Petri nets in binary control systems - from transformation to verification
Autorzy:: Grobelny, M.
Grobelna, I.
Powiązania:: https://bibliotekanauki.pl/articles/158260.pdf
Data publikacji:: 2010
Wydawca:: Stowarzyszenie Inżynierów i Techników Mechaników Polskich
Tematy:: diagramy aktywności UML
sieci Petriego
weryfikacja modelowa
UML activity diagrams
Petri nets
model checking
Opis:: 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.
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.
Źródło:: Pomiary Automatyka Kontrola; 2010, R. 56, nr 10, 10; 1154-1158
0032-4140
Pojawia się w:: Pomiary Automatyka Kontrola
Dostawca treści:: Biblioteka Nauki

Artykuł

Zmień widok

na półce

Skocz do pozycji: 20.

Tytuł:: A symbolic shortest path algorithm for computing subgame-perfect Nash equilibria
Autorzy:: Góngora, P. A
Rosenblueth, D. A.
Powiązania:: https://bibliotekanauki.pl/articles/329934.pdf
Data publikacji:: 2015
Wydawca:: Uniwersytet Zielonogórski. Oficyna Wydawnicza
Tematy:: shortest path
Bellman–Ford algorithm
Nash equilibrium
BDD
model checking
najkrótsza ścieżka
równowaga Nasha
sprawdzanie modelu
Opis:: Consider games where players wish to minimize the cost to reach some state. A subgame-perfect Nash equilibrium can be regarded as a collection of optimal paths on such games. Similarly, the well-known state-labeling algorithm used in model checking can be viewed as computing optimal paths on a Kripke structure, where each path has a minimum number of transitions. We exploit these similarities in a common generalization of extensive games and Kripke structures that we name “graph games”. By extending the Bellman–Ford algorithm for computing shortest paths, we obtain a model-checking algorithm for graph games with respect to formulas in an appropriate logic. Hence, when given a certain formula, our model-checking algorithm computes the subgame-perfect Nash equilibrium (as opposed to simply determining whether or not a given collection of paths is a Nash equilibrium). Next, we develop a symbolic version of our model checker allowing us to handle larger graph games. We illustrate our formalism on the critical-path method as well as games with perfect information. Finally, we report on the execution time of benchmarks of an implementation of our algorithms.
Źródło:: International Journal of Applied Mathematics and Computer Science; 2015, 25, 3; 577-596
1641-876X
2083-8492
Pojawia się w:: International Journal of Applied Mathematics and Computer Science
Dostawca treści:: Biblioteka Nauki

Artykuł

Zmień widok

na półce

Skocz do pozycji: 21.

Tytuł:: Logic in formal verification of computer systems. Some remarks
Logika i formalna weryfikacja systemów komputerowych. Kilka uwag
Autorzy:: Trzęsicki, K.
Powiązania:: https://bibliotekanauki.pl/articles/341099.pdf
Data publikacji:: 2009
Wydawca:: Politechnika Białostocka. Oficyna Wydawnicza Politechniki Białostockiej
Tematy:: logika
weryfikacja
metoda teorio-dowodowa
sprawdzanie za pomocą modelu
logic
verification
proof-theoretical method
model checking
Opis:: Various logics are applied to specification and verification of both hardware and software systems. The problem with finding of proof is the most important disadvantage of proof-theoretical method. The proof-theoretical method presupposes the axiomatization of the logic. Proprieties of a system can also be checked using a model of the system. A model is constructed with the specification language and checked using automatic model checkers. The model checking application presupposes the decidability of the task.
Do specyfikacji i weryfikacji zarówno sprzętu jak i programów stosowane są różne logiki. Główną wadą metody teorio-dowodowej weryfikacji jest problem znalezienia dowodu. Zastosowanie tej metody zakłada aksjomatyzację logiki. Własności systemu mogą być sprawdzane za pomocą jego modelu. Model jest zbudowany w języku specyfikacji i sprawdzany automatycznie. Zastosowanie sprawdzania za pomocą modelu zakłada rozstrzygalność zadania. Istnieje wielka różnorodność programów (model checker) do sprawdzania własności za pomocą modeli.
Źródło:: Zeszyty Naukowe Politechniki Białostockiej. Informatyka; 2009, 4; 151-175
1644-0331
Pojawia się w:: Zeszyty Naukowe Politechniki Białostockiej. Informatyka
Dostawca treści:: Biblioteka Nauki

Artykuł

Zmień widok

na półce

Skocz do pozycji: 22.

Tytuł:: Weryfikowanie specyfikacji wymagań sterownika logicznego za pomocą diagramów aktywności UML, logiki temporalnej LTL i środowiska NuSMV
Verification of logic controller requirements specification by means of UML activity diagrams, LTL temporal logic and NuSMV tool
Autorzy:: Grobelna, I.
Grobelny, M.
Powiązania:: https://bibliotekanauki.pl/articles/277589.pdf
Data publikacji:: 2013
Wydawca:: Sieć Badawcza Łukasiewicz - Przemysłowy Instytut Automatyki i Pomiarów
Tematy:: diagramy aktywności UML
specyfikacja
model logiczny
weryfikacja modelowa
logika temporalna
UML activity diagrams
specification
logical model
model checking
temporal logic
Opis:: 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).
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.
Źródło:: Pomiary Automatyka Robotyka; 2013, 17, 10; 188-192
1427-9126
Pojawia się w:: Pomiary Automatyka Robotyka
Dostawca treści:: Biblioteka Nauki

Artykuł

Zmień widok

na półce

Skocz do pozycji: 23.

Tytuł:: Weryfikacja modelowa hierarchicznej specyfikacji sterownika logicznego
Model checking of hierarchical logic controller specification
Autorzy:: Grobelna, I.
Grobelny, M.
Powiązania:: https://bibliotekanauki.pl/articles/153829.pdf
Data publikacji:: 2013
Wydawca:: Stowarzyszenie Inżynierów i Techników Mechaników Polskich
Tematy:: hierarchia
interpretowane sieci Petriego
diagramy aktywności UML
weryfikacja modelowa
hierarchy
interpreted Petri nets
UML activity diagrams
model checking
Opis:: 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.
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.
Źródło:: Pomiary Automatyka Kontrola; 2013, R. 59, nr 8, 8; 796-798
0032-4140
Pojawia się w:: Pomiary Automatyka Kontrola
Dostawca treści:: Biblioteka Nauki

Artykuł

Zmień widok

na półce

Skocz do pozycji: 24.

Tytuł:: Timed concurrent state machines
Współbieżne maszyny stanowe z czasem
Autorzy:: Daszczuk, W. B.
Powiązania:: https://bibliotekanauki.pl/articles/305419.pdf
Data publikacji:: 2007
Wydawca:: Akademia Górniczo-Hutnicza im. Stanisława Staszica w Krakowie. Wydawnictwo AGH
Tematy:: metody formalne
weryfikacja modelowa
weryfikacja w czasie rzeczywistym
automaty czasowe
formal methods
model checking
real time verification
Timed Automata
Opis:: 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.
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.
Źródło:: Computer Science; 2007, 8, Spec. Ed; 23-36
1508-2806
2300-7036
Pojawia się w:: Computer Science
Dostawca treści:: Biblioteka Nauki

Artykuł

Zmień widok

na półce

Skocz do pozycji: 25.

Tytuł:: Quantitative safety analysis of train control system based on statistical model checking
Autorzy:: Lin, Junting
Min, Xiaoqin
Powiązania:: https://bibliotekanauki.pl/articles/2124711.pdf
Data publikacji:: 2022
Wydawca:: Polska Akademia Nauk. Czytelnia Czasopism PAN
Tematy:: train control systems
statistical model checking
safety analysis
hybrid automata
UPPAAL-SMC
system sterowania pociągiem
analiza bezpieczeństwa
automaty hybrydowe
Opis:: With the rapid development of communication technology, the Train-centric Communication-based Train Control (TcCBTC) system adopting the train-train communication mode to reduce the transmission link of control information, will become the direction of urban rail transit field development. At present, TcCBTC system is in the stage of key technology research and prototype development. Uncertain behavior in the process of system operation may lead to operation accidents. Therefore, before the system is put into use, it must undergo strict testing and security verification to ensure the safe and efficient operation of the system. In the paper, the formal modeling and quantitative analysis of train tracking operation under moving block are carried out. Firstly, the structure of TcCBTC system and the train tracking interval control strategy under moving block conditions are analyzed. The subsystem involved in train tracking and the uncertain factors in system operation are determined. Then, based on the Stochastic Hybrid Automata (SHA), a network of SHA model of train dynamics model, communication components and on-board controller in the process of train tracking is established, which can formally describe the uncertain environment in the process of system operation. UPPAAL-SMC is used to simulate the change curve of train position and speed during tracking, it is verified that the model meets the safety requirements in static environment. Finally, taking Statistical Model Checking (SMC) as the basis of safety analysis, the probability of train collision in uncertain environment is calculated. The results show that after accurately modeling the train tracking operation control mechanism through network of SHA, the SMC method can accurately calculate the probability of train rearend collision, which proves that the method has strong feasibility and effectiveness. Formal modeling and analysis of safety-critical system is very important, which enables designers to grasp the hidden dangers of the system in the design stage and safety evaluation stage of train control system, and further provides theoretical reference for the subsequent TcCBTC system design and development, practical application and related specification improvement.
Źródło:: Archives of Transport; 2022, 61, 1; 7--19
0866-9546
2300-8830
Pojawia się w:: Archives of Transport
Dostawca treści:: Biblioteka Nauki

Artykuł

Zmień widok

na półce

Skocz do pozycji: 26.

Tytuł:: Formal analysis of use case diagrams
Formalna analiza diagramów przypadków użycia
Autorzy:: Klimek, R.
Szwed, P.
Powiązania:: https://bibliotekanauki.pl/articles/305621.pdf
Data publikacji:: 2010
Wydawca:: Akademia Górniczo-Hutnicza im. Stanisława Staszica w Krakowie. Wydawnictwo AGH
Tematy:: UML
przypadek użycia
model formalny
weryfikacja
weryfikacja modelowa
logika temporalna
metoda tablic semantycznych
use case
formal model
verification
model checking
temporal logic
semantic tableau
Opis:: 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.
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.
Źródło:: Computer Science; 2010, 11; 115-131
1508-2806
2300-7036
Pojawia się w:: Computer Science
Dostawca treści:: Biblioteka Nauki

Artykuł

Zmień widok

na półce

Skocz do pozycji: 27.

Tytuł:: Weryfikacja modelowa interpretowanych sieci Petriego sterowania
Model checking of control interpreted Petri Nets
Autorzy:: Grobelna, I.
Powiązania:: https://bibliotekanauki.pl/articles/152412.pdf
Data publikacji:: 2011
Wydawca:: Stowarzyszenie Inżynierów i Techników Mechaników Polskich
Tematy:: weryfikacja modelowa
sterownik logiczny
interpretowane sieci Petriego sterowania
logika temporalna
model checking
logic controller
control interpreted Petri nets
temporal logic
Opis:: 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.
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.
Źródło:: Pomiary Automatyka Kontrola; 2011, R. 57, nr 6, 6; 666-670
0032-4140
Pojawia się w:: Pomiary Automatyka Kontrola
Dostawca treści:: Biblioteka Nauki

Artykuł

Zmień widok

na półce

Skocz do pozycji: 28.

Tytuł:: Cooperation of multiple autonomous robots and analysis of their swarm behawior
Współpraca roju autonomicznych robotów i analiza ich zbiorowych zachowań
Autorzy:: Czejdo, B.
Daszczuk, W. B.
Grabski, W.
Bhattacharya, S.
Powiązania:: https://bibliotekanauki.pl/articles/316981.pdf
Data publikacji:: 2018
Wydawca:: Instytut Naukowo-Wydawniczy "SPATIUM"
Tematy:: autonomous robots
behavior verification
model checking
integrated model of distributed systems
deadlock
termination
autonomiczne roboty
weryfikacja zachowań
weryfikacja modelowa
zintegrowany model systemów rozproszonych
zakleszczenie
terminacja
Opis:: 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.
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.
Źródło:: Autobusy : technika, eksploatacja, systemy transportowe; 2018, 19, 12; 872-879
1509-5878
2450-7725
Pojawia się w:: Autobusy : technika, eksploatacja, systemy transportowe
Dostawca treści:: Biblioteka Nauki

Artykuł

Zmień widok

na półce

Skocz do pozycji: 29.

Tytuł:: Petri nets and activity diagrams in logic controller specification – transformation and verification
Sieci petriego i diagramy aktywności w specyfikacji sterowników logicznych – transformacja i weryfikacja
Autorzy:: Grobelna, I.
Grobelny, M.
Adamski, M.
Powiązania:: https://bibliotekanauki.pl/articles/389795.pdf
Data publikacji:: 2010
Wydawca:: Politechnika Bydgoska im. Jana i Jędrzeja Śniadeckich. Wydawnictwo PB
Tematy:: formal verification
logic controller
model checking
Petri nets
UML Activity
Diagrams
formalna weryfikacja
sterownik logiczny
weryfikacja modelowa
sieci Petriego
diagramy aktywności UML
Opis:: 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.
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.
Źródło:: Zeszyty Naukowe. Telekomunikacja i Elektronika / Uniwersytet Technologiczno-Przyrodniczy w Bydgoszczy; 2010, 13; 79-91
1899-0088
Pojawia się w:: Zeszyty Naukowe. Telekomunikacja i Elektronika / Uniwersytet Technologiczno-Przyrodniczy w Bydgoszczy
Dostawca treści:: Biblioteka Nauki

Artykuł

Zmień widok

na półce

Informacja

Wyszukujesz frazę "model checking" wg kryterium: Temat

Źródło danych

Dostawca treści

Kolekcja

Rok wydania

Wydawca

Temat

Autor

Typ dokumentu

Język