Reviewing many usability evaluation methods (UEMs) can be challenging and so selecting the appropriate UEM for a particular context, such as software process descriptions (SPDs), is difficult. Consequently, systematic analysis of UEMs based on a reusable set of evaluation criteria and strategies is essential. In this paper, we employ the feature analysis - screening mode of the DESMET methodology to analyse a range of UEMs and to suggest several UEM candidates for evaluating the usability of SPD.

Abstract Design patterns are typically defined imprecisely using natural language descriptions with graphical annotations. It is also common to describe patterns using a concrete design example with implementation details. Several approaches have been proposed to describe design patterns abstractly based on role concepts. However, the notion of role differs in each approach. The behavioral aspects of patterns are not addressed in the role-based approaches. This paper presents a rigorous approach to describe design patterns based on role concepts. Adopting metamodeling and formalism, our work defines an innovative framework where generic pattern concepts based on roles are precisely defined as a formal role metamodel using Object-Z. Individual patterns are specified using these generic role concepts in terms of pattern role models. Temporal behaviors of patterns are also specified using Object-Z and integrated in the pattern role models. Patterns described this way are abstract, separating pattern realization information from the pattern description. They are also precise providing a rigorous foundation for reasoning about pattern properties. This paper also formalizes the properties that must be captured in a class model when a design pattern is deployed. These properties are defined generically in terms of role bindings from a pattern role model to a class model. They provide a precise basis for checking the validity of pattern utilisation in designs. Our work is supported by tools. We have developed an initial role metamodel using an existing modeling framework, Eclipse Modeling Framework (EMF) and have transformed the metamodel to Object-Z using model transformation techniques. Complex constraints are added to the transformed Object-Z model. More importantly, we implement the role metamodel. Using this implementation, pattern authors can develop an initial pattern role model in the same modeling framework and convert the initial model to Object-Z using our transformation rules. The transformed Object-Z model is then enhanced with behavioral features of the pattern. This tool support significantly improves the practicability of applying formalism to design patterns.

Statistical testing involves the testing of software by selecting test cases from a probability distribution that is intended to represent the software's operational usage. In this paper, we describe and evaluate a framework for statistical testing of software components that incorporates test case execution and output evaluation. An operational profile and a test oracle are essential for the statistical testing of software components because they are used for test case generation and output evaluation respectively. An operational profile is a set of input events and their associated probabilities of occurrence expected in actual operation. A test oracle is a mechanism that is used to check the results of test cases. We present four types of operational profiles and three types of test oracles, and empirically evaluate them using the framework by applying them to two software components. The results show that while simple operational profiles may be effective for some components, more sophisticated profiles are needed for others. For the components that we tested, the fault-detecting effectiveness of the test oracles was similar.

In this paper, we present a framework for pattern-based model evolution approaches in the MDA context. In the framework, users define patterns using a pattern modeling language that is designed to describe software design patterns, and they can use the patterns as rules to evolve their model. In the framework, design model evolution takes place via two steps. The first step is a binding process of selecting a pattern and defining where and how to apply the pattern in the model. The second step is an automatic model transformation that actually evolves the model according to the binding information and the pattern rule. The pattern modeling language is defined in terms of a MOF-based role metamodel, and implemented using an existing modeling framework, EMF, and incorporated as a plugin to the Eclipse modeling environment. The model evolution process is also implemented as an Eclipse plugin. With these two plugins, we provide an integrated framework where defining and validating patterns, and model evolution based on patterns can take place in a single modeling environment.

A test oracle is a mechanism that is used during testing to determine whether a software component behaves correctly or not. The test oracle problem is widely acknowledged in the software testing literature and many methods for test oracle development have been proposed. Most of these methods use specifications or other resources to develop test oracles. A passive test oracle checks the behaviour of the component, but does not reproduce this behaviour. In this paper, we present a technique that develops passive test oracles for components using their APIs. This simple technique can be applied to any software component that is accessed through an API. In an initial experiment, we found that test oracles developed this way were more effective at finding faults with a relatively small number of test cases than test oracles developed from a formal specification and developed as a parallel implementation.

We describe the "STSC" prototype tool that supports the statistical testing of software components. The tool supports a wide range of operational profiles and test oracles for test case generation and output evaluation. The tool also generates appropriate values for different types of input parameters of operations. STSC automatically generates a test driver from an operational profile. This test driver invokes a test oracle that is implemented as a behaviour-checking version of the implementation. To evaluate the flexibility and usability of the tool, it has been applied to several case studies using different types of operational profiles and test oracles.

Three important goals in describing software design patterns are: generality, precision, and understandability. To address these goals, this paper presents an integrated approach to specifying patterns using Object-Z and UML To achieve the generality goal, we adopt a role-based metamodeling approach to define patterns. With this approach, each pattern is defined as a pattern role model. To achieve precision, we formalize role concepts using Object-Z (a role metamodel) and use these concepts to define patterns (pattern role models). To achieve understandability, we represent the role metamodel and pattern role models visually using UML. Our pattern role models provide a precise basis for pattern-based model transformations or refactoring approaches.

An operational profile is a quantification of the expected use of a system. Determining an operational profile for software is a crucial and difficult part of software reliability assessment in general and it can be even more difficult for software components. This paper presents a systematic method for deriving an operational profile for software components. The method uses both actual usage data and intended usage assumptions to derive a usage structure, usage distribution and characteristics of parameters (including relationships between parameters). A usage structure represents the flow and interaction of operation calls. Statecharts are used to model the usage structures. A usage distribution represents probabilities of the operations. The method is illustrated on two Java classes but can be applied to any software component that is accessed through an application program interface (API).

This paper describes an ongoing collaboration between Boeing Australia Limited and the University of Queensland to develop and deliver an introductory course on software engineering for Boeing Australia. The aim of the course is to provide a common understanding for all Boeing Australia's engineering staff of the nature of software engineering and the practices used throughout Boeing Australia. It is meant as an introductory course that can be presented to people with varying backgrounds, such as recent software engineering graduates, systems engineers, quality assurance personnel, etc. The paper describes the structure and content of the course, and the evaluation techniques used to collect feedback from the participants and the corresponding results. The course has been well-received by the participants, but the feedback from the course has indicated a need for more advanced courses in specific areas.

Abstract The refinement calculus is a well-established theory for deriving program code from specifications. Recent research has extended the theory to handle timing requirements, as well as functional ones, and we have developed an interactive programming tool based on these extensions. Through a number of case studies completed using the tool, this paper explains how the tool helps the programmer by supporting the many forms of variables needed in the theory. These include simple state variables as in the untimed calculus, trace variables that model the evolution of properties over time, auxiliary variables that exist only to support formal reasoning, subroutine parameters, and variables shared between parallel processes.

This paper presents an integrated process model of use-case driven analysis and task analysis for developing interactive systems. In the process model, an analysis model is developed adopting the use-case driven approach using various UML diagrams; a use case model and its supporting scenarios are defined using the UML use case diagram and sequence diagrams respectively. Then a task model is developed projecting the analysis model from a user-centric view. Given the use case and sequence diagrams, we identify tasks, sub-tasks and user actions. A dialog model defining communication between the user and the system and also a structure for the user interface is derived from the task model. Finally, we identify user-interface components (called user-interface classes in our work) from the dialog model and these are mapped to classes in the analysis model. A user-interface prototype can be generated based on the user-interface classes and the dialogue model. In this way, we provide a process model that incorporates task analysis into the use-case driven approach for the development of interactive systems.

Describes our experience with teaching some elements of the Personal Software Process/sup SM/ as part of a second programming course. A distinctive feature was the class size of more than 360 students. The goals were to help students develop good software development habits early, and to encourage them to see software development as a systematic discipline rather than a trial-and-error activity. The results indicate partial success, with indicators for future improvement. We hope that other people will be able to build on our experience of teaching the concepts of PSP to large groups of students.

Presents a framework that integrates a graphical specification technique (UML) with a formal specification technique (Object-Z) to support requirements elicitation and analysis activities. Various UML diagrams are used to specify the system from different concerns during the early requirements elicitation and analysis stage. The information captured in the diagrams is used to develop a complete Object-Z specification. This paper presents a semantic translation from statechart diagrams to Object-Z specifications. Finally, based on information captured in sequence diagrams and use case diagrams, a functional model of the whole system is formally defined. The case study used in this paper is a real-time, interactive and embedded system: a light control system.

We define a translation from the User Action Notation (UAN) to the process algebra Communicating Sequential Processes (CSP). UAN is an informal notation, used for task modeling and design. Translating a UAN task description to CSP provides a base for rigorous development of an interactive system. The resulting CSP description is a suitable abstract starting point for development, as it describes externally visible behaviour with no mention of presented or underlying state. Our translation covers all UAN constructs except for waiting, interruptibility and true concurrency which cannot be expressed in interleaving, un-timed CSP. Our approach integrates task models, typically based on user-oriented concerns, into rigorous development which is typically system-oriented. It provides a bases for a framework for formal development of interactive systems.

This paper describes a method for specification-based class testing that incorporates test case generation, execution, and evaluation based on formal specifications. This work builds on previous achievements in the areas of specification-based testing and class testing by integrating the two within a single framework. The initial step of the method is to generate test templates for individual operations from a specification written in the Object-Z specification language. These test templates are combined to produce a finite state machine for the class that is used as the basis for test case execution using the ClassBench test execution framework. An oracle derived from the Object-Z specification is used to evaluate the outputs. The method is explained using a simple example and its application to a more substantial case study is also discussed. Keywords: specification-based testing, Object-Z, class testing, ClassBench, oracles 1

Formal specification techniques provide precise and analyzable software specifications. However, the formal notations provided by most formal specification techniques are not easy to use and understand for most people. Our approach counters this difficulty by visualizing formal specifications. In this paper, we use various diagrams to visualize a Z specification. In our work, both static and dynamic aspects of formal specifications, including complex constraints, are included in the visualization scope.

The paper contains a case study demonstrating a complete process for specification based class testing. The process starts with an abstract specification written in Object-Z and concludes by exercising an implementation with test cases and evaluating the results. The test cases are derived using the Test Template Framework for each individual operation. They are analysed to generate a finite state machine that can execute test sequences within the ClassBench framework. An oracle is also derived from the Object-Z specification. The case study demonstrates how a formal specification contributes to the development of practical tests that can be executed by a testing tool. It also shows how a test oracle can be derived from a specification and used by the same testing tool to evaluate test results.

Abstract. The refinement calculus for the development of programs from specifications is well suited to mechanised support. We review the requirements for tool support of refinement as gleaned from our experience with existing refinement tools, and report on the design and implementation of a new tool to support refinement based on these requirements. The main features of the new tool are close integration of refinement and proof in a single tool (the same mechanism is used for both), good management of the refinement context, an extensible theory base that allows the tool to be adapted to new application domains, and a flexible user interface.

The specification of a user interface describes user-perceivable functions and information structures in an implementation-independent way. In this paper, we specify part of the user interface for the UQ* (University of Queensland) editor. The UQ* editor is part of an integrated programming environment currently under development at the University of Queensland. We use the Object-Z formal specification language. We demonstrate that Object-Z can be useful for abstractly specifying user interfaces.

Test templates and a test template framework are introduced as useful concepts in specification-based testing. The framework can be defined using any model-based specification notation and used to derive tests from model-based specifications-in this paper, it is demonstrated using the Z notation. The framework formally defines test data sets and their relation to the operations in a specification and to other test data sets, providing structure to the testing process. Flexibility is preserved, so that many testing strategies can be used. Important application areas of the framework are discussed, including refinement of test data, regression testing, and test oracles.

A framework for specification-based testing is demonstrated on a symbol table case study, specified using the Z notation. Test derivation and structuring is discussed, as well as applications of the framework in deriving test oracles and aiding regressing testing during maintenance. Areas for further research and discussion are comparison of heuristics with regard to generated test suites and usability, formalising testing heuristics, and the discrepancy between functional testing and robustness testing.