Extending the hierarchical interface-based supervisory control platform

提出的研究调查使用离散事件系统（DES）作为软件设计，规范和综合工具。这种方法的优点是，它提供了系统行为的直观图形表示，以及可立即用于验证和综合的精确形式化描述。然后可以将自动机用于目标软件语言的代码生成。该研究将针对该方法的三个主要障碍：1)能够处理工业强度问题的设计、验证和合成方法；2)为DES监督者提供可靠的实时实现方法；3)实现算法的图形软件工具，允许用户设计、验证、合成和模拟基于DES的系统，并根据结果自动生成代码。申请人博士论文中基于层次界面的监督控制（HISC）方法将作为基础。这种方法在组件之间开发定义良好的接口，以提供允许本地检查以保证全局属性（如可控性或非阻塞性）的结构。此外，干净接口的开发促进了组件子系统的并行开发和重用。这种方法将得到扩展，变得更加灵活和可扩展。下一步将是将定时DES、DES故障诊断和离散优化方法应用到新框架中。然后将根据申请人的硕士论文开发使用该框架的实施方法。此外，DES结果将扩展到更一般和更复杂的软件验证方法，如模型检查和使用定理证明器验证的基于谓词逻辑的描述。这将使这些方法能够更好地扩展。最后，将开发一个软件工具来实现上述理论。为了鼓励其他学者使用、测试和贡献软件，软件工具将被开发为开源。

The proposed research  investigates the use of discrete-event systems (DES) as a software design, specification and synthesis tool. The advantages of this approach is that it provides an intuitive graphical representation  of the systems behaviour as well as a precise formal description immediately usable for verification and synthesis. The automata can then be used for code generation for the target software language.    The research will target  three of the main obstacles to this approach: 1) a design, verification, and synthesis method capable of handling industrial strength problems,  2) a reliable real-time implementation method for DES supervisors, and  3) a graphical software tool to implement the algorithms and allow users to design, verify, synthesize, and  simulate DES based systems, and automatically generate code based on the results.      The hierarchical interface-based supervisory control (HISC) method from the applicant's doctoral thesis will be used as a foundation. This approach develops well defined interfaces between components to provide the structure to allow local checks to guarantee global properties such as controllability  or nonblocking. Additionally, the development of clean interfaces facilitates parallel development and re-use of the component subsystems.  This approach will be extended to be more flexible and scalable. The next step will be to adapt timed DES, DES fault diagnosis, and a discrete optimization method to the new framework. An implementation method that uses the framework will then be developed, based upon the applicant's masters thesis.    In addition, the DES results will be extended to more general and complex software verification approaches such as model checking and predicate logic based descriptions verified using theorem provers. This should enable these approaches to scale significantly better.    Finally, a software tool will be developed to implement the above theory. The software tool will be developed open source in order to encourage other academics to use, test, and contribute to the software.