Presents an overview of the Possum specification animation system and its integration into the Cogito methodology and toolset. Possum allows interpretation (or animation) of specifications written in Sum, the specification language of Cogito. We distinguish two potential uses for Possum and illustrate each of these with an example. The first is the use of Possum for specification verification, where the analysis of properties of specifications by the specification designer is emphasised. The second use is specification validation, where the specification is checked against the informal requirements of the system.

We present an overview of the Possum specification animation system, an addition to the Cogito methodology and toolset. Possum allows interpretation (or animation) of specifications written in SUM, which is the specification language used in Cogito. We give an account of the functionality of Possum, illustrated by some simple examples, and describe the way in which Possum is used in a typical Cogito development. The current capabilities and limitations of Possum are reviewed from a technical perspective and an overview of other systems that support the animation of formal specification languages is presented.

Reports on a collaborative project to pilot the use of formal methods in the development of safety-related software. Using the SVRC's Cogito methodology, staff from CSC Australia undertook: formal specification; validation of the specification by mathematical consistency checks; hazard analysis; and validation of the specification against the safety requirements. Part of the design was modelled formally and verified.

Cogito 1 is the first iteration of a Z-based integrated methodology and support system for formal software development. This paper gives an overview of the Cogito methodology and associated tools. Particular emphasis is placed on the way in which Cogito integrates the various phases of the formal development process and provides comprehensive tools support for all phases of development addressed by the methodology.

Cogito I is the first iteration of a Z-based integrated development methodology and support system for formal software development. This paper gives an overview of the Cogito methodology and associated tools. Particular emphasis is placed on the way in which Cogito integrates the various phases of the formal development process and provides comprehensive tool support for all phases of development addressed by the methodology.>

This paper describes the Cogito Repository Manager. The motivation behind, and structure of, the repository manager are presented in detail. Issues surrounding version and configuration management are also discussed. The way in which process modeling, configuration and version control, and tool integration are combined into a single framework is outlined. An example population which instantiates the system with a C development environment is given. The development has been undertaken, in the context of an integrated system and methodology for the formal construction of programs (Cogito). The repository manager described here forms the central components of the Cogito system.>

Transformations are functions over programs that adhere to some program refinement relation. The power of transformations stems, in the first instance, from the flexibility available within the transformation system for representing design decisions, which requires that transformations be parameterized with the knowledge of problem domain; and second, on the ability to reuse developments in an effective manner, after some modifications have been made to the problem definition. In this paper, knowledge-based transformational programming in the PROSPECTRA system is presented. The strength of this approach arises from the smooth combination of knowledge bases and transformations in the development and re-development of programs. In particular, emphasis is placed on the separation of concerns achieved by the effective partitioning of problem domain knowledge and problem specification.>