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

Znaleziono wyników: 9

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

help Ogranicz wyniki do:
first rewind previous Strona / 1 next fast forward last
1
Content available Generation of synchronizing state machines from a transition system: A region-based approach
Teren Viktor, Cortadella Jordi, Villa Tiziano
International Journal of Applied Mathematics and Computer Science
|
2023
|
Vol. 33, no. 1
133--149
EN
Transition systems (TSs) and Petri nets (PNs) are important models of computation ubiquitous in formal methods for modeling systems. A crucial problem is how to extract, from a given TS, a PN whose reachability graph is equivalent (with a suitable notion of equivalence) to the original TS. This paper addresses the decomposition of transition systems into synchronizing state machines (SMs), which are a class of Petri nets where each transition has one incoming and one outgoing arc. Furthermore, all reachable markings (non-negative vectors representing the number of tokens for each place) of an SM have only one marked place with only one token. This is a significant case of the general problem of extracting a PN from a TS. The decomposition is based on the theory of regions, and it is shown that a property of regions called excitation-closure is a sufficient condition to guarantee the equivalence between the original TS and a decomposition into SMs. An efficient algorithm is provided which solves the problem by reducing its critical steps to the maximal independent set problem (to compute a minimal set of irredundant SMs) or to satisfiability (to merge the SMs). We report experimental results that show a good trade-off between quality of results vs. computation time.
2
Content available Analysis of safeness in a Petri net-based specification of the control part of cyber-physical systems
Wojnakowski Marcin, Wiśniewski Remigiusz, Bazydło Grzegorz, Popławski Mateusz
International Journal of Applied Mathematics and Computer Science
|
2021
|
Vol. 31, no. 4
647--657
EN
The paper proposes an algorithm for safeness verification of a Petri net-based specification of the control part of cyber-physical systems. The method involves a linear algebra technique and is based on the computation of the state machine cover of a Petri net. Contrary to the well-known methods, the presented idea does not require obtaining all sequential components, nor the computation of all reachable states in the system. The efficiency and effectiveness of the proposed method have been verified experimentally with a set of 243 test modules (Petri net-based systems). The results of experiments show high efficiency of the proposed method since a solution has been found even for such nets where popular techniques are not able to analyze the safeness of the system. Finally, the presented algorithm is explained in detail using a real-life case-study example of the control part of a cyber-physical system.
3
Content available From UML object behavior description into petri net models towards systematic development of embedded systems
Szmuc W., Szmuc T.
International Journal of Microelectronics and Computer Science
|
2016
|
Vol. 7, nr 2
60--64
EN
The paper describes a translation of object behavior specified by UML into semantically equivalent Petri net models. The translation focuses on object behavior with event handling implemented in UML. The resulted Petri net allows to check UML model properties not only by simulation but also in formal way. For possibly closest congruence between UML and Petri net model an event queue is defined. Each state machine assigned to an object has its own event queue which is available as long as the machine exists. It allows modeling not just a simple message passing but also cases, when state machine cannot handle an event. A higher priority of sub-machine's event queue is also considered. The presented solution is a part of wider conversion algorithm from UML model into Petri nets [12]. However, the paper is intended to describe the issue in such a detailed way and focuses on aspects crucial for embedded systems development.
4
Content available remote Synthesis of controller for railway – level crossing devices using Petri nets and state machine
Mielnik R.
Czasopismo Techniczne. Elektrotechnika
|
2016
|
Y. 113, iss. 1-E
101--112
EN
The design of modern digital measurement-control systems applied in such fields as nuclear and power, chemical, air and rail transport as well as military requires a special approach to the philosophy of design, manufacture and the use of such systems. Therefore, attention should be focused on safeguarding the required level of reliability and safety of working conditions of such systems. On an example of a controller for an automatic railway crossing devices is presented synthesis of this controller. In this fact were used Petri nets – to modeling this controller and state machine – to make programming application.
PL
Projektowanie cyfrowych systemów pomiarowo-sterujących stosowanych w takich obszarach jak: energetyka jądrowa, przemysł chemiczny, transport powietrzny i kolejowy oraz zastosowania militarne wymaga specjalnego podejścia do filozofii projektowania, produkcji i eksploatacji tego typu. Systemy te wymagają zapewnienia odpowiedniego poziomu niezawodności i bezpieczeństwa. Na przykładzie sterownika samoczynnej sygnalizacji przejazdowej przedstawiono jego syntezę z wykorzystaniem sieci Petriego – do modelowania funkcji kontrolera, oraz maszyny stanów – do wykonania oprogramowania.
5
Content available Wykorzystanie pseudostanów historii do modelowania sytuacji awaryjnych w maszynie stanów UML
Bazydło G., Adamski M., Stefanowicz Ł.
Pomiary Automatyka Kontrola
|
2014
|
R. 60, nr 7
513--515
PL
W artykule przedstawiono zagadnienia związane z modelowaniem obsługi sytuacji awaryjnych opierając się na metodzie syntezy behawioralnej sterowników logicznych opisanych diagramami maszyny stanowej UML. Szczególną uwagę zwrócono na wykorzystanie pseudostanów historii a także zdarzeń i przejść zakończenia (typu completion event), przejść wysokiego poziomu, stanów końcowych i przejść bezwarunkowych. Celem zaproponowanej metody jest takie przekształcenie modelu hierarchicznej maszyny stanów UML, aby otrzymać opis układu w języku opisu sprzętu Verilog. Metoda została poparta stosownym przykładem układu sterowania.
EN
The paper presents the design methodology for deriving Verilog descriptions from UML state machine diagrams (Figs. 2, 3) in order to capture the behavioral hierarchy in the array structure of an embedded system. The exception handling is introduced at the top level of the graphical specification. As an intuitive example the interrupt is introduced. It illustrates the case of a system failure, when the control is temporarily transferred to exceptional safe and determined behavior. The precise semantic interpretation of the UML 2.4 state machine diagrams ensures, under the proposed structural design rules, that the Verilog description conserves modular properties of an initial specification. The behavioral hierarchy of the UML state machine is directly mapped into a structural hierarchy inside the designed reconfigurable controller. The tree of properly encapsulated submachines allows independent simulation and modification of particular parts of the behavioral model. In the paper the emphasis is put on the support of modeling an emergency situation with use of history pseudostates, high-level transitions and completion events. The way of hardware implementation of storing the information about the previously active state is also presented (Fig. 5). The most important algorithm of the proposed method is illustrated by an appropriate example (Fig. 1).
6
Content available remote Algorytm pracy programowalnego sterownika z optycznym sprzężeniem zwrotnym
Gilewski M.
Przegląd Elektrotechniczny
|
2012
|
R. 88, nr 5a
158-161
PL
W publikacji przedstawiono algorytm pracy autorskiego opracowania sterownika diod laserowych oraz LED. Algorytm został zakodowany w języku VHDL. Postać końcową kompilacji zaimplementowano w strukturze FPGA. Na podstawie amplitudy fotoprądu zwrotnego algorytm wyznacza natężenie prądu zasilającego diodę laserową. Przedstawione rozwiązanie umożliwia elastyczne sterowanie prądowym punktem pracy diody laserowej lub LED. Aplikację można również wykorzystać do syntezy charakterystyk przejściowych prądu zasilającego diody.
EN
The article presents the control algorithm of LEDs and laser diodes driver. This algorithm has been imlemented in VHDL. The source code was compiled using the Quartus II Web Edition software. The resulting bitsream is used to program FPGA. The algorithm dynamically calculates the current value of the laser diode. For this purpose it uses the current value of the monitor diode. The algorithm can also be applied to the synthesis of transient characteristics of LEDs or laser diodes.
7
Content available remote Konwersja wybranych elementów maszyny stanów UML w ramach dualnej specyfikacji
Doligalski M.
Przegląd Elektrotechniczny
|
2009
|
R. 85, nr 7
192-195
PL
W artykule przedstawiono metodę dywersyfikacji specyfikacji behawioralnej jako odpowiedź na zapotrzebowanie rynku na nowe techniki modelowania. Przedstawiono model dualny w postaci połączonej maszyny stanów UML oraz hierarchicznej sieci Petriego. Zastosowanie modelu dualnego pozwala na zwiększenie jakości oraz niezawodności sterownika logicznego, skraca czas projektowania. Maszyna stanów UML pełni rolę interfejsu użytkownika, izomorficzna do niej hierarchiczna sieć Petriego bazę do weryfikacji formalnej i implementacji układowej.
EN
In the paper method of the specification diversification was proposed. Also dual model based on hierarchical Petri net and UML state machine diagram was presented as a response for market demand for new modeling techniques. The application of dual model make possible quality grow and controller developing time short. The UML state ma-chine diagram act as front-end and according to UML SM diagram Petri net as back-end - base for formal verification and implementation. The dual specification was presented in context of logical controller developing process.
8
Content available System SMCAD wspomagający projektowanie częściowo rekonfigurowalnych sterowników logicznych
Doligalski M., Mrowiec P.
Pomiary Automatyka Kontrola
|
2009
|
R. 55, nr 7
504-507
PL
Rozwój technologii półprzewodnikowych, dynamiczny wzrost pojemności i funkcjonalności układów FPGA stwarza nowe możliwości funkcjonalne, które z powodów ograniczeń współcześnie stosowanego oprogramowania projektowego nie mogą być w pełni wykorzystanie. W referacie opisano moduł graficznego edytora systemu SMCAD - wspomagającego projektowanie oraz przeprowadzenie procesu częściowej rekonfiguracji sterowników logicznych. W artykule opisano moduł graficzny systemu SMCAD, który umożliwia modelowanie behawioralne sterowników logicznych z wykorzystaniem diagramów maszyny stanów UML.
EN
Evolution of silicon technology, dynamic growth of FPGA device capacity and functionality requires introducing new techniques and developing new design tools. The application of a Petri net as a form of specification is a common solution used in the field of discrete systems. The application of the UML language, especially the state machine diagrams, is a perfect solution. These diagrams enable the hierarchical modelling of programs with concurrent elements. The UML language makes it possible to shorten the time of designing such a system and to optimise the use of hardware resources of the controller. There is no editor of the UML state machine diagrams dedicated to logic controller developing. In this paper the graphical editor module of an SMCAD system is presented. The SMCAD system is driven on reprogrammable logic controller partial reconfiguration. The new graphical editor enables behavioural modelling based on the UML state machine diagrams. Section 2 describes the graphical editor advantages compared to the existing, classical, software engineering driven UML tools like: Sybase Power Designer, ArgoUML, StarUML. It also gives the reasons for implementing the new editor. The supported subset of the UML state machine diagrams is presented in Section 3. In Section 4 there is shown an example of the manufacturing process outline (Fig. 2). The process of developing logic controller specification for the exemplary schema is also contained in this section. The behavioural specification in form of the UML state machine diagrams (Figs. 3 and 5) shows the partial reconfiguration process. The graphic specification was exported in the SCXML format (Fig. 8). Lack of possibility of do actions specification justifies the proposal of SCXML standard extension (Fig. 8).
9
Bezpośrednie sterowanie procesem technologicznym z wykorzystaniem Windows Workflow Foundation
Jestratjew A., Kwiecień A.
Prace Naukowe Instytutu Informatyki Stosowanej Politechniki Wrocławskiej. Konferencje
|
2007
533-547
PL
Jednym ze sposobów sterowania procesem przemysłowym przez komputer klasy PC jest sterowanie bezpośrednie, z wykorzystaniem specjalizowanych kart wejść/wyjść analogowych i/lub cyfrowych oraz odpowiedniego oprogramowania. W rozdziale przeanalizowano możliwość wykorzystania środowiska .NET Framework wraz z Windows Workflow Foundation jako podstawy implementacji oprogramowania bezpośrednio sterującego procesem przemysłowym. Zwrócono przy tym szczególną uwagę na problem determini-zmu czasowego wykonania aplikacji. Na przykładzie rzeczywistej aplikacji w systemie sterowania pompownią głębinową zaproponowano wielowarstwową architekturę oprogramowania i przedstawiono metody programowania, których wykorzystanie umożliwia realizację algorytmu sterowania procesem technologicznym z tzw. "miękkimi" ograniczeniami czasowymi (ang. soft real-time). Pokazano konieczne modyfikacje architektury celu wykorzystania Windows Workflow Foundation. Na podstawie pomiarów wykonanych w środowisku rzeczywistym i testowym dokonano oceny własności czasowych aplikacji.
EN
Personal computers equipped with specialized analog and digital input/output expansion cards and control software are often used as direct controllers of soft-real time processes, e.g. in industry. The paper analyses whether it is possible to use Microsoft .NET Framework and Windows Workflow Foundation in order to create reliable control software for soft real-time processes. Special concern is made on behavior of the software in time domain, i.e. time determinism of software execution. Basic ideas are illustrated by example of control software that has been made for pump station in mining industry.
first rewind previous Strona / 1 next fast forward last
JavaScript jest wyłączony w Twojej przeglądarce internetowej. Włącz go, a następnie odśwież stronę, aby móc w pełni z niej korzystać.