Research Initiation Award: Verification and Analysis of Operating Systems and Computer Architectures Using Moore Machines

这项研究跨越了目前被认为相距甚远的计算机工程的两个领域。本研究主要针对操作系统、计算机体系结构和数字电路的设计与实现问题。该研究基于摩尔机（有输出的状态机）的代数理论。在先前的工作中，开发了一种用于定义、组合和推理非常大规模摩尔机及其产品的新方法。该研究使用这种方法来分析和验证（或取消）一些有趣的系统和设计原则-包括总线协议，容错和调度机制，以及异步电路设计规则。研究目标是：澄清对实例的理解。澄清或发展可靠系统的设计原则，并研究实时敏感和并发状态转换系统的基本数学性质。

This research spans two areas of computer engineering that are currently considered quite far apart. The research is aimed at problems in the design and implementation of operating systems, computer architecture and digital circuits. And the research is based on the algebraic theory of Moore machines (state machines with output). A new method for defining, composing, and reasoning about very large-scale Moore machines and their products was developed in prior work. The research uses this method to analyze and validate (or invalidate) some interesting systems and design principles - including bus protocols, fault tolerance and scheduling mechanisms, and asynchronous circuit design rules. The research goals are to: clarify understanding of the examples. Clarify or develop design principles for reliable systems, and investigate the basic mathematical properties of real-time sensitive and concurrent state transition systems.