作品简介
本书提出了一种基于形式化模型的严密的系统设计方法，详细阐述了严密系统设计方法的基本原理，介绍了严密系统设计框架BIP（Behavior，Interaction，Priority）的建模语言、形式语义及其工具链。自主系统作为人工智能技术应用落地的重要形态，讨论了自主系统设计的趋势和挑战，阐述了一种集成模型驱动方法与数据驱动方法的思路，并提出了一种新的基于替换测试的智能测试方法，用以判断自主系统在完成多种不同类型任务方面的智能水平。
约瑟夫·希发基思（Joseph Sifakis），法国和希腊双重国籍，国际知名计算机科学家，2007年“图灵奖”获得者，法国Verimag实验室创始人兼荣誉主任，南方科技大学杰出访问教授；曾任法国国家科学研究中心研究总监、法国约瑟夫傅里叶大学研究员、瑞士洛桑联邦理工学院教授；2001年获得法国国家科学研究中心银质奖章，2008年当选法国工程院院士和欧洲科学院院士，2010年当选法国科学院院士，2015年当选美国人文和科学院院士，2017年当选美国工程院外籍院士，2019年当选中国科学院外籍院士。
希发基思教授是模型检测以及嵌入式系统设计与验证等研究领域的先驱。他在国际上首次提出通过对时序逻辑公式的计值来验证并发系统性质的思想，得到一系列开创性理论成果，包括对含有“可能”和“必然”模态算子的分支时序逻辑的不动点刻画，以及首个面向带时间分支时序逻辑的符号模型检测算法和以该算法为基础的实时系统模型检测工具Kronos。这些工作为模型检测研究领域的创立和发展奠定了理论基础。当前，模型检测已成为分析、验证并发系统性质的最重要的技术，成功应用于计算机硬件、软件、通信协议、安全认证协议等领域。由于对模型检测理论和技术的开创性贡献，他荣获2007年国际计算机届最高奖“图灵奖”。
希发基思教授曾担任欧盟“卓越网络”ARTIST嵌入式系统研究联盟的科学协调人，负责协调欧洲35个实时与混成系统领域研究小组的工作。在此期间，他极力推动欧盟与中国在该领域的合作。在他领导下，该研究联盟从2006年至2011年在中国举办了6届嵌入式系统设计讲习班，使用欧盟经费，邀请国际上嵌入式系统领域的知名专家为国内研究生和青年学者讲课，极大促进了中国在该领域的人才培养和学科发展。
王强博士，中国人民解放军军事科学院副研究员，本科及硕士毕业于国防科技大学，博士师从Joseph Sifakis教授，毕业于瑞士洛桑联邦理工学院，承担国家及省部级项目多项，发表学术论文20余篇，主要从事安全关键系统形式化建模与验证、基于模型的系统设计方法等领域研究。
张继勇博士，杭州电子科技大学特聘教授，国家级人才专家，先后在清华大学获得计算机科学专业学士和硕士学位，博士毕业于瑞士洛桑联邦理工学院，长期从事云计算、机器学习、数据科学和推荐系统等领域研究。