序

非常荣幸向广大读者介绍《严密系统设计——方法、趋势与挑战》这本学术著作。世界著名计算机科学家、2007年图灵奖获得者Joseph Sifakis教授主笔，并与其合作者王强副研究员、张继勇教授共同撰写完成了该著作。该著作旨在全面阐述自主计算系统设计的原理和方法，包括系统设计的基本概念、意义以及对该领域未来发展的展望。

近十多年来，随着深度学习的成功所引发的人工智能技术的迅猛发展，计算系统也出现了从“自动”到“自主”的发展趋势。“自主系统”与“自动系统”的关键差别在于，前者必须具备正确应对在系统设计和开发阶段所无法预知的外部环境的能力，这对系统设计提出了重大挑战。由于自主系统往往部署在安全性至关重要的场景，因此需要一种新的方法来确保系统设计过程的语义连贯性，以实现安全可靠性需求的可回溯、可解释。Joseph Sifakis教授是国际上研究自主计算系统设计的先驱；在过去几年中，他提出了自主系统设计的一系列基本原理和方法，为这个新研究领域的形成和发展奠定了基础。作者在本书中对这些原理和方法进行了详尽、深入浅出的阐述。

本书主体内容包括6章，每章均围绕一个主题展开全面阐述。第1章介绍系统设计的基本概念，讨论传统的系统设计方法及其局限性。第2章解释系统设计中正确性的含义，以及确保正确性的复杂性根源及其带来的技术挑战。第3章重点阐述严密系统设计方法的基本原则及其应用，这是作者对过去数十年研究工作和成果的总结。第4章介绍基于 BIP（Behavior，Interaction，Priority） 的系统设计框架，该框架是对严密系统设计方法的具体实践，本章不仅包括对BIP建模语言和相关工具的介绍，也给出了详细的案例分析，论述了该框架的有效性。第5章讨论自主系统设计的发展趋势，特别是以机器学习为代表的人工智能技术的广泛应用为系统设计带来的技术挑战，探讨了在自主系统设计中不同类型知识的生成及其作用，以及将数据驱动的人工智能技术与传统的模型驱动技术进行集成的方法。第6章讨论自主系统的智能测试，即如何判定系统的智能水平，展示了一种新的面向自主系统的智能测试方法，称为“替换测试”。另外，针对自主系统的高度复杂性，书中也讨论了在理性的形式验证思想指导下基于仿真测试的经验验证。

本书不仅为计算机专业的学者、工程师和学生提供了全面且广泛的关于计算系统，特别是自主计算系统设计的理念、知识和方法，同时也为基于人工智能的一般计算系统的发展和应用，提供了深入细致的设计开发指导和宝贵的文献资源。

中国科学院软件研究所
中国科学院院士
2023年11月21日