基于推导树模型的软件可信性推理

doi:10.1007/s12204-022-2515-5

J Shanghai Jiaotong Univ Sci ›› 2024, Vol. 29 ›› Issue (3): 579-587.doi: 10.1007/s12204-022-2515-5

基于推导树模型的软件可信性推理

邓玉欣1，陈泽众1，汪洋1，杜文杰2，毛碧飞3，梁智章3，林秋诗3，李静辉3

（1.华东师范大学上海市高可信计算重点实验室，上海200062；2. 上海师范大学，上海200233；3. 华为技术有限公司可信理论、技术与工程实验室，广东深圳 518129）

收稿日期:2021-12-15 接受日期:2021-12-27 出版日期:2024-05-28 发布日期:2024-05-28

Reasoning about Software Trustworthiness with Derivation Trees

DENG Yuxin^1* (邓玉欣),CHEN Zezhong¹ (陈泽众),WANG Yang¹(汪洋), DU Wenjie²(杜文杰),MAO Bifei³(毛碧飞), LIANG Zhizhang ³(梁智章), LIN Qiushi³(林秋诗),LI Jinghui³(李静辉)

(1. Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, Shanghai 200062, China; 2. Shanghai Normal University, Shanghai 200233, China; 3. Trustworthiness Theory Research Center, Huawei Technologies Co., Ltd., Shenzhen 518129, Guangdong, China)

Received:2021-12-15 Accepted:2021-12-27 Online:2024-05-28 Published:2024-05-28

摘要/Abstract

摘要： 为分析复杂软件系统的可信性，提出了一个基于证据的软件可信模型，可信推导树（TDT）。构造一棵可信推导树的基本思想是把主要属性分解为关键要素，继续精化直至到达基本事实，比如证据。一个TDT的框架可以由一个规则的集合描述，便于在Prolog中实现自动化推理。开发了一个可视化工具，不仅能够通过输入规则自动构建TDT框架，还允许用户通过图形界面进行编辑。在软件开发生命周期中，TDT可作为一种沟通手段，为不同利益相关方在需求分析阶段就系统属性达成共识，并在产品验证阶段通过演绎推理验证系统是否达到可信性。在十多个实际软件开发场景中，试用了TDT方法。使用TDT能帮助我们发现并解决一些微妙的问题。

关键词: 可信性，精化，证据，可视化

Abstract: In order to analyze the trustworthiness of complex software systems, we propose a model of evidencebased software trustworthiness called trustworthiness derivation tree (TDT). The basic idea of constructing a TDT is to refine main properties into key ingredients and continue the refinement until basic facts such as evidences are reached. The skeleton of a TDT can be specified by a set of rules, which are convenient for automated reasoning in Prolog. We develop a visualization tool that can construct the skeleton of a TDT by taking the rules as input, and allow a user to edit the TDT in a graphical user interface. In a software development life cycle, TDTs can serve as a communication means for different stakeholders to agree on the properties about a system in the requirement analysis phase, and they can be used for deductive reasoning so as to verify whether the system achieves trustworthiness in the product validation phase. We have piloted the approach of using TDTs in more than a dozen real scenarios of software development. Indeed, using TDTs helped us to discover and then resolve some subtle problems.

Key words: trustworthiness, refinement, evidence, visualization

中图分类号:

TP311

邓玉欣1，陈泽众1，汪洋1，杜文杰2，毛碧飞3，梁智章3，林秋诗3，李静辉3. 基于推导树模型的软件可信性推理[J]. J Shanghai Jiaotong Univ Sci, 2024, 29(3): 579-587.

DENG Yuxin^1* (邓玉欣),CHEN Zezhong¹ (陈泽众),WANG Yang¹(汪洋), DU Wenjie²(杜文杰),MAO Bifei³(毛碧飞), LIANG Zhizhang ³(梁智章), LIN Qiushi³(林秋诗),LI Jinghui³(李静辉). Reasoning about Software Trustworthiness with Derivation Trees[J]. J Shanghai Jiaotong Univ Sci, 2024, 29(3): 579-587.

参考文献

[1] LI J H, MAO B F, LIANG Z Z, et al. Trust and trustworthiness: What they are and how to achieve them [C]//2021 IEEE International Conference on Pervasive Computing and Communications Workshops and other Affiliated Events. Kassel: IEEE, 2021: 711-717.
[2] CLOCKSIN W F, MELLISH C S. Programming in Prolog [M]. Berlin, Heidelberg: Springer, 2003.
[3] BISHOP P, BLOOMFIELD R. A methodology for safety case development [J]. Safety and Reliability, 2000, 20(1): 34-42.
[4] BLOOMFIELD R, BISHOP P. Safety and assurance cases: Past, present and possible future – an adelard perspective [M]//Making systems safer. London: Springer, 2010: 51-67.
[5] International Organization for Standardization. Systems and software engineering – Systems and software assurance – Part 2: Assurance case: ISO/IEC 15026-2 [S]. Geneva: IOS, 2011.
[6] WANG R, GUIOCHET J, MOTET G, et al. D-S theory for argument confidence assessment [M]//Belief functions: Theory and applications. Cham: Springer, 2016: 190-200.
[7] DEMPSTER A P. New method for reasoning towards posterior distributions based on sample data [J]. The Annals of Mathematical Statistics, 1966, 37(2): 355-374.
[8] DEMPSTER A P. Upper and lower probabilities induced by a multivalued mapping [J]. The Annals of Mathematical Statistics, 1967, 38(2): 325-339.
[9] SHAFER G. A mathematical theory of evidence [M]. Princeton: Princeton University Press, 1976.
[10] RINEHART D J, KNIGHT J, ROWANHILL J C. Current practices in constructing and evaluating assurance cases with applications to aviation [R]. Hampton: NASA, 2015.
[11] RINEHART D, KNIGHT J, ROWANHILL J. Understanding what it means for assurance cases to “work” [R]. Hampton: NASA, 2017.
[12] KELLY T, WEAVER R. The goal structuring notation: A safety argument notation [C]// Dependable Systems and Networks Workshop on Assurance Cases. Heslington: University of York, 2004.
[13] BLOOMFIELD R, BISHOP P, JONES C, et al. The adelard safety case development(ASCAD) manual [EB/OL]. (1998-07-01). https://www.adelard.com/resources/ascad.html.
[14] BLOOMFIELD R, NETKACHOVA K. Building blocks for assurance cases [C]//2014 IEEE International Symposium on Software Reliability Engineering Workshops. Naples: IEEE, 2014: 186-191.
[15] ANDERSON T, BLOOMFIELD R, BULL S, et al. Goal Structuring Notation [EB/OL]. [2022-01-08]. https://scsc.uk/gsn?page=gsn%206tools.
[16] WINSKEL G. The formal semantics of programming languages: An introduction [M]. Cambridge: MIT Press, 1993.
[17] WIELEMAKER J, LAGER T, RIGUZZI F. SWISH: SWI-Prolog for sharing [DB/OL]. (2015-11-03). https://arxiv.org/abs/1511.00915.
[18] TOULMIN S E. The uses of argument [M]. Cambridge: Cambridge University Press, 2003.
[19] WOODCOCK J, LARSEN P G, BICARREGUI J, et al. Formal methods: Practice and experience [J]. ACM Computing Surveys, 2009, 41(4): 19.
[20] ALEXY R, ADLER R, MACCORMICK N. A theory of legal argumentation the theory of rational discourse as theory of legal justification [M]. Oxford: Oxford University Press, 1989.
[21] WANG R, GUIOCHET J, MOTET G, et al. Modelling confidence in railway safety case [J]. Safety Science, 2018, 110: 286-299.

基于推导树模型的软件可信性推理

Reasoning about Software Trustworthiness with Derivation Trees

PDF (PC)

可视化

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 3

编辑推荐

Metrics

本文评价

[1]	高晓彤1，马艳芳1,2，周伟1. 基于FAHP-CRITIC方法的软件可信性分析[J]. J Shanghai Jiaotong Univ Sci, 2024, 29(3): 588-600.
[2]	曾志贤，曹建军，翁年凤，袁震，余旭. 基于细粒度联合注意力机制的图像-文本跨模态实体分辨[J]. J Shanghai Jiaotong Univ Sci, 2023, 28(6): 728-737.
[3]	曹鹤玲a,b，刘方正a，石建树a，楚永贺a，邓淼磊a. 基于随机搜索和代码相似性的程序自动修复[J]. J Shanghai Jiaotong Univ Sci, 2023, 28(6): 738-752.