严密系统设计——方法、趋势与挑战

本书提出了一种基于形式化模型的严密的系统设计方法，详细阐述了严密系统设计方法的基本原理，介绍了严密系统设计框架BIP（Behavior, Interaction, Priority）的建模语言、形式语义及其工具链。自主系统作为人工智能技术应用落地的重要形态，讨论了自主系统设计的趋势和挑战，阐述了一种集成模型驱动方法与数据驱动方法的思路，并提出了一种新的基于替换测试的智能测试方法，用以判断自主系统在完成多种不同类型任务方面的智能水平。

约瑟夫·希发基思(Joseph Sifakis)

法国和希腊双重国籍，国际知名计算机科学家，2007 年“图灵奖”获得者，法国 Verimag 实验室创始人兼荣誉主任，南方科技大学杰出访问教授；曾任法国国家科学研究中心研究总监、法国约瑟夫傅里叶大学研究员、瑞士洛桑联邦理工学院教授；2001 年获得法国国家科学研究中心银质奖章，2008 年当选法国工程院院士和欧洲科学院院士，2010 年当选法国科学院院士，2015 年当选美国人文和科学院院士，2017 年当选美国工程院外籍院士，2019 年当选中国科学院外籍院士。

希发基思教授是模型检测以及嵌入式系统设计与验证等研究领域的先驱。他在国际上首次提出通过对时序逻辑公式的计值来验证并发系统性质的思想，得到一系列开创性理论成果，包括对含有“可能”和“必然”模态算子的分支时序逻辑的不动点刻画，以及首个面向带时间分支时序逻辑的符号模型检测算法和以该算法为基础的实时系统模型检测工具 Kronos。这些工作为模型检测研究领域的创立和发展奠定了理论基础。当前，模型检测已成为分析、验证并发系统性质的最重要的技术，成功应用于计算机硬件、软件、通信协议、安全认证协议等领域。由于对模型检测理论和技术的开创性贡献，他荣获 2007 年国际计算机届最高奖“图灵奖”。

希发基思教授曾担任欧盟“卓越网络”ARTIST 嵌入式系统研究联盟的科学协调人，负责协调欧洲 35 个实时与混成系统领域研究小组的工作。在此期间，他极力推动欧盟与中国在该领域的合作。在他领导下，该研究联盟从 2006 年至 2011 年在中国举办了 6 届嵌入式系统设计讲习班，使用欧盟经费，邀请国际上嵌入式系统领域的知名专家为国内研究生和青年学者讲课，极大促进了中国在该领域的人才培养和学科发展。

王强博士

中国人民解放军军事科学院副研究员，本科及硕士毕业于国防科技大学，博士师从Joseph Sifakis 教授，毕业于瑞士洛桑联邦理工学院，承担国家及省部级项目多项，发表学术论文 20 余篇，主要从事安全关键系统形式化建模与验证、基于模型的系统设计方法等领域研究。

张继勇博士

杭州电子科技大学特聘教授，国家级人才专家，先后在清华大学获得计算机科学专业学士和硕士学位，博士毕业于瑞士洛桑联邦理工学院，长期从事云计算、机器学习、数据科学和推荐系统等领域研究。

目 录
第1章 引言 1
1.1 系统设计的概念 2
1.2 系统的演变过程 6
1.3 传统的系统设计方法 12
1.3.1 “V-模型”方法的设计流程 13
1.3.2 “V-模型”方法的假设条件 17
1.4 本书组织结构 19
参考文献 21
第2章 系统设计的正确性和复杂性 23
2.1 正确性内涵 24
2.1.1 可信性 25
2.1.2 关键等级 31
2.2 复杂性挑战 36
2.2.1 设计复杂性 37
2.2.2 模型复杂性 39
参考文献 44
第3章 严密系统设计方法 46
3.1 基本思想 47
3.2 关注点分离 50
3.2.1 从需求到应用软件 52
3.2.2 从应用软件到软硬件融合系统 56
3.3 基于组件的设计 59
3.3.1 基本原则 59
3.3.2 组件框架 61
3.4 语义连贯的设计 65
3.5 “构造即正确”的设计 70
3.5.1 基本原理 70
3.5.2 水平正确性 73
3.5.3 垂直正确性 76
3.6 实践讨论 78
参考文献 81
第4章 基于 BIP 的系统设计框架 86
4.1 BIP框架介绍 87
4.2 BIP语言 92
4.2.1 原子组件 93
4.2.2 连接器 98
4.2.3 优先级 103
4.2.4 复合组件 104
4.3 BIP编译器与引擎 108
4.3.1 BIP操作语义 108
4.3.2 BIP编译器 111
4.3.3 BIP引擎 112
4.4 案例：Dala自主机器人 114
4.4.1 自主机器人功能需求建模 114
4.4.2 基于模型的代码生成 120
4.4.3 形式化验证 121
参考文献 123
第5章 自主系统的设计方法 126
5.1 自主系统的内涵 127
5.1.1 自主系统的功能架构 127
5.1.2 自主系统的目标管理 130
5.1.3 自主系统与自动化系统 133
5.1.4 自主系统的混合设计 137
5.2 自主系统的测试 139
5.2.1 测试的基本原理 141
5.2.2 基于仿真的测试 144
5.3 知识的生成与应用 147
5.3.1 知识的类型 148
5.3.2 知识的生成 150
5.4 自主系统的可信性评估 155
参考文献 160
第6章 自主系统的智能测试 164
6.1 智能的内涵 165
6.1.1 自主系统的视角 165
6.1.2 人类智能的视角 167
6.2 智能测试方法 170
6.2.1 替换测试的概念 171
6.2.2 通用测试框架 174
6.3 智能测试的适用性 179
参考文献 183
第7章 系统设计的挑战与展望 189
参考文献 195