Publications

This is a list of the publications which I have written, singly or jointly.

Journals
Refereed Conferences
Refereed Workshops
Technical Reports / Thesis
Posters

Developing Critical Systems with PLD Components

Adrian J. Hilton and Jon G. Hall
In: Proceedings of the Tenth International Workshop on Formal Methods for Industrial Critical Systems (FMICS)
September 2005

Abstract

Understanding the roles that rigour and formality can have in the design of critical systems is critical to anyone wishing to contribute to their development. Whereas knowledge of these issues is good in software development, in the use of hardware -- specifically programmable logic devices (PLDs) and the combination of PLDs and software -- the issues are less well known. Indeed, even in industry there are many differences between current and recommended practice and engineering opinion differs on how to apply existing standards. This situation has led to gaps in the formal and rigorous treatment of PLDs in critical systems.

In this paper we examine the range of and potential for formal specification and analysis techniques that address the requirements for verifiable PLD programs. We identify existing formalisms that may be used, and lay out the areas of contributions that academia and industry in collaboration can make that would allow high-integrity PLD programming to be as practicable as high-integrity software development.

This paper also touches briefly on some important practical, technical, organisational, social, and psychological aspects of the introduction of formal methods into industrial practice for hardware and system design. It also provides an update and summary of the recent UK Defence Standard 00-56, as it relates to hardware.

@inproceedings{hilton05,
  title="Developing critical systems with {PLD} components",
  author="Adrian J. Hilton and Jon G. Hall",
  crossref="fmics05"
}

@proceedings{fmics05,
  title="Tenth International Workshop on Formal Methods for Industrial Critical Systems",
  booktitle="Tenth International Workshop on Formal Methods for Industrial Critical Systems",
  location="Lisbon, Portugal",
  publisher="Elsevier",
  month="September",
  year=2005
}

FMICS 2005 PDF (136Kb)

Practical Experiences of Safety- and Security-Critical Technologies

Peter Amey and Adrian J. Hilton
In: Ada User Journal, June 2004
June 2004

Abstract

In this article we identify the special properties of systems intended for use in ultra-reliable domains and the qualitative shift in development methods needed to achieve these properties. The advantages (and disadvantages) of Ada are introduced in the contexts of the ISO HRG report on High- Integrity Ada and of the SPARK sub-language. The demands of common important development standards are described together with appropriate and cost-effective techniques for meeting them. Finally project experience illustrating successes in meeting the main standards is discussed.

@article{amey04,
  title="Practical Experiences of Safety- and Security-Critical Technologies",
  author="Peter Amey and Adrian J. Hilton",
  journal="Ada User Journal",
  volume=25,
  number=2,
  pages="98--106",
  month="June",
  year=2004
}

Ada User Journal 2004 PDF (337Kb PDF)

High Integrity Hardware-Software Codesign

Adrian J. Hilton
Ph.D. thesis, The Open University
April 2004

Abstract

Programmable logic devices (PLDs) are increasing in complexity and speed, and are being used as important components in safety-critical systems. Methods for developing high-integrity software for these systems are well-known, but this is not true for programmable logic.

We propose a process for developing a system incorporating software and PLDs, suitable for safety critical systems of the highest levels of integrity. This process incorporates the use of Synchronous Receptive Process Theory as a semantic basis for specifying and proving properties of programs executing on PLDs, and extends the use of SPARK Ada from a programming language for safety-critical systems software to cover the interface between software and programmable logic.

We have validated this approach through the specification and development of a substantial safety-critical system incorporating both software and programmable logic components, and the development of tools to support this work.

This enables us to claim that the methods demonstrated are not only feasible but also scale up to realistic system sizes, allowing development of such safety-critical software-hardware systems to the levels required by current system safety standards.

@phdthesis{hilton04a,
  title="High Integrity Hardware-Software Codesign",
  author="Adrian J. Hilton",
  school="The Open University",
  month="April",
  year=2004}

Thesis PDF (1.1Mb PDF)

High Integrity Interfacing to Programmable Logic with Ada

Adrian J. Hilton and Jon G. Hall
In Proceedings of the 9th Ada-Europe International Conference on Reliable Software Technologies (Ada-Europe 2004)
June 2004

Abstract

Programmable logic devices (PLDs) are now common components of safety-critical systems, and are increasingly used for safety-related or safety-critical functionality. Recent safety standards demand similar rigour in PLD specification, design and verification to that in critical software design. Existing PLD development tools and techniques are inadequate for the higher integrity levels.

In this paper we examine the use of Ada as a design language for PLDs. We analyse earlier work on Ada-to-HDL compilation and identify where it could be improved. We show how program fragments written in the SPARK Ada subset can be efficiently and rigorously translated into PLD programs, and how a SPARK Ada program can be effectively interfaced to a PLD program. The techniques discussed are then applied to a substantial case study and some preliminary conclusions are drawn from the results.

@inproceedings{hilton04,
  title="High-Integrity Interfacing to Programmable Logic with {Ada}",
  author="Adrian J. Hilton and Jon G. Hall",
  pages="249--260",
  crossref="adaeurope04"}
@proceedings{adaeurope04,
  title="Proceedings of the 9th Ada-Europe International Conference on Reliable Software Technologies (Ada-Europe 2004)",
  booktitle="Proceedings of the 9th Ada-Europe International Conference on Reliable Software Technologies (Ada-Europe 2004)",
  editor="Albert Llamos{\'{i}} and Alfred Strohmeier",
  publisher="Springer",
  volume="3063",
  series="Lecture Notes in Computer Science",
  location="Palma de Mallorca, Spain",
  month="June",
  year=2004}

Ada Europe 2004 PDF (147Kb PDF)

NB: won Best Presentation award

Enforcing Security and Safety Models with an Information Flow Analysis Tool

Roderick Chapman and Adrian J. Hilton
In Proceedings of SIGAda 2004
November 2004

Abstract

Existing security models require that information of a given security level be prevented from "leaking" into lower-security information. High-security applications must be demonstrably free of such leaks, but such demonstration may require substantial manual analysis. Other authors have argued that the natural way to enforce these models automatically is with information-flow analysis, but have not shown this to be practicable for general purpose programming languages in current use.

Modern safety-critical systems can contain software components with differing safety integrity levels, potentially operating in the same address space. This case poses problems similar to systems with differing security levels; failure to show separation of data may require the entire system to be validated at the higher integrity level.

In this paper we show how the information flow model enforced by the SPARK Examiner provides support for enforcing these security and safety models. We describe an extension to the SPARK variable annotations which allows the specification of a security or safety level for each state variable, and an extension to the SPARK analysis which automatically enforces a given information flow policy on a SPARK program.

@inproceedings{chapman04,
  title="Enforcing Security and Safety Models with an Information Flow Analysis Tool",
  author="Roderick Chapman and Adrian Hilton",
  organization="Praxis Critical Systems Ltd.",
  crossref="sigada04"}

@proceedings{sigada04,
  title="Proceedings of SIGAda 2004",
  booktitle="Proceedings of SIGAda 2004",
  location="Atlanta, Georgia, USA",
  editor="Ricky Sward",
  month="November",
  year=2004}

SIGADA 2004 PDF (112 Kb)

Engineering Software Systems for Customer Acceptance

Adrian J. Hilton
In Proceedings of the workshop on Software Engineering of High-Assurance Systems (SEHAS'03) (published by SEI)
May 2003

Abstract

Building a software system is a well-understood problem with a wide range of solutions, each suitable for some classes of system but not for others. The commercial success of a software system, however, depends on its acceptance by the customer. Therefore, the developer must demonstrate that a system is fit for its purpose. A common view is that following a specified software or systems development process is adequate for this purpose. However, as software and safety standards move from a prescriptive to goal-oriented form, this demonstration of fitness will become more tailored to each system.

In this paper we examine how existing processes and products can be used to build an evidence-based case for high-assurance system acceptance. We draw on our own experience of developing and delivering such systems, and make practical recommendations for improving acceptance rates. We show how existing technologies and tools can support this process.

@inproceedings{hilton03,
  title="Engineering Software Systems for Customer Acceptance",
  author="Adrian J. Hilton", 
  organization="Praxis Critical Systems Ltd.",
  crossref="sehas03"}
@proceedings{sehas03,
  title="Workshop on Software Engineering for High-Assurance Systems ({SEHAS'03}), Proceedings",
  booktitle="Proceedings of {SEHAS'03}",
  editors="N. Mead and M. Feather and A. Nikora and C. Heitmeyer",
  location="Portland, Oregon",
  month="May",
  year=2003}

SEHAS 2003 PDF [47Kb PDF]

White Box Software Development

Dewi Daniels, Richard Myers and Adrian Hilton
In Proceedings of the 11th Safety-Critical Systems Symposium (published by Springer-Verlag)
February 2003

Abstract

This article attempts to debunk the populist view that building high quality software is difficult and costly, and that having software systems that crash is an acceptable state of affairs.

The technology to build predictable reliable software systems exists today. Principled engineering judgement can be used to tailor software development so that quality can be built in with cost in mind -- this is particularly the case with safety-critical systems, where the application of standards can force an unnecessarily rigorous approach for little proven benefit.

This article explores the general poor quality of software "in the large", the public's (and the industry's) view that this is in some way acceptable, and then presents some real case studies which show how quality can be built in without the need to invest in overweight tools and technologies.

@inproceedings{daniels03,
  title="White Box Software Development",
  author="Dewi Daniels and Richard Myers and Adrian Hilton",
  organization="Praxis Critical Systems Ltd.",
  crossref="sss03"}
@proceedings{sss03,
  title="Current Issues in Safety-critical systems",
  booktitle="Proceedings of the Eleventh Safety-Critical Systems Symposium",
  editor="F. Redmill and T. Anderson",
  location="Bristol, England",
  publisher="Springer-Verlag",
  month="February", 
  year=2003}

SCS 2003 PDF [311Kb PDF]

FPGAs in Critical Hardware/Software Systems

Adrian J. Hilton, Gemma Townson and Jon G. Hall
In Proceedings of FPGA 2003 (published by ACM)
February 2003

Abstract

FPGAs are being used in increasingly complex roles in critical systems, interacting with conventional critical software. Established safety standards require rigorous justification of safety and correctness of the conventional software in such systems. Newer standards now make similar requirements for safety-related electronic hardware, such as FPGAs, in these systems.

In this paper we examine the current state-of-the-art in programming FPGAs, and their use in conventional (low-criticality) hardware/software systems. We discuss the impact that the safety standards requirements have on the co-development of hardware/software combinations in critical systems and suggest adaptations of existing best practice in software development that could discharge them. We pay particular attention to the development and analysis of high-level language programs for FPGAs designed to interact with conventional software.

@techreport{hilton03b,
  title = "FPGAs in Critical Hardware/Software Systems",
  author = "Adrian J. Hilton and Gemma Townson and Jon G. Hall",
  institution = "The Open University",
  number = "2003/1",
  year=2003}

(Accepted as a poster, made available as an OU technical report)

Mandated Requirements for Hardware / Software Combination in Safety-Critical Systems

Adrian J. Hilton and Jon G. Hall
In: Proceedings of RHAS 2002 (published by SEI)
September 2002

Abstract

Safety-critical systems are an important subset of high-assurance systems. Higher performance requirements have led to the increased use of combined hardware/software systems therein, with hardware devices taking processing load off software.

As might be expected, safety-critical systems have many requirements made of them by established standards. By implication, and now by emerging safety standards, such requirements must be discharged over hardware/software combinations, with important ramifications for best practice.

In this paper we discuss the impact that such requirements have on the co-development of hardware/software combinations, and suggest adaptations of existing best practice that could discharge them.

@inproceedings{hilton02b,
  title = "Mandated Requirements for Hardware/Software Combination in Safety-Critical Systems",
  author = "Adrian J. Hilton and Jon G. Hall",
  institution = "The Open University",
  crossref = "rhas02"}
@proceedings{rhas02,
  title = "Proceedings of the workshop on Requirements for High-Assurance Systems 2002",
  booktitle = "Proceedings of the workshop on Requirements for High-Assurance Systems 2002",
  organization = "Software Engineering Institute, Carnegie-Mellon University",
  location = "Essen, Germany",
  month = "September",
  year = 2002}

RHAS 2002 PDF [120Kb PDF]

Refining Specifications to Programmable Logic

Adrian J. Hilton and Jon G. Hall
In: Proceedings of the Refinement workshop at Formal Methods Europe (REFINE 2002) (published by the University of Kent at Canterbury)
July 2002

Abstract

Combined hardware/software systems are increasingly being used for safety-critical systems, with hardware taking processing load off the software. To attain the necessary safety integrity levels, new safety standards require that the correctness arguments for safety-critical hardware and software are developed together with the same rigour as for software alone.

In this paper we describe work in progress on the continuing development of such a notation and proof system. Based on process description using Synchronous Receptive Proof Theory, we propose refinement rules for developing a specification into an SRPT implementation.

As illustration, we demonstrate the full formal refinement of a 2k bit carry look-ahead adder into a Pebble implementation, and test the implementation.

@inproceedings{hilton02a,
  title = "Refining specifications to programmable logic",
  author = "Adrian J. Hilton and Jon G. Hall",
  institution = "The Open University",
  crossref = "refine02"}
@proceedings{refine02,
  title = "Proceedings of REFINE 2002",
  booktitle = "Proceedings of REFINE 2002",
  editor = "John Derrick and Eerke Boiten and Jim Woodcock and Joakim von Wright",
 series = "Electronic Notes in Theoretical Computer Science",
  publisher = "Elsevier",
  volume = 30,
  issue = 3,
  location = "Copenhagen, Denmark",
  month = "November",
  year= 2002}

REFINE 2002 PDF [222Kb PDF]

Proving Safety Properties of FPGAs

Adrian J. Hilton and Jon G. Hall
In: Proceedings of the Ninth ACM/SIGDA International Symposium on Field Programmable Gate Arrays (published by ACM)
February 2001

Abstract

FPGAs are increasing in complexity and being used as important components of safety-critical systems. Emerging safety standards require analytic reasoning to demonstrate the safety of FPGAs in such systems. We describe a method which uses a synchronous process algebra to produce formal proof that an FPGA program satisfies safety properties, and demonstrates its use in the specification of safety functions for a safety-critical system.

(Accepted as a poster.)

On Applying Software Development Best Practice to FPGAs in Safety-Critical Systems

Adrian J. Hilton and Jon G. Hall
In: Proceedings of the 10th International Conference on Field Programmable Logic and Applications (FPL'00) (published by Springer-Verlag)
Lecture Notes in Computer Science volume 1896,
August 2000

Abstract

The recent increase in the functionality of programmable logic devices allows them to take an increasingly important role in complex electronic systems. Consequently, new standards for safety-critical systems require the developer to demonstrate the safety and correctness of programmable logic in such systems. In this paper we survey current approaches with a view to determining a suitable approach, derived from existing software best practice.

@inproceedings{hilton00,
   title = "On Applying Software Development Best Practice to   
            {FPGAs} in Safety-Critical Systems",
   author = "Adrian Hilton and Jon Hall",
   crossref = "fpl00"}
@proceedings{fpl00,
   title = "Proceedings of the 10th International Conference on Field Programmable Logic and Applications ({FPL'00})",
   booktitle = "Proceedings of the 10th International Conference on Field Programmable Logic and Applications ({FPL'00})",
   editor = "Reiner W. Hartenstein and Herbert Gr├╝nbacher",
   publisher = "Springer-Verlag",
   series = "Lecture Notes In Computer Science",
   volume = 1896,
   location = "Villach, Austria",
   month = "August",
   year = 2000}

FPL 2000 PDF [108Kb PDF]

Comments