Decomposing Digital-System Specifications into Interacting Sequential Processes

Johnson这项研究是在开发正式的技术，将更高级别的系统规范分解为相互作用的顺序过程。函数代数用于定义形式化表示并构建一组用于操作它们的转换。“交互方案”的概念是中心主题。该项目由四个活动组成：1。数字系统分解的理论研究特别是控制同步和数据通信协议的形式化推导；2. 正确进行顺序分解的形式转换的自动化；3. 将机械化形式化系统与可用的CAD工具和其他推理系统集成；和4。设计系统在数字系统设计实例中的应用。

Johnson This research is on developing formal techniques to decompose higher-level system specifications into interacting sequential processes. A functional algebra is used for defining formal representations and building a set of transformations for manipulating them. The notion of "interaction schemes" is the central subject. The project is composed of four activities: 1. theoretical studies of the decomposition of digital systems; especially formal derivation of control-synchronization and data- communication protocols; 2. automation of formal transformations which correctly do sequential decompositions; 3. integration of the mechanized formal system with available CAD tools, and other reasoning systems; and 4. application of the design system to meaningful examples of digital-system designs.