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.