Informacja

Drogi użytkowniku, aplikacja do prawidłowego działania wymaga obsługi JavaScript. Proszę włącz obsługę JavaScript w Twojej przeglądarce.

English (EN)·Polski (PL)·Yкраїнський (UK)
Przejdź do strony domowej biblioteki Centralna Biblioteka Wojskowa Link otwiera się w nowym oknie Logo biblioteki Prolib Integro - strona głównaCentralna Biblioteka Wojskowa

Wyszukujesz frazę "weryfikacja" wg kryterium: Temat

  Lista filtrów
Wyrównaj
    Wyświetlanie 1-10 z 10
    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ł
    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ł
    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ł
    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ł
    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ł
    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ł
    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ł
    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ł
    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ł
    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ł
      Wyświetlanie 1-10 z 10

      Ta witryna wykorzystuje pliki cookies do przechowywania informacji na Twoim komputerze. Pliki cookies stosujemy w celu świadczenia usług na najwyższym poziomie, w tym w sposób dostosowany do indywidualnych potrzeb. Korzystanie z witryny bez zmiany ustawień dotyczących cookies oznacza, że będą one zamieszczane w Twoim komputerze. W każdym momencie możesz dokonać zmiany ustawień dotyczących cookies