| 引用本文: | 王淑灵,詹博华,盛欢欢,吴昊,易士程,王令泰,金翔宇,薛白,李静辉,向霜晴,向展,毛碧飞.可信系统性质的分类和形式化研究综述.软件学报,2022,33(7):2367-2410 |
| |
|
| |
|
|
| 本文已被：浏览 3857次 下载 8169次 |
码上扫一扫！ |
|
|
| 可信系统性质的分类和形式化研究综述 |
|
王淑灵1,2, 詹博华1,2, 盛欢欢1,2, 吴昊1,2, 易士程1,2, 王令泰1,2, 金翔宇1,2, 薛白1,2, 李静辉3, 向霜晴3, 向展3, 毛碧飞3
|
|
1.计算机科学国家重点实验室(中国科学院 软件研究所), 北京 100190;2.中国科学院大学, 北京 100049;3.华为技术有限公司 可信理论研究室, 广东 深圳 518129
|
|
| 摘要: |
| 计算机系统被应用于各种重要领域,这些系统的失效可能会带来重大灾难.不同应用领域的系统对于可信性具有不同的要求,如何建立高质量的可信计算机系统,是这些领域共同面临的巨大挑战.近年来,具有严格数学基础的形式化方法已经被公认为开发高可靠软硬件系统的有效方法.目标是对形式化方法在不同系统的应用进行不同维度的分类,以更好地支撑可信软硬件系统的设计.首先从系统的特征出发,考虑6种系统特征:顺序系统、反应式系统、并发与通信系统、实时系统、概率随机系统以及混成系统.同时,这些系统又运行在众多应用场景,分别具有各自的需求.考虑4种应用场景:硬件系统、通信协议、信息流以及人工智能系统.对于以上的每个类别,介绍和总结其形式建模、性质描述以及验证方法与工具.这将允许形式化方法的使用者对不同的系统和应用场景,能够更准确地选择恰当的建模、验证技术与工具,帮助设计人员开发更加可靠的系统. |
| 关键词: 可信系统 形式化方法 性质分类 验证方法和工具 |
| DOI：10.13328/j.cnki.jos.006587 |
| 分类号: |
| 基金项目:国家自然科学基金(61972385,62032024,61836005) |
|
| Survey on Requirements Classification and Formalization of Trustworthy Systems |
|
WANG Shu-Ling1,2, ZHAN Bo-Hua1,2, SHENG Huan-Huan1,2, WU Hao1,2, YI Shi-Cheng1,2, WANG Ling-Tai1,2, JIN Xiang-Yu1,2, XUE Bai1,2, LI Jing-Hui3, XIANG Shuang-Qing3, XIANG Zhan3, MAO Bi-Fei3
|
|
1.State Key Laboratory of Computer Science (Institute of Software, Chinese Academy of Sciences), Beijing 100190, China;2.University of Chinese Academy of Sciences, Beijing 100049, China;3.Trustworthiness Theory Research Center, Huawei Technologies Co. Ltd., Shenzhen 518129, China
|
| Abstract: |
| Computer systems have been applied in many different areas, and the failure of these systems may bring catastrophic results. Systems in different areas have different requirements, and how to build trustworthy computer systems with high quality is the challenge faced by all these areas. Recently, formal methods with rigorous mathematical foundation have been widely recognized as effective methods for developing trustworthy software and hardware systems. Based on formal methods, this paper presents a classification of requirements of systems and their formalization, to support the design of trustworthy systems. First of all, six types of system characteristics are considered, namely, sequential systems, reactive systems, parallel and communicating systems, real-time systems, probabilistic and stochastic systems, and continuous and hybrid systems. All these systems may run in different application scenarios, with their respective requirements. Four classes of scenarios are considered, i.e., hardware systems, security protocols, information flow, and AI systems. For each class of systems and application scenarios above, the related formal methods are introduced and summarized, including formal modeling, property specification, verification methods and tools. This will allow users of formal methods to choose, based on different system characteristics and application scenarios, the appropriate formal models, verification methods and tools, which ultimately helps the design of more trustworthy systems. |
| Key words: trustworthy system formal method requirement classification verification method and tool |
|
|
|
|
