Abstract Many tools can check if a test set provides control coverage; they are, however, of little or no help when coverage is not achieved and the test set needs to be completed. In this paper, we describe how a formal characterisation of a coverage criterion can be used to generate test data; we present a procedure based on traditional programming techniques like normalisation, and weakest precondition calculation. It is a basis for automation using an algebraic theorem prover. In the worst situation, if automation fails to produce a specific test, we are left with a specification of the compliant test sets. Many approaches to model-based testing rely on formal models of a system under test. Our work, on the other hand, is not concerned with the use of abstract models for testing, but with coverage based on the text of programs.

Abstract For many, Java is the antithesis of a high‐integrity programming language. Its combination of object‐oriented programming features, its automatic garbage collection, and its poor support for real‐time multi‐threading are all seen as particular impediments. The Real‐Time Specification for Java has introduced many new features that help in the real‐time domain. However, the expressive power of these features means that very complex programming models can be created, necessitating complexity in the supporting real‐time virtual machine. Consequently, Java, with the real‐time extensions as they stand, seems too complex for confident use in high‐integrity systems. This paper presents a Java profile for the development of software‐intensive high‐integrity real‐time systems. This restricted programming model removes language features with high overheads and complex semantics, on which it is hard to perform timing and functional analyses. The profile fits within the J2ME framework and is consistent with well‐known guidelines for high‐integrity software development, such as those defined by the U.S. Nuclear Regulatory Commission. Copyright © 2005 John Wiley & Sons, Ltd.

In this paper, we present the Ravenscar-Java profile from the perspective of memory utilization. This restricted programming model removes language features with high overheads and complex semantics, on which it is hard to perform various static analyses. Several classes in the RTSJ are refined, and a few new classes are added, which all result in a compact, yet powerful and predictable computational model for the development of software-intensive high integrity real-time systems. We provide rationales behind the decisions we have made on the use of memory areas and other language features that can have an effect on the predictability of memory utilization. After that, some analysis approaches are discussed in terms of how they can be developed and beneficially used.

The paper describes the use of formal development methods on an industrial safety-critical application. The Z notation was used for documenting the system specification and part of the design, and the SPARK subset of Ada was used for coding. However, perhaps the most distinctive nature of the project lies in the amount of proof that was carried out: proofs were carried out both at the Z level (approximately 150 proofs in 500 pages) and at the SPARK code level (approximately 9000 verification conditions generated and discharged). The project was carried out under UK Interim Defence Standards 00-55 and 00-56, which require the use of formal methods on safety-critical applications. It is believed to be the first to be completed against the rigorous demands of the 1991 version of these standards. The paper includes comparisons of proof with the various types of testing employed, in terms of their efficiency at finding faults. The most striking result is that the Z proof appears to be substantially more efficient at finding faults than the most efficient testing phase. Given the importance of early fault detection, we believe this helps to show the significant benefit and practicality of large-scale proof on projects of this kind.

Abstract. Some clarification is made of a recent article in Formal Aspects of Computing [Hen98]. Specifically, it is noted that the inconsistency found is in a draft logic, which is clearly unfinished. The latest news of the position of the Z Standards Panel on a logic for Z is given.

Abstract Although many programming languages contain exception handling mechanisms, their formal treatment — necessary for rigorous development — can be complex. Nevertheless, this paper presents a simple incorporation of exit commands and exception blocks into a rigorous program development method. The refinement calculus, chosen for the exercise, is a method of developing imperative programs. It is based on weakest preconditions, although they are not used explicitly during program construction; they merely justify the general method. In the style of the refinement calculus, program development laws are given that introduce and allow the manipulation of exit s. The soundness of the new laws is shown using weakest preconditions (as for the existing refinement calculus laws). The extension of weakest preconditions needed to handle exit s is a variation on earlier work of Cristian; the variation is necessary to handle nondeterminism.