Modeling, Interface Design, and Verification of Hybrid and Discrete Event Systems

ECS-9709796 Kumar 这个项目的动机是从一个全面的和正式的研究操作嵌入式航空电子软件系统，用于飞机系统的自动控制。 这样的自动控制系统是混合的，具有连续和离散状态。 将开发一种航空电子软件操作程序的摩尔机型形式表示法，并将其用于检查软件的一致性和完整性。 还将进行必要的扩展，以包括系统的混合特性。混合系统的性质验证是通过混合自动机表示的系统和规格。 我们提出了一个模块化和层次化的混合自动机建模框架的复杂混合系统。 接下来，通过扩展离散事件系统的优先同步理论，将发展这种混合系统的相互作用理论。这个理论将被用来设计多个相互作用的混合系统之间所需的接口逻辑。 最后，工具和算法的验证和综合的混合系统将在建议的框架，具体来说，我们建议开发一种方法，连续的分层验证和综合。

ECS-9709796 Kumar This project is motivated from a comprehensive and formal study of operationally embedded avionics software systems that are used in automated control of aircraft systems. Such automated control systems are hybrid-possessing both continuous and discrete states. A Moore machine type formal representation of the operational procedures of the avionics software will be developed and it will be used to check consistency and completeness of the software. Requisite extensions will be also made to include hybrid characteristics of the system. Verification of properties of hybrid systems is accomplished by hybrid automaton representation of the system and the specification. We propose to develop a modular and hierarchical hybrid automata modeling framework of complex hybrid systems. Next a theory of interaction of such hybrid systems will be developed by extending the theory of prioritized synchronization of discrete event systems. This theory will then be used to design the required interface logic between multiple interacting hybrid systems. Finally, tools and algorithms for the verification and synthesis of hybrid systems will be developed in the proposed framework, specifically we propose to develop a method of successive hierarchical verification and synthesis.