Computational Tree Logic (CTL) model update is an approach to software verification and modification, where minimal change is employed to generate updated models that represent the corrected software design. In this paper, we propose a new update principle named minimal change with maximal reachable states (II) which is a further optimisation of an existing algorithm to solve a model explosion problem during CTL model update. We provide comparison of the two methods based on Graph Theory. The algorithm of this update principle is also provided. Our experimental results show that in the case of updating the Andrew File System protocol model, the new CTL update approach significantly narrows down the committed models to fewer strong committed models.

Architecture description languages (ADLs) and architecture analysis and design languages (AADLs) are important modelling and analysing languages for the software design phase. Around a decade ago, a significant number of ADLs, such as Unicon (9), Rapide (5), Wright (1) and C3 (7), were developed to describe a variety of system features. For example, Rapide describes event triggered dynamic architectures; while Wright describes architectures at a predefined conceptual level. However, these ADLs do not provide strong support for analysis. More recently, the MetaH AADL (2) has been developed, with improved support for analysis and the expression of real-time behaviour.Developed from MetaH AADL, SAE AADL (4) provides further advances on previous ADLs and AADLs, with support for describing dynamic features in real-time systems, and stronger support for analysis than earlier languages. However, this AADL still lacks certain flexibility to express generic and conceptual features of software architectures. Furthermore, it does not provide strong support for error correction and non-functional behaviour 1 is not expressed formally.We propose a new ADL, named CRADLE, with our main aims to provide strong support for: architecture analysis (detecting inconsistencies or violations of functional and/or non-functional constraints); architecture adaptation (correcting these inconsistencies and constraint violations); and architecture expressiveness (being able to describe a variety of architectural features including function properties and non-functional timing constraints using a formal notation).A key feature of CRADLE is the support for defining generic architectures that can be adapted by instantiating parameters. This allows us to model and analyse architectures with more genericity, allowing a single architecture model to capture, for example, differing control styles (e. g. concurrent versus sequential), varying numbers of components, and configurable timing constraints. Furthermore, by providing a library of generic architectures, both high level architectures and lower level sub-architectures, we can provide support for architecture adaptation, by extending existing approaches to component adaptation.Tool support for checking and adapting CRADLE architectures will be based on model checkers and theorem provers. In general, we plan to use model checking to check non-functional properties whereas theorem proving is used to check the functional properties.This paper describes a case study to model an air traffic control scenario using CRADLE. The previous generation ADL Rapide modelled the architecture of the air traffic control system. For simplicity, the architecture consists of aircraft radio components and control tower transmitter/receiver components and the radio components are connected to the transmitter/receiver components. In reality, CRADLE is able to specify bi-directional connection between the aircraft and the tower. There are two possible communication styles: pipeline style (sequential); or broadcast style (concurrent). Both of these architectures can be expressed separately using non-generic CRADLE constructs as Rapide. However using CRADLE we are able to express both possibilities in a single specification. The air traffic control model is described in two parts: interface and configuration. The interface contains types of component and connector. The configuration contains "instance", "connection" and "communication". The structure of the architecture is adjusted by parametrisation. Thus, one architecture describes all possibilities of the system. We demonstrate how the generic and other advance features of CRADLE are properly used in this system to support its particular features and requirements.

Group-based software engineering projects are an important part of computer science and information technology curricula. Fair assessment of individual contributions to group-based projects remains a challenging problem. Peer-based assessment, where students assess their fellow team members, is seen as one answer to this. In this paper we discuss the key aspects that need to be addressed in order to develop a successful peer assessment method. We propose a method for carrying out peer assessments for a large software engineering class. We briefly describe a Web-based tool that we have developed to support our method, and comment on our initial experiences in using the tool.

Architecture description languages (ADLs) describe the abstracted structure of a system. In this paper we describe a new ADL based on extension of the existing CARE language used informally specifying and implementing reusable software components. The main elements of this ADL are components and connectors, with functional and nonfunctional behaviours and interfaces defined. The ADL includes a configuration part, describing the connection between components and connectors, defined using a CSP-like notation. The ADL is amenable to the use of theorem proving techniques for establishing correctness of the architecture. The recursive architecture is also specified as apart of the communication. The design for the CARE ADL is incorporated with the plan to leverage existing tools for matching and adapting CARE components, to develop support for the detection and correction of architecture mismatches (i.e. where components do not interoperate correctly).

Note: Most SVRC technical reports are available via anonymous ftp, from svrc.it.uq.edu.au in the directory /pub/techreports. Individual abstracts and compressed postscript les are available from Abstract This paper outlines a new approach to construction and veriication of software, developed in response to identiied industrial needs for a formal development method which does not require the user to be an expert in mathematical logic. The approach is based on a framework which allows formal veriication to be performed oo-line or consigned to automated tools, thereby allowing the software engineer to concentrate instead on the design and development of useable, eecient pieces of software.

A number of formal approaches to component-based software development have been proposed, based on the idea of using formal specifications as a basis for retrieval. These approaches provide good recall and precision when searching for components. More recently, the problem of component adaptation has begun to be addressed, in recognition of the fact that a library component will rarely meet the needs of the user exactly. However the main weakness of the current approaches is they only cater for a single adaptation step. In reality, we typically need to apply some combination of adaptation steps. In this paper we present a collection of search tactics, which allow us to combine a sequence of matching and adaptation commands into a single step. The tactics are presented in a general manner, with the intention that they could be applied to a variety of different formal-based approaches to CBSD. We illustrate the use of the search tactics using a simple example.

Any program that measures quantities from its physical environment must compute using correct and consistent units of measurement. Such a program is described as well-measuring. In many systems, particularly embedded control software, paying inadequate attention to units of measurement can result in catastrophe. Unfortunately, current programming languages and tools provide little aid to the programmer attempting to establish or verify the well-measuring property. We present a program analysis technique for inferring and checking the units used within a program. The technique combines traditional Hindley-Milner-style type inference with the use of static single assignment (SSA) form to enable analysis of imperative programs.

In this paper we describe a framework that allows users of formal development environments (FDEs) to prove verification conditions using stand-alone theorem provers. Verification conditions from a given FDE are translated into an intermediate representation, then in turn translated into a form that is readable by the target theorem prover. In this paper we describe a systematic approach to the development of translators from the intermediate representation to a target theorem prover representation. The approach involves the development of a generic translator, which is instantiated for a particular target theorem prover by defining a variety of translation rules. In this paper we describe the different kinds of translation rules and illustrate their use with an example.

A number of industrial software development standards mandate that safety-critical software components be developed using formal methods, including formal verification. While formal development is supported by a number of formal development environments, verification of correctness properties is still a major bottleneck. Most formal development environments provide built-in facilities for discharging these correctness properties (so-called proof obligations). However these built-in tools are typically less mature and sophisticated than stand-alone theorem provers. FDEs would benefit from being able to use a variety of theorem provers to discharge proof obligations, where different provers can be selected for different problem domains.In this paper we describe a generic framework that supports the many-to-many connection of formal development environments and theorem provers. Before developing the framework we completed three case studies in order to reveal the main translation issues that need to be addressed. These translation issues were used as input to the requirements for our translation framework. We describe one of these case studies in detail in this paper. We then describe the framework and an Intermediate Modelling Language (IML), which is used to connect the FDEs to the theorem provers. The framework is supported by a collection of translators, both from FDEs (B and CARE) to the IML, and from the IML to theorem provers (Isabelle/HOL, Ergo and Otter).

In component-based software development (CBSD) programs are developed by combining reusable library components. Two of the main technical issues that need to be addressed are: locating suitable components in the library (retrieval); and adapting them to solve a specific problem. Intelligent retrieval techniques, based on matching formal specifications (so-called specification matching), have been developed to overcome some of the problems associated with traditional keyword-based retrieval techniques. Also approaches to semi-automating component adaptation have been proposed. These approaches are based on using component wrappers and component architectures for defining adaptation strategies. Such strategies can be represented by generic library templates that are parameterised over higher-order variables (therefore ensuring that they are applicable in a variety of situations). We would like to use existing specification matching techniques to locate suitable library adaptation templates. However, at present these two approaches are not compatible. This is because the current specification matching methods are based on matching first-order component specifications, whereas templates are specified using higher-order logic. In this paper we extend existing specification matching methods to handle higher-order library templates, with a focus on achieving the best possible tradeoff between automatability and precision/recall.

CARE provides a framework for construction and verification of programs, based around the recording of reusable design knowledge in parameterized templates. This paper shows how pattern-matching can be used to aid in the selection and application of design templates from a reusable library. A general framework is presented which is independent of the particular matching algorithm used at the level of mathematical expressions. A prototype has been built which supports a large subset of the Z mathematical language.

Component based software engineering (CBSE), can in principle lead to savings in the time and cost of software development, by encouraging software reuse. However the reality is that CBSE has not been widely adopted. From a technical perspective, the reason is largely due to the difficulty of locating suitable components in the library and adapting these components to meet the specific needs of the user.Formal approaches to retrieval - using formal notations for interface specification, and semantic based matching techniques - have been proposed as a solution to the retrieval problem. These approaches are aimed at overcoming the lack of precision and ambiguity associated with text-based component interfaces, requirements and retrieval techniques. However these approaches fail to adequately address the problem of component adaptation and composition.In this paper we describe how component adaptation and composition strategies can be defined using parameterised library templates. We define a variety of templates, including wrapper templates that adapt a single program component, and architecture templates that combine program components. We include definitions for sequential architectures, independent architectures and alternative architectures. These library templates are formally specified, so we are able to employ existing formal-based retrieval strategies to match problem specifications against library templates. We discuss how adaptation and composition can be semi-automated by the library templates defined in this paper in combination with existing retrieval strategies.

The use of formal verification to prove the correctness of software is increasingly being mandated by international standards for the development of safety critical systems. While formal development environments exist to assist in formal software development, formal verification is still an extremely difficult and time-consuming task, requiring expert skills not possessed by the typical software engineer. The authors propose a component-based development approach, where the aim is not so much to make savings in the cost of implementation, but instead to reduce the amount of verification that the software engineer needs to perform, as well as reducing the complexity of any remaining verification. This is achieved by providing reusable design templates that have been verified offline by an expert in mathematical logic and theorem proving. An important feature of the template language is the presence of higher-order parameters, which enable templates to be defined that are more widely applicable, thus giving better value for the one-off verification effort.

Industry is increasingly adopting software and system safety standards that mandate the use of hazard logs in the development and operation of safety critical systems. Hazard logs are used to record and track the results of hazard analysis and risk assessment throughout the lifecycle of the system. Even relatively simple systems give rise to large amounts of information and the need for tools to support the management of hazard logs.Def(Aust) 5679 is the Australian Department of Defence's standard for procurement of computer-based safety critical systems. Def(Aust) 5679 has particular requirements for the nature of the information that needs to be tracked in the hazard log, and on the way that levels of trust (LOT) and safety integrity levels (SIL) are assigned to safety requirements.This paper describes a prototype tool, called HazLog, that has been built on top of the DOORS tool in order to support the Def(Aust) 5679 hazard management process. DOORS is a requirements management tool which is already widely used within the Australian Department of Defence. Because many users will already be familiar with DOORS, learning to use the HazLog tool is expected to be easy. The tool helps users structure their hazard logs in the form required by Def(Aust) 5679, and helps them check the LOT and SIL rules from Def(Aust) 5679.

In this paper we demonstrate a refinement calculus for logic programs, which is a framework for developing logic programs from specifications. The paper is written in a tutorial-style, using a running example to illustrate how the refinement calculus is used to develop logic programs. The paper also presents an overview of some of the advanced features of the calculus, including the introduction of higher-order procedures and the refinement of abstract data types.

In this paper we describe a higher-order associative commutative pattern matching algorithm. We are motivated by the need for developing tool support for matching user requirements against library component interfaces, both specified using a formal language. In developing such tool support we aim for a maximum level of recall, while at the same time maintaining a reasonable level of automation and effciency.

A refinement calculus provides a method for transforming specifications to executable code, maintaining the correctness of the code with respect to its specification. In this paper we extend the refinement calculus for logic programs to include higher-order programming capabilities in specifications and programs, such as procedures as terms and lambda abstraction. We use a higher-order type and term system to describe programs, and provide a semantics for the higher-order language and refinement. The calculus is illustrated by refinement examples.

Object-orientation supports software reuse via features such as abstraction, information hiding, polymorphism, inheritance and redefinition. However, while libraries of classes do exist, one of the challenges that still remains is to locate suitable classes and adapt them to meet the specific requirements of the software developer. Traditional approaches to library retrieval are text-based; it is therefore difficult for the developer to express their requirements in a precise and unambiguous manner. A more promising approach is specification-based retrieval, where library component interfaces and requirements are expressed using a formal specification language. In this case retrieval is based on matching formal specifications. In this paper, we describe how existing approaches to specification matching can be extended to handle object-oriented components.

Retrieval of software components from a library relies on techniques for matching user requirements against library component interfaces. Here we introduce a number of techniques for matching formally specified, state-based modules. These techniques will form the basis for retrieval tool support. The techniques described are built on existing specification matching methods, based on individual functions, specified using pre- and post-conditions. We begin by defining a basic module matching technique, based on matching the individual units within a module. We consider variations of this technique that take into account two important features of modules: the visibility of module entities; and the use of state invariants. An advanced technique, based on data refinement and the use of coupling invariants, is also described.

Existing refinement calculi provide frameworks for the stepwise development of imperative programs from specifications. This paper presents a refinement calculus for deriving logic programs. The calculus contains a wide-spectrum logic programming language, including executable constructs such as sequential conjunction, disjunction, and existential quan-tification, as well as specification constructs such as general predicates, assumptions and universal quantification. A declarative semantics is defined for this wide-spectrum language based on executions. Executions are partial functions from states to states, where a state is represented as a set of bindings. The semantics is used to define the meaning of programs and specifications, including parameters and recursion. To complete the calculus , a notion of correctness-preserving refinement over programs in the wide-spectrum language is defined and refinement laws for developing programs are introduced. The refinement calculus is illustrated using example derivations and prototype tool support is discussed.