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

研究启动奖：使用摩尔机验证和分析操作系统和计算机架构

• 批准号: 9409454
• 负责人: Victor Yodaiken
• 金额: $ 4.58万
• 依托单位: New Mexico Institute of Mining and Technology
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 1994
• 资助国家: 美国
• 起止时间: 1994-12-01 至 1998-05-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=9409454&HistoricalAwards=false
• 关键词: Research; Initiation; Award; Verification; Analysis

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.

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