Reasoning about Software Trustworthiness with Derivation Trees

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

• Automation & Computer Technologies • Previous Articles Next Articles

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

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

Abstract

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

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

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

CLC Number:

TP311

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.

References

[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)

Knowledge

Abstract

Cite this article

share this article

References

Related Articles 3

Recommended Articles

Metrics

Comments

[1]	GAO Xiaotong1¹ (高晓彤), MA Yanfang^1，2* (马艳芳), ZHOU Wei¹ 周伟). Analysis of Software Trustworthiness Based on FAHP-CRITIC Method [J]. J Shanghai Jiaotong Univ Sci, 2024, 29(3): 588-600.
[2]	ZENG Zhirian(曾志贤),CAO Jianjun*(曹建军),WENG Nianfeng(翁年凤)，YUAN Zhen(袁震)，YU Xu(余旭). Cross-Modal Entity Resolution for Image and Text Integrating Global and Fine-Grained Joint Attention Mechanism [J]. J Shanghai Jiaotong Univ Sci, 2023, 28(6): 728-737.
[3]	CAO Heling,a,b (曹鹤玲),LIU Fangzhenga (刘方正)，SHI Jianshua (石建树),CHU Yonghea (楚永贺)，DENG Miaoleia*. (邓淼磊). Random Search and Code Similarity-Based Automatic Program Repair [J]. J Shanghai Jiaotong Univ Sci, 2023, 28(6): 738-752.