Authors: Thomas Hallgren, James Hook, Mark P. Jones and Dick Kieburtz.
Presented at the High Confidence Software and Systems Conference, April 2004 (HCSS04).
Full paper available as: PDF (259KB), HTML.
Introduction
With ever increasing use of computers in safety and security critical applications, the need for trustworthy computer systems has never been greater. But how can such trust be established? For example, how can we be sure that our computer systems will not destroy or corrupt valuable data, compromise privacy, or trigger serious failures that could, in the worst cases, lead to loss of life?Industry and academia have attacked this problem in many different ways, demonstrating concretely that the use of techniques such as systematic design processes, rigorous testing, or formal methods can each contribute significantly to increased reliability, security, and trustworthiness. There are obviously some significant differences between these techniques, but there is also a unifying feature: each one results in some tangible form of evidence that provides a basis for trust. Examples of such evidence include a record of the meeting where a code review was conducted, the set of test cases to which an application was subjected, or a formal proof that establishes the validity of a critical property.
Unfortunately, the diversity, volume, and variability of evidence that is needed in practice, even in the development of some fairly small systems, makes it hard to manage, maintain, and exploit this evidence as a project evolves and as meaningful levels of assurance are required. Without support, practical difficulties like these could easily discourage or prevent system builders from capturing and leveraging evidence to produce systems in which they, and their users, can develop a well-placed trust.
In the Programatica project at OGI, we are exploring the role that tools can play in facilitating and supporting effective use of evidence during the design, development and maintenance of complex software systems. From a programmer's perspective, Programatica provides a development environment for an extended version of the functional programming language Haskell that provides a notation (and an associated logic, called P-logic) for expressing properties of Haskell code. From a verification perspective, we expect that a broad spectrum of techniques will be useful in establishing such properties, including code review, testing, and formal methods. To support evidence management, Programatica provides: mechanisms for capturing different forms of evidence in certificates; methods exploiting fine-grained dependency analysis to automate the tasks of tracking, maintaining, and reestablishing evidence as a system evolves; and tools to help users understand, manage, and guide further development and validation efforts. One way to understand Programatica is as a framework for Extreme Formal Methods: we expect property assertions to be developed and established in parallel with the code that they document, just as test cases are developed in extreme programming.
This paper describes the current version of the Programatica tools and illustrates how they address some of the above goals in practice.