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.