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.
DENG Yuxin1* (邓玉欣),CHEN Zezhong1 (陈泽众),WANG Yang1(汪洋), DU Wenjie2(杜文杰),MAO Bifei3(毛碧飞), LIANG Zhizhang 3(梁智章), LIN Qiushi3(林秋诗),LI Jinghui3(李静辉)
. Reasoning about Software Trustworthiness with Derivation Trees[J]. Journal of Shanghai Jiaotong University(Science), 2024
, 29(3)
: 579
-587
.
DOI: 10.1007/s12204-022-2515-5
[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.
