Every year, British Telecom's (BT's) level of investment in software is growing. Not only is the level of investment high, but there is a great deal of reliance on this software to retain BT's competitive edge against stiff competition. The software is, therefore, likely to be working in a commercially critical environment where the cost of failure is high both in terms of lost revenue and good will. Techniques are available, at various levels of maturity, which can help to provide added assurance against software failure. The first part of the paper relates specifically to the ESPRIT COSMOS project and work within BT on validating measures gathered using the COSMOS tool at the source code level. The second part of the paper describes how the results of this project fit within the wider context of software assessment, and outlines some of the techniques that are currently being used within BT or are being developed. The paper concludes with a brief description of what may be viable in the next few years.>

Abstract LOTOS is one of the most recent formal description languages to appear and one of very few with a standard definition. It has both a process algebra and an abstract data‐type component, and these facilities are used in combination to describe the behaviour of concurrent systems. The purpose of this paper is to examine, in a tutorial style, what is involved in constructing and taking benefit from such descriptions. The presentation is illustrated through the development of two formal descriptions for the children's game of pass‐the‐parcel. These descriptions and a concise summary of the main features of LOTOS are given as appendices. Many of the points made in the paper apply equally well to other process‐oriented languages such as CCS and CSP.

A key factor in the acceptance of high level programming languages has been the development of a comprehensive set of tools to support the user. If formal languages for specification are to achieve the same level of acceptance, they too will require extensive automated support. This paper describes a set of prototype tools which are designed to assist the developer in the use of fortnal specilication techniques.