大规模计算机软件和系统的状态机
摘要：大规模计算机软件和硬件行为、架构和抽象属性的技术的介绍纯粹基于普通确定性有限状态机。目标是能够处理从操作系统到数据库和实时控制的规范。带有输出的状态机被表示为从有限事件序列到输出的映射，使得f(s)是在从初始状态经过s到达的状态中的输出。复合序列映射对应于状态机乘积。这里使用的方法可以指定或约束系统行为和系统设计。所介绍的激励性示例范围从简单计数器到分布式一致性算法和实时电路。该方法旨在方便地描述设备和软件的“信封背面”，同时允许对行为和架构进行详细的分层规范。数学方法基于序列的原始递归和反馈有限状态机的自动机产品，适应于Moore类型的状态机。不采用任何形式方法或其他元数学技术，尽管并行和并发的复合系统易于指定，但并不需要将任何特定的通信方案作为原始方案。状态机不被增强或扩展-即使是最复杂的复合系统也被普通确定性有限状态机建模，这与半群的丰富数学理论有关。
作者：Victor Yodaiken
论文ID：1512.06788
分类：Formal Languages and Automata Theory
分类简称：cs.FL
提交时间：2023-06-22