可信系统性质的分类和形式化研究综述
作者:
作者单位:

作者简介:

王淑灵(1981-),女,博士,副研究员,CCF专业会员,主要研究领域为嵌入式系统的建模与验证;
金翔宇(1996-),男,博士生,主要研究领域为混成系统的模型学习;
詹博华(1989-),男,博士,副研究员,CCF专业会员,主要研究领域为交互式定理证明,嵌入式系统的建模与验证;
薛白(1986-),男,博士,研究员,CCF专业会员,主要研究领域为混成系统和AI形式验证;
吴昊(1997-),男,硕士生,主要研究领域为形式化验证;向霜晴(1992-),女,博士,主要研究领域为形式化方法,认知逻辑,可信理论;易士程(1998-),男,硕士生,主要研究领域为形式化验证;向展(1991-),男,硕士,主要研究领域为形式化验证,深度学习,网络安全;王令泰(1993-),女,博士生,主要研究领域为混成系统安全与隐私的形式化验证;毛碧飞(1970-),女,硕士,主要研究领域为可信基础理论,IPD可信框架和方法,可信验证与量化评估框架,基于声明的论证,技术伦理前瞻性评估.

通讯作者:

詹博华,E-mail:bzhan@ios.ac.cn

中图分类号:

基金项目:

国家自然科学基金(61972385,62032024,61836005)


Survey on Requirements Classification and Formalization of Trustworthy Systems
Author:
Affiliation:

Fund Project:

  • 摘要
  • |
  • 图/表
  • |
  • 访问统计
  • |
  • 参考文献
  • |
  • 相似文献
  • |
  • 引证文献
  • |
  • 资源附件
  • |
  • 文章评论
    摘要:

    计算机系统被应用于各种重要领域,这些系统的失效可能会带来重大灾难.不同应用领域的系统对于可信性具有不同的要求,如何建立高质量的可信计算机系统,是这些领域共同面临的巨大挑战.近年来,具有严格数学基础的形式化方法已经被公认为开发高可靠软硬件系统的有效方法.目标是对形式化方法在不同系统的应用进行不同维度的分类,以更好地支撑可信软硬件系统的设计.首先从系统的特征出发,考虑6种系统特征:顺序系统、反应式系统、并发与通信系统、实时系统、概率随机系统以及混成系统.同时,这些系统又运行在众多应用场景,分别具有各自的需求.考虑4种应用场景:硬件系统、通信协议、信息流以及人工智能系统.对于以上的每个类别,介绍和总结其形式建模、性质描述以及验证方法与工具.这将允许形式化方法的使用者对不同的系统和应用场景,能够更准确地选择恰当的建模、验证技术与工具,帮助设计人员开发更加可靠的系统.

    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.

    参考文献
    相似文献
    引证文献
引用本文

王淑灵,詹博华,盛欢欢,吴昊,易士程,王令泰,金翔宇,薛白,李静辉,向霜晴,向展,毛碧飞.可信系统性质的分类和形式化研究综述.软件学报,2022,33(7):2367-2410

复制
分享
文章指标
  • 点击次数:
  • 下载次数:
  • HTML阅读次数:
  • 引用次数:
历史
  • 收稿日期:2021-09-05
  • 最后修改日期:2021-10-14
  • 录用日期:
  • 在线发布日期: 2022-01-28
  • 出版日期: 2022-07-25
您是第位访问者
版权所有:中国科学院软件研究所 京ICP备05046678号-3
地址:北京市海淀区中关村南四街4号,邮政编码:100190
电话:010-62562563 传真:010-62562533 Email:jos@iscas.ac.cn
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号