Serwis Infona wykorzystuje pliki cookies (ciasteczka). Są to wartości tekstowe, zapamiętywane przez przeglądarkę na urządzeniu użytkownika. Nasz serwis ma dostęp do tych wartości oraz wykorzystuje je do zapamiętania danych dotyczących użytkownika, takich jak np. ustawienia (typu widok ekranu, wybór języka interfejsu), zapamiętanie zalogowania. Korzystanie z serwisu Infona oznacza zgodę na zapis informacji i ich wykorzystanie dla celów korzytania z serwisu. Więcej informacji można znaleźć w Polityce prywatności oraz Regulaminie serwisu. Zamknięcie tego okienka potwierdza zapoznanie się z informacją o plikach cookies, akceptację polityki prywatności i regulaminu oraz sposobu wykorzystywania plików cookies w serwisie. Możesz zmienić ustawienia obsługi cookies w swojej przeglądarce.
We introduce a new methodology for the specification and the design of the control logic of automated manufacturing systems. Our aim is to make specification express just what is necessary earlier in the design process. This permits to produce an optimized work cycle for the system and makes both production recovery calculation and code generation easier. The methodology is based on a modular modeling...
Since it is an important issue for users and system designers, verification of PLC programs has already been studied in various contexts, mostly for untimed programs. More recently, timed features were introduced and modeled with timed automata. In this case study, we consider a part of the so-called MSS (mecatronic standard system) platform from Bosh group, a framework where time aspects are combined...
Industrial automation is currently on the cusp to the application of distributed systems based on distributed intelligence enabling distributed decision making within control. As one main technology within this field IEC 61499 based function block systems would be applied. But the usage of function block systems may cause problems which have to be avoided prior to the integration of a function block...
This paper presents the planned and on-going activities inside the FORDESIGN research project, funded by the Portuguese FCT (Foundation for Science and Technology), whose main objective is to foster the effective use of formal methods for embedded systems co-design. The project proposes a methodology where the use-cases are used as a starting point, not only for capturing requirements but also to...
The paper presents an approach to obtain a closed-loop model of controlled manufacturing systems. The major obstacle in applying such models to formal verification of real systems is the effort that is needed to design a formal model of the plant behavior. We show in this contribution how a semi-formal description of the plant, called pneumatic equipment plan, can be used to reduce the effort to design...
This paper discusses a new approach to the development life-cycle of agent-based production control applications, from the design to the operation, based in a catalogue of high-level Petri nets. The high-level Petri net-based approach facilitates the conception, definition and formal specification of an "encapsulation process" in industrial production systems. The catalogue includes elements...
A reported liability of the controller area network protocol is that it does not provide a clock synchronization service. Therefore, whenever a CAN-based distributed embedded system requires its nodes to have a common time base, clock synchronization has to be implemented by means of an external mechanism. In a previous work, we proposed a fault-tolerant and high-precision clock synchronization protocol...
The introduction of non-deterministic networks to the automation field leads to new questions in the analysis of the resulting systems often called networked control systems (NCS). To determine reaction times not only the cycle times of the controllers but also the network delays have to be taken into account. The problem further increases in reliability analysis. Here the failures of a variety of...
This paper describes formal modeling and verification of automation systems from the system engineering point of view. Reuse of model components is the key issue in order to bring the scientific modeling methodology into engineering practice. The reuse is achieved by the combination of modular modeling of automation systems with object-oriented description of models in UML style. This allows to benefit...
The acceptance of formal methods in industry is a challenging task mainly due to difficult learning process and the lack of the tools and methods helping control engineer to interpret the results of formal verification procedure. We model existing source code of the controller and controller related information (controller model) along with controlled object (plant model) and verify modeled system...
To properly deal with the increasing complexity of industrial distributed and agile manufacturing control systems, the use of methods and tools that support the designer in the definition, implementation and verification of intelligent logic control software is more and more necessary. Nowadays, many different software tools are available to face the rapid prototyping and closed loop simulation based...
The developer of logic control systems is faced with increasing complexity of the functions to be implemented and, at the same time, increasing demands on the reliability of the resulting software. To analyze the reliability of such complex systems formal methods can be applied. One area of the corresponding research is focused on the application of model checking techniques to Programmable Logic...
The behaviour verification of hybrid systems, for example for safety properties, is based on the computation of the reachable state space of a hybrid automaton modelling the system under study. In this paper we present a method for the computation of reachable set of uncertain hybrid affine systems. This method extends previous works which compute the reachable set of certain affine systems by abstracting...
Podaj zakres dat dla filtrowania wyświetlonych wyników. Możesz podać datę początkową, końcową lub obie daty. Daty możesz wpisać ręcznie lub wybrać za pomocą kalendarza.