Discrete Event Systems

Applications

Dear Colleagues, you are all welcome to contribute additional applications of DES (either applications developed by you, your group, or applications you would like to recommend) to our page. To contribute, you can just send the following information to: [email protected]

  1. The application domain or name
  2. Links of detailed descriptions, e.g., published papers or project websites
  3. A short description paragraph would be very useful but is not required.

Applications of DES

1. Gadara Project: Control of Execution of Multithreaded Software for Deadlock Avoidance

Application of discrete control techniques to online control of execution of multithreaded software for deadlock avoidance, by use of an enhanced lock scheduler. This lock scheduler is synthesized using algorithmic techniques based on avoidance of "bad" siphons in the Petri net model of the underlying multithreaded program being executed. The Petri net model is built at program compile time. Some manual model tuning may be necessary, but after that, the synthesis of the controller is fully automated. The controller is then embedded into the program source code and it will be automatically invoked at execution time, whenever necessary to guarantee deadlock-free execution of all program threads.

References:

2. Management and Resource Planning of Intermodal Freight Transport Terminals using Petri Nets

In the context of smart and sustainable freight transportation, the use of intermodality is strongly supported and promoted by the European Union, which identifies in such technique a way to reduce emissions and dependency from oil. In particular, the European Union encourages member states in proposing and realizing innovative solutions to improve and advance such transportation systems.

Intermodal Freight Transport Terminals (IFTTs) are the nodes of the transportation chain in which the transfer between modes takes place. Therefore, it is necessary to efficiently manage these areas, so as to guarantee an efficient interface service between freight forwarders and hauliers and ensure a high competitiveness of the whole intermodal chain.

The D&CLab (Polytechnic of Bari) and AUTOlab (University of Cagliari) research groups are now cooperating for the enhancement of IFTTs. More in detail, thanks to the intrinsic discrete dynamics of IFTTs, the Petri net formalism was proposed to evaluate the performance, to plan resources, and to manage at strategical level the intermodal terminals. Stochastic Timed Petri Nets (STPNs) and First Order Hybrid Petri Nets (FOHPNs) were used to modularly model, simulate, analyze, and control IFTTs. The techniques were tested on a real case study, i.e., an intermodal terminal located in southern Italy, and demonstrated their efficiency in representing the dynamics of such complex systems, allowing the identification of criticalities and the implementation of a support tool for the decision makers of the terminal.

References:

3. Reconfigurable Hardware architectures based on FPGA

This work features an application of discrete controller synthesis (DCS) techniques to a class of dynamically reconfigurable embedded computing systems and contributes to the general approach of control for feedback computing. We propose a general model for applications defined as data-flow graphs of computing tasks, and target execution architectures that are dynamically partially reconfigurable Field Programmable Gate Arrays (FPGAs). We define our model in terms of parallel automata. Then, we encode relevant scheduling and control requirements in terms of a DCS problem w.r.t. multiple constraints and objectives. We take into account the system reconfiguration overhead, and the resulting controller is able to make decisions by foreseeing their impact on future requests. We validate our approach by using the BZR programming language (http://bzr.inria.fr/) for modeling and simulations, with a video processing system implementation on a specific FPGA platform. A new ongoing project on more advanced topics is considering embedded hardware for UAV drones: http://hpec.fr/

References:

4. Cloud Computing Infrastructures

The ever-growing complexity of software systems, as evidenced typically by Cloud computing, has led to the emergence of automated solutions for their management, called Autonomic Management Systems (AMS). They are designed as a composition of several managers, which are evaluating the dynamics of the system under management through measurements (e.g., workload, memory usage), taking decisions, and acting upon it so that it stays in a set of acceptable operating states. However, a careless combination of managers may lead to inconsistencies in the taken decisions, and classical approaches dealing with these coordination problems often rely on intricate and ad hoc solutions. To tackle this problem, we take a global view and underscore that AMSs are intrinsically reactive, as they react to flows of monitoring data by emitting flows of reconfiguration actions. Therefore we propose a new approach for the design of AMSs, based on synchronous programming and discrete controller synthesis techniques, using the BZR programming language (http://bzr.inria.fr/). They provide us with high-level languages for the specification of the system to manage, as well as means for statically guaranteeing the absence of logical coordination problems. Hence, they suit our main contribution, which is to obtain guarantees at design time about the absence of logical inconsistencies in the taken decisions. We detail our approach, illustrate it by designing an AMS for a realistic multi-tier application, and evaluate its practicality with an implementation This work was partially supported by the Ctrl-Green project on Autonomic energy management for virtualized datacenter: http://www.en.ctrlgreen.org/

References:

5. Software Components and Their Reconfiguration

Architecting in the context of variability has become a real need in today's software development. Modern software systems and their architecture must adapt dynamically to events coming from the environment (e.g., workload requested by users, changes in functionality) and the execution platform (e.g., resource availability). Software Component-based architectures have shown to be very suited for self-adaptation especially with their dynamical reconfiguration capabilities. However, existing solutions for reconfiguration often rely on low-level, imperative, and nonformal languages. This work proposes Ctrl-F, a domain-specific language whose objective is to provide high-level support for describing adaptation behaviors and policies in component-based architectures. It relies on reactive programming for formal verification and control of reconfigurations, using the BZR programming language. We integrate Ctrl-F with the FraSCAti Service Component Architecture middleware platform and apply it to the Znn.com self-adaptive case study. On a related topic, we worked on an adaption of a classical theory of supervisory control for synthesizing a controller, for controlling the behavior of a Software Components system modeled using graph transition systems. This theory is used to synthesize a controller that can impose both behavioral and structural constraints on the system during a reconfiguration.

References:

6. Fault Diagnosis of Fixed-Block Railway Signaling Systems

The use of railway transportation among different alternatives (e.g. road and air transportation) brings many profits such as less carbon dioxide emission and energy consumption. Railway signaling systems are mainly divided into two main groups such as fixed-block and moving-block. Independent of the signaling category, the vital component of railway systems that provide safe travel and transportation is the interlocking system (IS). Train operations in fixed-block signaling systems are realized by route reservation procedures. Railway lines are divided into fixed-length blocks (tracks) where each railway block has an entrance and an exit signal. These signals inform the train drivers about the occupation of the next railway block. Each railway block is permitted to be occupied by only one train at a time.

Fixed-block signaling systems consist of three main parts: The traffic command center (TCC), IS, and the field equipment. The IS works as an evaluation and decision-making mechanism between the TCC and the field equipment. Railway signaling systems are classified as safety-critical systems by the international safety standards due to the occurrence of faults that may result in a huge loss of life and property. Therefore, the design of the IS for fixed-block signaling systems is realized by considering the national and international safety standards.

The path to be followed in the design of the IS for the fixed-block signaling systems is defined by the V-model given in the IEC 61508-3 and the EN 50128 standards. At first, the requirements of the IS are determined in the V-model and the software is realized at the desired Safety Integrity Level (SIL) by using the recommended methods and architectures which are also defined in the safety standards. However, the design errors arise at the test phase while developing the safety-critical software according to the V-model. After the errors are detected, the designer passes to the modeling phase again and all software development processes are being initiated from the very beginning. When considering that the testing phase for a medium-scaled railway field takes 2-3 weeks, there arises a huge loss of time and workforce.

In this project, the proposed method allows the diagnosis of faults by using the obtained models in the software development process before passing to the test phase and permits the obtained models to be checked again. This project basically consists of four sections: 1. Determining the relations of possible routes and the field equipment for the chosen railway field (construction of the interlocking table), determining the traffic command center requirements (software, hardware and testing), determining the interlocking system requirements (software, hardware and testing) and determining the software requirements of the field, 2. Modeling the field equipment by using Petri net method which is also recommended by the safety standards, construction of the fault diagnosers of the field equipment and showing that the system is fault diagnosable. 3. Implementation of the Petri net models and the fault diagnosers on fail-safe PLCs, implementation of the traffic command center SCADA software on PC and implementation of the field software on fail-safe PLC, 4. Verification of the developed software by the software tests.

Diagnosability analysis for fixed-block signaling systems can be considered as an intermediate step between modeling the system and testing the developed software. Even though the design of the diagnoser can be seen as a time-consuming and stringent task for signaling system software developers but it determines whether the developed system models are diagnosable or not before testing the signaling system software. Another benefit of this intermediate step is to combine the theoretical and practical experience of signaling system engineers. In addition to the interlocking software, another software will be also realized for the TCC in this project. Additionally, another fail-safe PLC which is independent of the IS PLC will be provided to work as the real railway field. Thus, the application of a real fixed-block railway system design can be realized.

References:

7. Supervisory Control for Lock-Bridge Systems

In the coming decades, numerous navigation locks have to be renovated or replaced in the Netherlands. This project focuses on the model-based modular synthesis of supervisory control for lock-bridge systems, suitable for a product family of locks.

The complexity of the design, realization and maintenance of operation and control systems for civil infrastructures is increasing rapidly. Infrastructures are transformed from just civil systems to cyber-physical systems. Synthesis-based engineering is deployed to synthesize supervisory controllers for locks based on models of the plants and formal descriptions of the requirements. This research aims to find suitable non-monolithic supervisors such that several modules can be created each with its own supervisory controller. This increases the reuse of controllers for similar locks in the product family of locks and easy integration with nearby civil systems such as bridges.

The complete design method for the realization of supervisory controller implementations is taken into account. This includes all steps from requirement specification to real-time implementation. Special attention is paid to fault diagnosis, fault-tolerant control and automatic PLC code generation from the supervisory controller model.

References:

8. Teloco: Test of programmable logic controllers from IEC 60848 specifications

Teloco (TEst of LOgic COntrollers) is an academic tool that permits the generation of a conformance test sequence from an industrial specification in IEC 60848 language (GRAFCET). Technically, the specification model is first automatically translated, without semantics loss, into an equivalent Mealy machine. A minimum-length test sequence is then automatically generated from this machine. This sequence can afterward be used for the black-box conformance test of Programmable Logic Controllers (PLC) with cyclic I/O scanning. This tool has been developed in the frame of a project funded by the French Research Agency.

References:

9. Software Engineering: Concurrency Control and Service Composition

The correct-by-construction feature of supervisory control solutions is applied to two areas of software engineering: concurrency control and service composition.

In the development of code that incorporates concurrency control, we use the synthesis procedures of supervisory control theory to automate the process of determining where and when in software code to inject concurrency controls. Our work uses some limited-lookahead techniques to encompass the case of dynamic threads-- -where threads may be created and terminated at run time.

Our work on service composition develops a model of discrete-event systems based on labeled transition systems. The model can be used to represent services in a service-oriented architecture and the results create an orchestration of services to achieve given requirements.

Our work combines research in Model-Based Software Development (lab of J. Dingel) and Supervisory Control of Discrete-Event Systems (lab of K. Rudie).
 
References:

10. Logistics Specification and Analysis

We consider the domain of manufacturing systems. Due to competitive landscapes and dynamic customer expectations, manufacturing firms seek flexibility in product development. A dimension in which product development flexibility can be measured is concept flexibility; a concept flexible firm is able to anticipate the needs of the market, generate multiple concepts for those needs, and develop the design alternatives in parallel. Proper computer-aided design and engineering tools, combined with rapid prototyping technologies, can significantly improve concept flexibility. The Logistics Specification and Analysis Tool (LSAT) is a workbench for model-based system design and analysis. LSAT enables rapid design-space exploration of supervisory controllers that orchestrate the behavior of these systems. LSAT has the following combined functionality integrated:

Specification: A domain-specific language is used to model the system layout and behavior. The uncontrolled system is specified in terms of resources, peripherals, actions, motion profiles, and activities. The supervisory controller is specified as a network of finite-state automata, or as a sequence of activities that is (repeatedly) executed. This supervisory controller can be computed by supervisory controller synthesis (using the CIF tool).

Analysis: LSAT provides means to analyze the productivity characteristics of the system such as makespan or throughput. It can analyze the critical path and highlight bottlenecks in the system to show where performance can be gained.

Synthesis: A makespan or throughput optimal controller can be synthesized. Partial order reduction methods are used to efficiently come up with the result.
Visualization: The productivity of the system is shown graphically using Gantt charts. The system specification can also be done using graphical editors for motion profiles and activity specifications.

Validation: Using conformance checking, the implementation can be validated against the specification.

By having this functionality combined, engineers can efficiently compare different design concepts for a manufacturing system. The results from synthesis and analysis act in a feedback loop to improve the layout and behavior specification. The specification itself is a system blueprint, that can be used for communicating the design and act as a contract for system realization. The functioning of the tool has been demonstrated in the following case studies:

  • xCPS manufacturing system
  • Twilight manufacturing system
  • Lithography machine wafer logistics

References: