Complexity and Implementation for Discrete-Event Systems

离散事件系统(DES)将系统的行为建模为自动机，并使用自动机来正式验证属性，如可控性(系统是否会保持在所需的行为范围内)和非阻塞(死锁检测的一种形式)。应用领域包括制造、通信和运输系统，以及汽车应用。*该项目的长期目标是促进行业对离散事件系统的采用。在这份提案中，我们将关注的短期目标是1)简化监管器的实施和2)设计，以及3)提高可扩展性。*简化实施的短期目标将通过建立王的采样数据(SD)监督控制工作来解决。该方法解决了将定时DES(TDES)监控程序转换为摩尔有限状态机(FSM)实现所涉及的多个并发性和计时问题。要实现此转换，必须满足许多SD属性，其中许多属性可能不容易手动解决，也不能仅基于安全和死锁问题进行指定。为了使翻译的所有步骤变得容易和自动化，我们将开发一种综合方法和离散优化方法，以解决任何剩余的控制决策。这将提供一个关键的缺失步骤，不仅将提供更高质量的结果，还将从设计中消除一个困难和耗时的过程。*简化监控器设计的短期目标将通过创建一种方法来实现，该方法允许设计人员将控制器直接指定为摩尔有限状态机(FSM)，然后自动将FSM(工程师常用的设计格式)转换为等效的监控器以进行验证。由于采用正式方法的一个主要障碍是缺乏受过该领域培训的用户，这将使非专家更容易使用这种方法。*提高可扩展性的短期目标将主要通过利用Leduc基于分层界面的分层监督控制(HISC)方法来解决。该项目将从将Timed DES扩展到HISC开始。这将允许TDES应用于更大的系统，使该方法更适用于工业，并为将采样数据方法扩展到HISC奠定了基础。*我们还将研究提高故障诊断的可扩展性和容错管理程序。之所以选择这些主题，是因为行业对检测和处理故障的能力非常感兴趣，因此提高它们可以处理的系统的大小是非常可取的。对于故障诊断，将开发一种手动设计诊断器的方法(与当前基于综合的方法相反)，该方法应允许显著降低算法复杂性。在容错方面，我们将采用Leduc的方法来利用HISC基础设施。

Discrete-Event Systems (DES) model a system's behaviour as automata, and use this to formally verify properties such as controllability (will the system stay within desired behaviour) and nonblocking (a form of deadlock detection). Application areas include manufacturing, communication, and transport systems, as well as automotive applications. ******The long-term goal of this project is to improve the adoption of Discrete-Event Systems by industry. The short-term objectives we will focus on in this proposal are 1) simplifying supervisor implementation and 2) design, and 3) improving scalability.******The short-term objective of simplifying implementation will be addressed by building upon the Sampled-Data (SD) supervisory control work of Wang. This method addresses a number of concurrency and timing issues involved in converting a Timed DES (TDES) supervisor into an implementation as a Moore Finite State Machine (FSM). To make this translation possible, a number of SD properties must be satisfied, many of which may not be easy to address by hand, nor specified based solely on safety and deadlock concerns. To make all steps of the translation easy and automatic, we will develop a synthesis method and a discrete optimization approach that will resolve any remaining control decisions. This will provide a key missing step that will not only provide a higher quality result, but remove a difficult and time consuming process from the design. ******The short-term objective of simplifying supervisor design will be addressed by creating a method to allow the designer to specify controllers directly as Moore finite state machine (FSM), and then automatically convert the FSM (a common design format for engineers) into equivalent supervisors for verification. As a major barrier to the adoption of formal methods is the lack of users trained in the area, this should make this approach much more accessible to non-experts.******The short-term objective of improving scalability will be primarily addressed by leveraging the Hierarchical Interface-based Hierarchical Supervisory Control (HISC) approach of Leduc. This project will start with extending timed DES to HISC. This will allow TDES to be applied to much larger systems, making the method more useful to industry, and lay the foundation for extending the sampled-data method to HISC as well. ******We will also investigate improving the scalability of fault diagnosis and the fault-tolerant supervisors. These topics were chosen as the ability to detect and handle faults is of wide interest to industry, so improving the size of systems they can handle is highly desirable. For fault diagnosis, a method to manually design diagnosers (as opposed to the current synthesis-based approach) will be developed that should allow for significant reduction in algorithm complexity. For fault-tolerance, we will adapt the approach of Leduc to make use of the HISC infrastructure.