Applications

Dear Colleagues, you are all welcomed to contribute more applications of DES (either applications developed by your our group or applications you would like to recommend) to our page. To contribute, you can just send the following information to: xiangyin@umich.edu

1. The application domain or name

2. Links of detailed descriptions, e.g., published papers or project websites

A short paragraph of description will be very useful but is not necessary.

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:

  1. http://gadara.eecs.umich.edu/

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:

  1. A Timed Petri Nets Model for Performance Evaluation of Intermodal Freight Transport Terminals

  2. Management of Intermodal Freight Terminals by First-Order Hybrid Petri Nets

  3. Resource planning of intermodal terminals using timed Petri nets

  4. Simulation and performance evaluation of an Intermodal terminal using Petri Nets

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:

  1. Discrete Control for Reconfigurable FPGA-based Embedded Systems

  2. Model-based synthesis of correct controllers for dynamically reconfigurable architectures

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 an 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, 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:

  1. Distributed Execution of Modular Discrete Controllers for Data Center Management

  2. Designing Autonomic Management Systems by using Reactive Control Techniques

5. Software Components and Their Reconfiguration

Architecting in the context of variability has become a real need in todays 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 non formal 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 (http://bzr.inria.fr/). 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:

  1. Behavioural Model-based Control for Autonomic Software Components

  2. A Domain-specific Language for The Control of Self-adaptive Component-based Architecture

  3. Supervisory Controller Synthesis for Safe Software Adaptation

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 which provides 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 are consists 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 may result with 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 arises 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 process is 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 (contruction 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 implementaion 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 the practical experience of signaling system engineers. In addition to the interlocking software, another software will be also realised for the TCC in this project. Additionally, another fail-safe PLC which is independent from the IS PLC will be provided to work as the real railway field. Thus, application of a real fixed-block railway system design can be realised

References:

  1. http://railway.pau.edu.tr/

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 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:

  1. https://www.tue.nl/en/university/departments/mechanical-engineering/research/research-groups/control-systems-technology/research/research-areas/systems-engineering/ongoing-phd-research-projects/supervisory-control-for-lock-bridge-systems/

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

Teloco (TEst of LOgic COntrollers) is an academic tool that permits to generate 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 afterwards be used for 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:

  1. http://webserv.lurpa.ens-cachan.fr/teloco