Trusting computers through trusting humans: software verification in a safety-critical information system

Adam, AE; Spedding, PR

Abstract

This article considers the question of how we may trust automatically generated program code. The code
walkthroughs and inspections of software engineering mimic the ways that mathematicians go about assuring
themselves that a mathematical proof is true. Mathematicians have difficulty accepting a computer
generated proof because they cannot go through the social processes of trusting its construction. Similarly,
those involved in accepting a proof of a computer system or computer generated code cannot go through
their traditional processes of trust. The process of software verification is bound up in software quality
assurance procedures, which are themselves subject to commercial pressures. Quality standards, including
military standards, have procedures for human trust designed into them. An action research case study of
an avionics system within a military aircraft company illustrates these points, where the software quality
assurance (SQA) procedures were incommensurable with the use of automatically generated code.

Citation

Adam, A., & Spedding, P. Trusting computers through trusting humans: software verification in a safety-critical information system. International Journal of Technology and Human Interaction, 3(4), 1-14

• Journal Article Type: Article
• Deposit Date: Apr 3, 2009
• Journal: International Journal of Technology and Human Interaction
• Print ISSN: 1548-3908
• Publisher: IGI Global
• Peer Reviewed: Peer Reviewed
• Volume: 3
• Issue: 4
• Pages: 1-14
• Keywords: Proof, safety-critical systems, software verification, software quality assurance, trust
• Publisher URL: http://www.igi-global.com/articles/details.asp?ID=7494