严密系统设计——方法、趋势与挑战
作 译 者：Joseph Sifakis （约瑟夫·希发基思）
出 版 日 期：2023-12-01
书 代 号：TP467650
Ｉ Ｓ Ｂ Ｎ：9787121467653
编辑推荐：
1."图灵奖"得主、中美法欧六院院士发轫之作，思想与技术并重，智能变革时代不可不读。2.深入解析系统设计方法论，洞悉智能自主趋势，直面可信技术挑战。3.中国科学院院士、中国科学院软件研究所研究员、计算机科学国家重点实验室主任 林惠民作序，中国工程院院士、北京大学博雅讲席教授、鹏城实验室主任 高文推荐。4.什么是系统设计？如何实现“构造即正确”的系统设计？人工智能时代的系统设计面临哪些技术挑战？如何判断自主系统（比如自动驾驶系统）的智能水平？本书带你进入系统设计的奇妙世界！
-
配 套 资 源
本书资源
-
图 书 内 容
内容简介
本书提出了一种基于形式化模型的严密的系统设计方法，详细阐述了严密系统设计方法的基本原理，介绍了严密系统设计框架BIP（Behavior, Interaction, Priority）的建模语言、形式语义及其工具链。自主系统作为人工智能技术应用落地的重要形态，讨论了自主系统设计的趋势和挑战，阐述了一种集成模型驱动方法与数据驱动方法的思路，并提出了一种新的基于替换测试的智能测试方法，用以判断自主系统在完成多种不同类型任务方面的智能水平。图书详情
ISBN：9787121467653开 本：16(170*240)页 数：208字 数：151本书目录
目 录 第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展开前 言
序 非常荣幸向广大读者介绍《严密系统设计—方法、趋势与挑战》这本学术著作。世界著名计算机科学家、2007 年图灵奖获得者 Joseph Sifakis 教授主笔，并与其合作者王强副研究员、张继勇教授共同撰写完成了该著作。该著作旨在全面阐述自主计算系统设计的原理和方法，包括系统设计的基本概念、意义以及对该领域未来发展的展望。 近十多年来，随着深度学习的成功所引发的人工智能技术的迅猛发展，计算系统也出现了从“自动”到“自主”的发展趋势。“自主系统”与“自动系统”的关键差别在于，前者必须具备正确应对在系统设计和开发阶段所无法预知的外部环境的能力，这对系统设计提出了重大挑战。由于自主系统往往部署在安全性至关重要的场景，因此需要一种新的方法来确保系统设计过程的语义连贯性，以实现安全可靠性需求的可回溯、可解释。Joseph Sifakis 教授是国际上研究自主计算系统设计的先驱；在过去几年中，他提出了自主系统设计的一系列基本原理和方法，为这个新研究领域的形成和发展奠定了基础。作者在本书中对这些原理和方法进行了详尽、深入浅出的阐述。 本书主体内容包括 6 章，每章均围绕一个主题展开全面阐述。第 1 章介绍系统设计的基本概念，讨论传统的系统设计方法及其局限性。第 2 章解释系统设计中正确性的含义，以及确保正确性的复杂性根源及其带来的技术挑战。第 3 章重点阐述严密系统设计方法的基本原则及其应用，这是作者对过去数十年研究工作和成果的总结。第 4 章介绍基于 BIP(Behavior，Interaction，Priority)的系统设计框架，该框架是对严密系统设计方法的具体实践，本章不仅包括对 BIP 建模语言和相关工具的介绍，也给出了详细的案例分析，论述了该框架的有效性。第 5 章讨论自主系统设计的发展趋势，特别是以机器学习为代表的人工智能技术的广泛应用为系统设计带来的技术挑战，探讨了在自主系统设计中不同类型知识的生成及其作用，以及将数据驱动的人工智能技术与传统的模型驱动技术进行集成的方法。第 6 章讨论自主系统的智能测试，即如何判定系统的智能水平，展示了一种新的面向自主系统的智能测试方法，称为“替换测试”。另外，针对自主系统的高度复杂性，书中也讨论了在理性的形式验证思想指导下基于仿真测试的经验验证。 本书不仅为计算机专业的学者、工程师和学生提供了全面且广泛的关于计算系统，特别是自主计算系统设计的理念、知识和方法，同时也为基于人工智能的一般计算系统的发展和应用，提供了深入细致的设计开发指导和宝贵的文献资源。 林惠民 中国科学院软件研究所 中国科学院院士 2023 年 11 月 21 日展开作者简介
约瑟夫·希发基思(Joseph Sifakis), 法国和希腊双重国籍，国际知名计算机科学家，2007 年“图灵奖”获得者，法国 Verimag 实验室创始人兼荣誉主任，南方科技大学杰出访问教授；曾任法国国家科学研究中心研究总监、法国约瑟夫傅里叶大学研究员、瑞士洛桑联邦理工学院教授；2001 年获得法国国家科学研究中心银质奖章，2008 年当选法国工程院院士和欧洲科学院院士，2010 年当选法国科学院院士，2015 年当选美国人文和科学院院士，2017 年当选美国工程院外籍院士，2019 年当选中国科学院外籍院士。希发基思教授是模型检测以及嵌入式系统设计与验证等研究领域的先驱。他在国际上首次提出通过对时序逻辑公式的计值来验证并发系统性质的思想，得到一系列开创性理论成果，包括对含有“可能”和“必然”模态算子的分支时序逻辑的不动点刻画，以及首个面向带时间分支时序逻辑的符号模型检测算法和以该算法为基础的实时系统模型检测工具 Kronos。这些工作为模型检测研究领域的创立和发展奠定了理论基础。当前，模型检测已成为分析、验证并发系统性质的最重要的技术，成功应用于计算机硬件、软件、通信协议、安全认证协议等领域。由于对模型检测理论和技术的开创性贡献，他荣获 2007 年国际计算机届最高奖“图灵奖”。希发基思教授曾担任欧盟“卓越网络”ARTIST 嵌入式系统研究联盟的科学协调人，负责协调欧洲 35 个实时与混成系统领域研究小组的工作。在此期间，他极力推动欧盟与中国在该领域的合作。在他领导下，该研究联盟从 2006 年至 2011 年在中国举办了 6 届嵌入式系统设计讲习班，使用欧盟经费，邀请国际上嵌入式系统领域的知名专家为国内研究生和青年学者讲课，极大促进了中国在该领域的人才培养和学科发展。 王强博士中国人民解放军军事科学院副研究员，本科及硕士毕业于国防科技大学，博士师从Joseph Sifakis 教授，毕业于瑞士洛桑联邦理工学院，承担国家及省部级项目多项，发表学术论文 20 余篇，主要从事安全关键系统形式化建模与验证、基于模型的系统设计方法等领域研究。张继勇博士杭州电子科技大学特聘教授，国家级人才专家，先后在清华大学获得计算机科学专业学士和硕士学位，博士毕业于瑞士洛桑联邦理工学院，长期从事云计算、机器学习、数据科学和推荐系统等领域研究。 -
样 章 试 读
-
图 书 评 价 我要评论
