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.