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ę "model sieci Petri" wg kryterium: Temat

  Lista filtrów
Wyrównaj
    Wyświetlanie 1-13 z 13
    Tytuł:
    DP2PN2Solver: A flexible dynamic programming solver software tool
    Autorzy:
    Mauch, H.
    Powiązania:
    https://bibliotekanauki.pl/articles/970851.pdf
    Data publikacji:
    2006
    Wydawca:
    Polska Akademia Nauk. Instytut Badań Systemowych PAN
    Tematy:
    sieć Bellmana
    model sieci Petri
    programowanie dynamiczne
    Bellman net
    dynamic programming
    matrix chain multiplication problem
    optimization software
    Petri net model
    traveling salesman problem
    Opis:
    Dynamic programming (DP) is a very general optimization technique, which can be applied to numerous decision problems that typically require a sequence of decisions to be made. The solver software DP2PN2Solver presented in this paper is a general, flexible, and expandable software tool that solves DP problems. It consists of modules on two levels. A level one module takes the specification of a discrete DP problem instance as input and produces an intermediate Petri net (PN) representation called Bellman net (Lew, 2002; Lew, Mauch, 2003, 2004) as output - a middle layer, which concisely captures all the essential elements of a DP problem in a standardized and mathematically precise fashion. The optimal solution for the problem instance is computed by an "executable" code (e.g. Java, Spreadsheet, etc.) derived by a level two module from the Bellman net representation. DP2PN2Solver's unique potential lies in its Bellman net representation. In theory, a PN's intrinsic concurrency allows to distribute the computational load encountered when solving a single DP problem instance to several computational units.
    Źródło:
    Control and Cybernetics; 2006, 35, 3; 687-702
    0324-8569
    Pojawia się w:
    Control and Cybernetics
    Dostawca treści:
    Biblioteka Nauki
    Artykuł
    Tytuł:
    Modelowanie i symulacja pracy złożonych systemów technicznych
    Modelling and Simulation of the Complex Technological Systems Operation
    Autorzy:
    KĘSY, Marek
    Powiązania:
    https://bibliotekanauki.pl/articles/457444.pdf
    Data publikacji:
    2015
    Wydawca:
    Uniwersytet Rzeszowski
    Tematy:
    model
    modelowanie
    symulacja
    sieci Petriego
    modelling
    simulation
    Petri nets
    Opis:
    Przedstawiono podstawowe informacje z zakresu modelowania systemów technicznych. Zaprezentowano możliwość modelowania złożonego systemu technicznego za pomocą modelu matematycznego – sieci Petriego, analizując ich praktyczną i dydaktyczną użyteczność.
    In the paper basic information regarding modelling of the technical systems has been presented. Modelling of the complex technical system was performed by Petri nets theory. Their professional and didactical useability has been analyzed.
    Źródło:
    Edukacja-Technika-Informatyka; 2015, 6, 3; 225-231
    2080-9069
    Pojawia się w:
    Edukacja-Technika-Informatyka
    Dostawca treści:
    Biblioteka Nauki
    Artykuł
    Tytuł:
    Czasowy model bloku przetwarzania danych w systemie pomiarowym
    Time Model of Data Processing Block in Measurement System
    Autorzy:
    Bilski, P.
    Łukaszewski, Ł.
    Powiązania:
    https://bibliotekanauki.pl/articles/151363.pdf
    Data publikacji:
    2007
    Wydawca:
    Stowarzyszenie Inżynierów i Techników Mechaników Polskich
    Tematy:
    systemy pomiarowe
    sieci Petriego
    model czasowy
    modelling
    Petri Nets
    measurement systems
    Opis:
    Artykuł dotyczy modelowania komputerowych systemów pomiarowo-sterujących (KSPS) uwzględniającej czasowe aspekty przepływu informacji w KSPS. W artykule zamieszczono opis części większych prac dotyczących nowej metody opisu modelu KSPS z wykorzystaniem sieci Petri`ego i narzędzia CPN Tools. Szczegółowo przedstawiono model bloku przetwarzania KSPS. Opisano dokładnie funkcje opóźnień zaimplementowane w modelu oraz metodą ich wyznaczania. Dodatkowo zamieszczono badania opóźnień bloku przetwarzania rzeczywistego KSPS oraz symulacje weryfikujące zaprojektowany model.
    The paper presents the method of the distributed measuring and control systems modelling, regarding the time aspects of the information flow inside the system. Results of the work including a new method of the measuring system model description using the Petri nets and CPN Tools are included. The data processing model inside the measuring system was presented in detail with delay functions implemented in the model. The paper is concluded with experimental results, comparing simulations with real measuring system behavior.
    Źródło:
    Pomiary Automatyka Kontrola; 2007, R. 53, nr 9 bis, 9 bis; 253-256
    0032-4140
    Pojawia się w:
    Pomiary Automatyka Kontrola
    Dostawca treści:
    Biblioteka Nauki
    Artykuł
    Tytuł:
    The functionally-oriented method for specialized EI-systems design application
    Funkcjonalnie zorientowana metoda projektowania aplikacji specjalistycznych systemów edukacyjnych i inteligentnych
    Autorzy:
    Mykhailiuk, A.
    Pukach, A.
    Powiązania:
    https://bibliotekanauki.pl/articles/408608.pdf
    Data publikacji:
    2014
    Wydawca:
    Politechnika Lubelska. Wydawnictwo Politechniki Lubelskiej
    Tematy:
    method
    model
    Petri nets
    design
    EI system
    sposób
    sieci Petriego
    projektowanie
    EI-systemy
    Opis:
    The algorithm and the model of the functionally-oriented method for specialized educational and intellectual systems (EI systems) automated design, based on Petri nets, are developed in the article. The example of the developed algorithm application for the real EI-system design is also given. The developed model based on Petri nets helps to identify the major states of the system synthesis process.
    W artykule rozpatrzono algorytm i model funkcjonalnie zorientowanej metody projektowania automatycznego specjalizowanych systemów edukacyjnych i inteligentnych (systemów EI) opartych na sieciach Petri. Przedstawiono również przykład tworzenia algorytmu aplikacji dla rzeczywistego projektowania systemu EI. Opracowano model oparty na sieci Petriego wspomagającej identyfikację głównych stanów systemu syntezy procesów
    Źródło:
    Informatyka, Automatyka, Pomiary w Gospodarce i Ochronie Środowiska; 2014, 2; 57-61
    2083-0157
    2391-6761
    Pojawia się w:
    Informatyka, Automatyka, Pomiary w Gospodarce i Ochronie Środowiska
    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ł:
    Using the Petri nets for forming the technological lines of the passenger trains processing in Ukraine
    Autorzy:
    Aleshinskiy, E.
    Naumov, V.
    Prymachenko, G.
    Powiązania:
    https://bibliotekanauki.pl/articles/224307.pdf
    Data publikacji:
    2016
    Wydawca:
    Polska Akademia Nauk. Czytelnia Czasopism PAN
    Tematy:
    passenger complexes
    passenger technical station
    Petri nets
    simulation model
    technological line
    pociągi pasażerskie
    sieci Petriego
    model symulacyjny
    linia technologiczna
    Opis:
    Despite the large number of publications, which authors use the mathematical apparatus of Petri nets for the transportation systems studies, there are still no such researches of technological processing lines for passenger trains on the territory of passenger complexes that aim to improve trains processing technology. In this article, we present simulation models of technological processing lines for passenger trains of different categories developed with the use of Petri nets. The structure of proposed simulation models is based on real time parallel-operating objects. Such an approach allows maximizing similarity of developed models and the simulated objects; in this way we achieve the increased adequacy of the obtained models. The article presents an interface of developed models and examples of their functioning under conditions of different input parameters, as well as the results of their use in order to reduce the passenger trains processing time. The proposed models are generic and could be applied for simulation of passenger trains processing at any station of Ukraine.
    Źródło:
    Archives of Transport; 2016, 38, 2; 7-15
    0866-9546
    2300-8830
    Pojawia się w:
    Archives of Transport
    Dostawca treści:
    Biblioteka Nauki
    Artykuł
    Tytuł:
    Interpretowane sieci Petriego - model formalny w zintegrowanym projektowaniu mikroprpcesorowych systemów sprzętowo-programowych
    Interpreted Petri nets as a formal model in hardware/software codesign
    Autorzy:
    Adamski, M.
    Skowroński, Z.
    Powiązania:
    https://bibliotekanauki.pl/articles/157576.pdf
    Data publikacji:
    2003
    Wydawca:
    Stowarzyszenie Inżynierów i Techników Mechaników Polskich
    Tematy:
    sieci Petriego
    programowanie zintegrowane
    mikroprocesorowe systemy sprzętowo-programowe
    Petri nets
    formal model in hardware/sofrware codesign
    Opis:
    Podejście systemowe do projektowania urządzeń o niejednorodnym charakterze wymaga stosowania formalnych metod specyfikacji, syntezy i analizy. Metody i narzędzia projektowe z kolei bazują na formalnym modelu obliczeniowym. Z tego względu dobór właściwego modelu ma fundamentalne znaczenie dla efektywności całego procesu projektowania. W pracy zaproponowano środowisko projektowe dla potrzeb zintegrowanego projektowania, w którym części sprzętowe systemu specyfikowane sa w języku VHDL, część programowa w języku C, a modelem formalnym są interpretowane sieci Petriego. Prezentowane wyniki prac znajdują również zastosowanie w projektowaniu mikrosystemów cyfrowych, zawierających układy FPGA.
    In order to model heterogeneous systems some common representation vehicle is needed. The model should have several features, the most important of wchich are : to be well suited both for software and hardware representation, allow for different manipulations (including partitioning) and be able to cope explicitly with parallelism. Interpreted Petri nets can meet all three requirements. The paper analyses the suitability of the petri nets for a representation of heterogeneous systems and outlines some practical aspects of the application of petri nets in modelling such systems.
    Źródło:
    Pomiary Automatyka Kontrola; 2003, R. 49, nr 2/3, 2/3; 17-20
    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ł:
    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ł
    Tytuł:
    Optymalizacja realizacji układowej hierarchicznych sieci Petriego
    The implementation optimization of the hierarchical Petri nets
    Autorzy:
    Stasiak, A.
    Powiązania:
    https://bibliotekanauki.pl/articles/152872.pdf
    Data publikacji:
    2007
    Wydawca:
    Stowarzyszenie Inżynierów i Techników Mechaników Polskich
    Tematy:
    projektowanie zintegrowane
    sieci Petriego
    model formalny
    systemy osadzone
    systemy cyfrowe
    mikrosystemy cyfrowe
    FPGA
    hardware-software codesign
    Petri nets
    formal model
    embedded systems
    digital systems
    digital microsystems
    PLD
    Opis:
    Projektowanie wysokiego poziomu systemów cyfrowych dotyczy szeregu aspektów związanych bezpośrednio z wybraną metodologią projektowania, modelem formalnym, algorytmami syntezy sprzętowej i programowej opisu behawioralnego. Rozważając sieci Petriego jako model formalny projektowanego systemu, szczególnie interpretowane hierarchiczne sieci Petriego, projektant ma do dyspozycji bogaty zbiór algorytmów analizy formalnej, metod syntezy programowej i sprzętowej. Jednak znane rozwiązania dotyczą przede wszystkim opisu zachowania funkcjonalnego sterowników logicznych, gdzie miejsce sieci reprezentuje logiczną operację przypisania poziomu '0' lub '1' do wyjścia układu (jeden bit lub wektor). Zauważalny jest jednak brak propozycji naukowych wspierających projektowanie systemu opisanego sieciami Petriego, gdzie w miejscu sieci realizowane są złożone instrukcje arytmetyczne lub logiczne. Przykładem sieci Petriego wspierającej w pełni projektowanie systemu sprzętowo-programowego jest siec PNHSDM (ang. Petri Net for Hardware So-ftware Digital Microsystem). Artykuł w sposób ogólny przedstawia model formalny sprzętowo-programowych sieci Petriego PNSHDM, skupiając się szczególnie na metodzie optymalizacji algorytmu syntezy sprzętowej sieci PNHSDM do reprogramowalnych układów FPGA. W pracy podjęto tematykę szeregowania zadań (ASAP, ALAP). Rozwiązano problem systemu przełączania sprzętowych modułów wykonawczych w kontekście planowanych do wykonania zadań. Wyznaczono wzór pozwalający na oszacowanie kosztów realizacji sprzętowej systemu przełączania, który zależny jest od liczby instancjacji i złożoności harmonogramowanej instrukcji.
    The high level designing concerns several aspects that are directly related to the designing methodology as well as formal model definition, hardware/software synthesis algorithms, etc. When a Petri nets are considered as a formal model of developing system, especially hierarchical interpreted Petri nets, then a designer has a lot of ready to use and very well documented algorithms dedicated for formal verification, hardware and software synthesis, transformations, etc. However, most of the know solutions for Petri nets concerns designing logic controllers, where a one net place implements simple assigning operation of logical state to the output. There is lack of solutions that use a Petri nets to formalize and describe really system, where a place implements complex algebraic or logic functions. A formal model based on Petri nets for hardware-software digital microsystems (PNHSDM) has been elaborated to eliminate this gap. This paper shortly describes PNHSDM model, but author have concentrate on optimization of hardware Petri nets synthesis algorithm that is responsible to translate functional description into VHDL-RTL language. This approach takes into consideration task scheduling (ASAP, ALAP), presents elaborated solution of switching system for PNHSDM Petri nets as well as provides static hardware cost estimations of the switching system.
    Źródło:
    Pomiary Automatyka Kontrola; 2007, R. 53, nr 5, 5; 108-110
    0032-4140
    Pojawia się w:
    Pomiary Automatyka Kontrola
    Dostawca treści:
    Biblioteka Nauki
    Artykuł
    Tytuł:
    Metody walidacji i weryfikacji specyfikacji funkcjonalnej mikrosystemu cyfrowego
    Validation and verification methods of the digital microsystem functional specification
    Autorzy:
    Stasiak, A.
    Skowroński, Z.
    Powiązania:
    https://bibliotekanauki.pl/articles/152874.pdf
    Data publikacji:
    2007
    Wydawca:
    Stowarzyszenie Inżynierów i Techników Mechaników Polskich
    Tematy:
    projektowanie zintegrowane
    sieci Petriego
    model formalny
    systemy osadzone
    systemy cyfrowe
    mikrosystemy cyfrowe
    FPGA
    hardware-software codesign
    Petri nets
    formal model
    embedded systems
    digital systems
    digital microsystems
    PLD
    Opis:
    Proces projektowy systemów cyfrowych, a w szczególności zintegrowanych sprzętowo-programowych mikrosystemów cyfrowych realizowanych z wykorzystaniem platformy SOPC, nie może być zakończony pomyślnie bez przeprowadzenia sprawdzenia i korekcji ewentualnych błędów projektowych. Do tego celu stosuje się metody walidacji zapisu specyfikacji funkcjonalnej zachowania systemu oraz metody weryfikacji funkcjonalnej projektowanego modelu. W artykule scharakteryzowano oraz omówiono opracowane na Uniwersytecie Zielonogórskim metody i oprogramowanie do walidacji i weryfikacji funkcjonalnej specyfikacji funkcjonalnej modelu opisanej sieciami Petriego.
    The design process of the today digital systems, especially integrated hardware-software digital microsystems for SOPC platform, can not be finalized successfully without the verification and debug process. To meet the product requirements, like: system functionality, system stability, time-to-market, project costs, etc; there has to be performed several validation and/or verification tasks to confirm the finale model behaviour with initial/input functional specification. This paper describes validation and verification methods as well as software/tools elaborated and developed at University of Zielona Góra, by the Computing and Engineering Department.
    Źródło:
    Pomiary Automatyka Kontrola; 2007, R. 53, nr 5, 5; 111-113
    0032-4140
    Pojawia się w:
    Pomiary Automatyka Kontrola
    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ł
      Wyświetlanie 1-13 z 13

      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