Trusting Computers Through Trusting Humans: Software Verification in a Safety-Critical Information System

Trusting Computers Through Trusting Humans: Software Verification in a Safety-Critical Information System

Alison Adam (University of Salford, UK) and Paul Spedding (University of Salford, UK)
DOI: 10.4018/978-1-60566-142-1.ch024
OnDemand PDF Download:


This chapter 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.
Chapter Preview


They have computers, and they may have other weapons of mass destruction. Janet Reno, former US Attorney General

In this chapter our aim is to develop a theoretical framework with which to analyse a case study where one of the authors was involved, acting as an action researcher in the quality assurance procedures of a safety-critical system. This involved the production of software for aeroplane flight systems. An interesting tension arose between the automatically generated code of the software system (i.e., ‘auto-code’—produced automatically by a computer, using CASE [Computer Aided Software Engineering] tools from a high level design) and the requirement of the quality assurance process which had built into it the requirement for human understanding and trust of the code produced.

The developers of the system in the case study designed it around auto-code—computer generated software, free from ‘human’ error, although not proved correct in the mathematical sense, and cheaper and quicker to produce than traditional program code. They looked to means of verifying the correctness of their system through standard software quality assurance (SQA) procedures. However, ultimately, they were unable to bring themselves to reconcile their verification procedures with automatically generated code. Some of the reason for this was that trust in human verification was built into (or inscribed into [Akrich, 1992]) the standards and quality assurance procedures which they were obliged to follow in building the system. Despite their formally couched descriptions, the standards and verification procedures were completely reliant on human verification at every step. However these ‘human trust’ procedures were incompatible with the automated production of software in ways we show below. The end result was not failure in the traditional sense but a failure to resolve incommensurable procedures; one set relying on human trust, one set on computer trust.

Our research question is therefore: How may we understand what happens when software designers are asked to trust the design of a system, based on automatically generated program code, when the SQA procedures and military standards to which they must adhere demand walkthroughs and code inspections which are impossible to achieve with auto-code?

The theoretical framework we use to form our analysis of the case study is drawn from the links we make between the social nature of mathematical proof, the need to achieve trust in system verification, the ways in which we achieve trust in the online world, the methods of software engineering, and within that, the software quality movement and the related highly influential domain of military standards.

In the following section we briefly outline the social nature of mathematical proof. The next section discusses the debate over system verification which encapsulates many of the ideas of mathematical proof and how such proofs can be trusted by other mathematicians. The chapter proceeds to consider ‘computer mediated’ trust, briefly detailing how trust has been reified and represented in computer systems to date, mainly in relation to the commercial interests of e-commerce and information security. Trust is particularly pertinent in the world of safety-critical systems, where failure is not just inconvenient and financially damaging, although commercial pressures are still evident here, but where lives can be lost. The model of trust criticised by e-commerce critics is more similar to the type of trust we describe in relation to safety-critical systems, than one might, at first, expect. Understandably, we would like to put faith in a system which has been mathematically proved to be correct. However computer generated proofs, proofs about correctness of computer software, and automatically generated code are not necessarily understandable or amenable to inspection by people, even by experts. The question then arises of whether we can bring ourselves to trust computer generated proofs or code, when even a competent mathematician, logician,or expert programmer cannot readily understand them.

Complete Chapter List

Search this Book:
Editorial Advisory Board
Table of Contents
Chapter 1
Claus Hohmann
This chapter introduces emotional digitalization as a phenomenon of future information systems. It argues that emotional digitalization is a... Sample PDF
Emotional Digitalization as Technology of the Post-Modern: A Reflexive Examination from the View of The Industry
Chapter 2
Elias A. Hadzilias, Andrea Carugati
This chapter aims at defining a framework for the design of e-government services on cultural heritage. Starting from an analysis of three cases on... Sample PDF
Bridging User Requirements and Cultural Objects: A Process-Oriented Framework for Cultural E-Services
Chapter 3
Samantha Bax, Tanya McGill
The technology acceptance model (TAM) is a popular model for the prediction of information systems acceptance behaviors, defining a causal linkage... Sample PDF
From Beliefs to Success: Utilizing an Expanded TAM to Predict Web Page Development Success
Chapter 4
George E. Heilman, Jorge Brusa
This study assesses the psychometric properties of a Spanish translation of Doll and Torkzadeh’s End- User Computing Satisfaction (EUCS) survey... Sample PDF
Assessing a Spanish Translation of the End-User Computing Satisfaction Instrument
Chapter 5
Ishraga Khattab, Steve Love
Over the last several years, the ubiquitous use of mobile phones by people from different cultures has grown enormously. For example, mobile phones... Sample PDF
Understanding the Impact of Culture on Mobile Phone Usage on Public Places: A Comparison between the UK and Sudan
Chapter 6
Netta Iivari
Users should participate in information technology (IT) artifact development, but it has proven to be challenging. This applies also in the open... Sample PDF
Discourses on User Participation: Findings from Open Source Software Development Context
Chapter 7
Anita Greenhill, Gordon Fletcher
In this article we build upon existing research and commentary from a variety of disciplinary sources, including information systems, organisational... Sample PDF
Exploring "Events" as an Information Systems Research Methodology
Chapter 8
Hannakaisa Isomäki
This chapter describes a study clarifying information systems (IS) designers’ conceptions of human users of IS by drawing on in-depth interviews... Sample PDF
Different Levels of Information Systems Designers' Forms of Thought and Potential for Human-Centered Design
Chapter 9
Barbara Jones, Angelo Failla, Bob Miller
Constant renewal of the self-image and self-knowledge of the organisation becomes part of the day-to-day knowledge-in-use of front-line... Sample PDF
Tacit Knowledge in Rapidly Evolving Organisational Environments
Chapter 10
Anastasia Papazafeiropoulou, Reshma Gandecha
Interpretive flexibility is a term used to describe the diverse perspectives on what a technology is and can or can not do during the process of... Sample PDF
Interpretive Flexibility Along the Innovation Decision Process of the UK NHS Care Records Service (NCRS): Insights from a Local Implementation Case Study
Chapter 11
Sylvie Albert, Rolland LeBrasseur
This article reviews the literature on networks and, more specifically, on the development of community telecommunication networks. It strives to... Sample PDF
Collaboration Challenges in Community Telecommunication Networks
Chapter 12
Mary R. Lind
In this article, wireless technology use is addressed with a focus on the factors that underlie wireless interaction. A de-construction of the... Sample PDF
A De-Construction of Wireless Device Usage
Chapter 13
François-Xavier de Vaujany
The following chapter suggests a critical realistic framework, which aims at modeling sociotechnical change linked to end-users’ IT appropriation... Sample PDF
Modeling Sociotechnical Change in IS with a Quantitative Longitudinal Approach: The PPR Method
Chapter 14
Janet C. Dunlop
Today’s media are vast in both form and influence; however, few cultural studies scholars address the video gaming industry’s role in domestic... Sample PDF
The U.S. Video Game Industry: Analyzing Representation of Gender and Race
Chapter 15
Luciano Floridi
The article argues that Information Ethics (IE) can provide a successful approach for coping with the challenges posed by our increasingly... Sample PDF
Global Information Ethics: The Importance of Being Environmentally Earnest
Chapter 16
Philip Brey
In this chapter, I examine whether information ethics is culture relative. If it is, different approaches to information ethics are required in... Sample PDF
Is Information Ethics Culture-Relative?
Chapter 17
John Weckert
This chapter examines the concept of offence, both its giving and taking, and argues that such an examination can shed some light on global ethical... Sample PDF
Giving and Taking Offence in a Global Context
Chapter 18
Reima Suomi, Ari Serkkola, Markku Mikkonen
In this chapter we focus on the application of a mobile time reservation system for dental care. The specific application allocates cancelled... Sample PDF
GSM-Based SMS Time Reservation System for Dental Care
Chapter 19
Debra Howcroft, Robert McDonald
Both academics and practitioners have invested considerably in the information systems evaluation arena, yet rewards remain elusive. The aim of this... Sample PDF
An Ethnographic Study of IS Investment Appraisal
Chapter 20
Kevin Gallagher, Robert M. Mason
This chapter frames the requirements definition phase of systems design as a problem of knowledge transfer and learning between two communities of... Sample PDF
Reframing Information System Design as Learning Across Communities of Practice
Chapter 21
Tanya Bondarouk, Maarten van Riemsdijk
In this chapter, we conceptualize the implementation process associated with SAP_HR as an experiential learning one (Kolb, 1984), and analyze... Sample PDF
Successes and Failures of SAP Implementation: A Learning Perspective
Chapter 22
Pietro Murano, Patrik O’Brian Holt
Experimental work on anthropomorphic feedback in user interfaces has shown inconsistent results and researchers offer differing opinions as to the... Sample PDF
Anthropomorphic Feedback in User Interfaces: The Effect of Personality Traits, Context and Grice's Maxims on Effectiveness and Preferences
Chapter 23
Richard Diamond
This study explores decision premises that were used to manage and stabilise a complex technochange programme in a financial institution. Decision... Sample PDF
Several Simple Shared Stable Decision Premises for Technochange
Chapter 24
Alison Adam, Paul Spedding
This chapter considers the question of how we may trust automatically generated program code. The code walkthroughs and inspections of software... Sample PDF
Trusting Computers Through Trusting Humans: Software Verification in a Safety-Critical Information System
About the Editor
About the Contributors