Projects

Security verification and reconfiguration of DES

This area of research has currently three ramifications. The first one is related to the application to manufacturing systems.

Manufacturing systems may be subject to external attacks and failures, so it is important to deal with the detection of the attack and recoverability of the system after these situations.

One of the problems that may occur after an attack is the desynchronization of the control structure, called supervisor, with the physical plant. Such desynchronization may be seen as plant and supervisor being in uncorresponding states. The possibility of leading the system to a known state, recovering control, is of extreme importance to the safety of industrial processes. The main idea of this research is to use concepts of synchronizing automata to find synchronizing word, that regardless the state of each one of the subsystems (plant and supervisor), brings the system and supervisor back to a known state.

The second ramification is related to the detection of the attacks in computational systems and the third ramification is related to the design of fault tolerant control for autonomous vehicles under attacks in the communication.

Related works:

• PhD in progress (JAIME ARTURO DULCE-GALINDO)
• PhD in progress (MICHEL RODRIGO DAS CHAGAS ALVES)
• Aplicação de Autômatos Sincronizáveis na Segurança de Sistemas a Eventos Discretos (PhD Thesis of LUCAS VINÍCIUS RIBEIRO ALVES)

UltraDES

UltraDES is an object oriented library composed of data structures and algorithms for the modeling, analysis and control of discrete event systems (DES). The library was developed in C# language and is based on the .NET Framework.

UltraDES can be used in any programming language and platform that supports .NET Standard 2.0, even in mobile environments, like in Android and IOS apps.

The library has several algorithms implemented, most of then used in the Supervisory Control Theory, but also some algorithms and data structures for graphs and petri nets.

Related works:

• Desenvolvimento de uma Biblioteca para Sistemas a Eventos Discretos para Plataforma .NET (Undergraduate final project of LUCAS VINÍCIUS RIBEIRO ALVES)
• Aprimoramento das Estruturas de Dados do UltraDES – Uma Biblioteca para Modelagem, Análise e Controle de Sistemas a Eventos Discretos (Undergraduate final project of LUCAS RANGEL RODRIGUES MARTINS)
• Desenvolvimento de uma Ferramenta para a Geração de Gráficos de Autômatos Utilizando a Plataforma .NET (Undergraduate final project of NELSON FILIPE ARAUJO DIAS)
• Desenvolvimento da Biblioteca clDES: Algoritmos Paralelos para Sistemas a Eventos Discretos em Plataformas Heterogêneas (Undergraduate final project of ADRIANO DE ARAÚJO ABREU MOURÃO)

Task scheduling in Manufacturing Systems using the Supervisory Control of Discrete Event Systems

We develop an approach for the problem of optimal task scheduling in flexible manufacturing systems as a combination of metaheuristic optimization techniques with the supervisory control theory of discrete-event systems.

One of the great problems in optimization is to model the restrictions of the system. The closed loop behavior of the system under the Supervisory Control Theory is used as the search universe for the optimization problem. The optimization algorithm performs the search for the optimal schedules, while the supervisory control has the role of codifying all the problem constraints, allowing an efficient feasibility correction procedure, and avoiding schedules that are sensitive to uncertainties in the execution times associated with the plant operation.

Typically, we deal with makespan, that is the duration of the production of a batch of products. There are a few different directions taken using the same idea.

SCT to model the search universe for classical optimization algorithms

With the search space delimited by the Supervisory Control Solution, we have worked with different evolutionary computation algorithms, such as VNS with a 2-opt local search, Clonal Selection Algorithm, Ant Colony, Tabu Search, among known algorithms from the literature.

Related works:

• Solution of a Scheduling Problem using an Abstraction of the Closed Loop Behavior of a Discrete Event System (Master’s Dissertation of Gustavo Caetano Rafael)
• Método para Sequenciamento de Tarefas em Sistemas Flexíveis de Manufatura baseado em Metaheurísticas e Controle Supervisório (PhD Thesis of Tatiana Alves Costa)
• Escalonamento Ótimo de um Sistema Flexível de Manufatura com Controle Supervisório (Master’s Dissertation of Regiane de Sousa e Silva)

Maximization of the Parallelism

In this ramification, we also use as the search space to a planning problem, the closed loop behavior of a system under the Supervisory Control Theory. Aiming to minimize makespan, we propose another metric that allows to turn the problem into a path finding problem. This metric relates to the number of devices working in parallel, by adding the information of the number of active tasks in each state of an automaton. States where the machine is idle have 0 active tasks and the states where the machine is working have a nonzero number of active tasks. Algorithms were developed in order to find sequences with high parallelism, that is a suboptimal solution to the problem of minimizing makespan. Three heuristics were developed under the same paradigm.

Logical Parallelism Maximization
Heuristic Makespan Minimization
Paralelism Maximization with Time Restrictions

Related works:

• Planejamento da Produção em Sistemas a Eventos Discretos – Análise Lógica e Temporal (Master’s Dissertation of LUCAS VINÍCIUS RIBEIRO ALVES)

Factorization

This approach starts from the closed-loop behavior and searches for a production route that minimizes makespan. It uses a divide-and-conquer strategy that allows to decompose the domain into a concatenation of smaller languages, then optimize each of them separately, and finally, concatenate all the partial solutions to get the optimal production route. The decomposition depends on the existence of states with a specific characteristic, the idle states. When they are The proposed method is implemented in an exact algorithm and its performance is tested on a set of benchmark examples.

Related works:

• PhD in progress (HUGO JERZY BRAVO CIPRIANO)

Formal Verification

In this ramification, we study the use of model checking to solve the problem of optimal task scheduling in a flexible manufacturing system. The system is modelled as a discrete event system, and first the least restrictive safe behaviour is synthesised according to supervisory control theory. Timing constraints are added to the model in the form of extended finite-state machines, and time-optimal schedules are computed using the discrete event systems and model checking tool Supremica. Preliminary work was done with the tool Uppaal.

Related works:

• Aplicação da Ferramenta de Verificação Formal UPPAAL na Obtenção de Planos de Produção para Sistemas de Manufatura Modelados como Sistemas a Eventos Discretos (Undergraduate final project of ROGGER LACERDA GONTIJO)
• MALIK, R. ; PENA, P.N. . Optimal Task Scheduling in a Flexible Manufacturing System using Model Checking. In: 14th International Workshop on Discrete Event Systems, 2018, Sorrento Coast, Itália. Preprints of the 14th International Workshop on Discrete Event Systems, 2018. v. x. p. 241-246.

Applications

• Estudo do Desempenho do Cluster Tool – Abordagem Baseada na Teoria de Controle Supervisório (Master’s Dissertation of MÁRCIO JÚNIOR NUNES)
• Tradução Automática de Problemas de Escalonamento Job Shop Flexível com Bloqueio para Autômatos Utilizando a Teoria de Controle Supervisório (Master’s Dissertation of DANIEL SARSUR CÂMARA)
• Sequenciamento de Movimentos Utilizando Sistemas a Eventos Discretos para uma Tarefa com Interface Homem-Máquina (Undergraduate final project of ANA CHRISTINE DE OLIVEIRA)
• Análise do Processo de Roteamento de Minério Baseada na Teoria de Controle Supervisório (Undergraduate final project of TASSIO ABREU DE SOUZA)
• Análise das Linhas de Produção de Peças da Carroceria de um Automóvel atráves da Teoria de Controle Supervisório (Undergraduate final project of GUILHERME HENRIQUE FERREIRA SALES)

Abstractions to overcome complexity issues in DES

The closed-loop behavior of a system under the Supervisory Control Theory (SCT) guarantees nonblockingness and safety requirements while implementing the minimally restrictive behavior. Such feature causes the SCT to suffer with the “curse of dimensionality” when systems become bigger and more complex.

The use of abstraction for task scheduling

The closed-loop behavior of a system under the Supervisory Control Theory (SCT) guarantees nonblockingness and safety requirements and, thus, it can be used as the search universe for a planning problem. Abstractions obtained through natural projection with the observer property applied to the closed-loop behavior are used instead, as the search universe for a planning problem. We develop conditions that such abstractions may have. This process leads to a reduction of the search space.

Heuristics to do the search over the abstractions are also developed.

Related works:

• Abstração do Supervisor para a Aplicação na Solução de Problemas de Planejamento (Master’s Dissertation of JULIANA NOGUEIRA VILELA)
• Solution of a Scheduling Problem Using an Abstraction of the Closed Loop Behaviour of a Discrete Event System (Master’s Dissertation of GUSTAVO CAETANO RAFAEL)
• Abstrações de Supervisores Localmente Modulares para Aplicação na Solução de Problemas de Planejamento (Master’s Dissertation of MICHEL RODRIGO DAS CHAGAS ALVES)
• Abstração do Supervisor para Sistemas com Retrabalho Visando a Solução de um Problema de Planejamento (Master’s Dissertation of FRANKLIN M. GARCIA-ACEVEDO)

The use of abstractions for the nonconflict test

This work proposed an efficient test that uses abstractions to detect conflict in composed systems controlled by local supervisors. This test, called nonconflict test, is not applied over the languages generated by the supervisors, but over abstractions of the supervisors with some specific characteristics, related to the observe property and the sets of events kept by the projection.

Related works:

• Verificação de Conflito na Supervisão de Sistemas Concorrentes usando Abstrações (PhD Thesis of PATRÍCIA NASCIMENTO PENA)

Verification of the observer property

The observer property is an important condition to be satisfied by abstractions of Discrete Event System (DES) models. We developed a test to find out if an abstraction of a DES obtained through natural projection has the observer property. The procedure, called OP-Verifier, can be applied to (potentially nondeterministic) automata, with quadratic complexity in the number of states.

Also, we developed an algorithm to extends the set of events kept by the projection in order to attain the observer property.

Related works:

• Verificação de Conflito na Supervisão de Sistemas Concorrentes usando Abstrações (PATRÍCIA NASCIMENTO PENA)
• Verificação e Busca da Propriedade do Observador em Sistemas a Eventos Discretos (HUGO JERZY BRAVO CIPRIANO)