Research Report - 2001
Software Engineering
Academic Staff
A/Prof David Carrington
A/Prof Roger Duke
A/Prof Ian Hayes
Dr Doug Goldson
Dr Anthony MacDonald
Dr Helen Purchase
Dr Peter Robinson
Dr Paul Strooper
Research Staff
Mr Richard Hagen (SVRC)
Dr David Hemer (SVRC)
Mrs Wendy Johnston (SVRC)
Research Students
Mr Robert Colvin
Mr Chris Hunter
Ms Soon-Kyeong Kim
Mr Brad Long
Mr Ian MacColl
Mr Jason McDonald
Mr Craig Mann
Ms Leesa Murray
Mr Jamie Shield
Mr Richard Thomas
Miss Janelle Pollard
Mr Philip Cook
Mr Stephen Grundon
Mr Geoff Foster
Mr Timothy Miller
Webpages
The software engineering research group involves multiple projects with the common theme of improving methods and tools for software development. Some of the research is done in conjunction with the Software Verification Research Centre (SVRC).
Specification-based Testing
Most of the information needed to determine test cases for software is contained in the software's specification. This project, which is funded by an ARC Large Grant, examines how to exploit this information in the context of testing object-oriented software. In particular, the project aims to develop methods and tools for testing object-oriented class implementations, using test cases and oracles generated from formal object-oriented specifications. The generated oracles will serve to verify the behaviour of the implementations when the test cases are executed. This project builds on previous work by Phil Stocks and David Carrington on the Test Template Framework for generating test cases and oracles from Z specifications. It also builds on work by Paul Strooper and Dan Hoffman on the ClassBench framework for testing collection classes. In 1999, the work has focussed on using the TinMan tool for test case management and on writing up the results of the project.
Daniel Hoffman, Paul Strooper and Lee White. Boundary Values and Automated Testing, Journal on Software Testing, Verification and Reliability, 1999.
I. MacColl and D. Carrington. Extending the Test Template Framework for specification-based testing of interactive systems. In Australasian Computer Science Conference (ACSC99), 1999.
L Murray, D Carrington, I MacColl and P Strooper. TinMan - A Test Derivation and Management Tool for Specification-based Class Testing. In Technology of Object- Oriented Languages & Systems TOOLS 32, 1999.
Refinement Calculus for Logic Programming
Two promising developments in addressing the problem of assuring software correctness are: refinement calculi, which allow the derivation of a program by a sequence of correctness preserving steps; and logic programming languages, which lead to a smaller conceptual gap between a problem and its solution when compared with procedural languages. This project aims to bring these two areas of research together by developing a refinement calculus for logic programming languages. Robert Colvin started a PhD project in 1997 on logic program refinement, emphasising data abstractions in the wide-spectrum language, data refinement and module refinement. For a specification to be complete the types of variables should be specified. Types can easily be represented in the wide-spectrum language by specification predicates. The role of types in program refinement has been investigated, and the concept has been extended to relationships between variables (invariants). In 1999 work continued on the semantics of logic program refinement. This work generalises the earlier semantics by modelling commands as partial mappings from a set of bindings to a subset of the bindings. For his Honours project, Chris Hunter worked on tool support for the refinement calculus in Ergo 5.
The project will receive Australian Research Council (ARC) Large Grant support for 1999 to 2001. David Hemer joined the project from August and Richard Hagen from October. David is working on Isabelle-based tool support, and Richard on code generation from tool-generated output. Ray Nickson from the Victoria University of Wellington, New Zealand, continues as an Associate Investigator on this project.
R. Colvin, I. J. Hayes and P. A. Strooper. Refining Logic Programs Using Types and Invariants, SVRC Tech Rpt 99-25, November 1999
R. Colvin, I. J. Hayes and P. A. Strooper. Refining Logic Programs Using Types, Australasian Computer Science Conf, ACSC, 2000.
Graphical User-Interface Builders
This project is concerned with user interface construction using both tools and formal (mathematical) specifications to achieve correctness. It is funded by an ARC small grant and is being performed in conjunction with the Software Verification Research Centre. The goals of this project are to:
Combine the practical benefits of graphical user interface builders with the rigorous analysis possible with mathematical specifications, and
Simplify the construction of formal specifications.
This project will use a reverse engineering approach by producing a formal specification as output from a modified user interface builder. The significant advantages of this approach are that it:
Combines the accessibility and tangibility of a user interface builder with the rigorous analysis and early problem correction of a formal specification,
Enables the construction of a formal specification by non-experts,
Overcomes the difficulty of finding an initial abstraction for a formal specification, and
Overcomes the very real problem of maintaining consistency between the (formal) specification and the corresponding implementation by changing the formal specification as the user interface is modified.
The project is constructing a formal model of user interface components and their composition, and will modify a user interface builder to output a formal specification based on this model.
Andrew Hussey and David Carrington, Platform Independent Graphical User Interface Design, Technical report 99-04, Software Verification Research Centre, 1999.
Andrew Hussey and David Carrington. Model-based Design of User-Interfaces using Object-Z. In Computer-Aided Design of User Interfaces II, 1999.
Ian MacColl and David Carrington. Specifying Interactive Systems in Object-Z and CSP. In Integrated Formal Methods (IFM99), 1999.
Automated Support for Verification and Validation of Control System Software
This project, which is funded by an ARC SPIRT (Strategic Partnerships with Industry - Research and Training) grant is a collaborative research project between Foxboro Australia and the Software Verification Research Centre (SVRC). The project started in June 1999, and involves Dr. Peter Lindsay and Leesa Murray from the SVRC, Dr. Paul Strooper from the Department of Information Technology and Electrical Engineering, and members of the Foxboro Firmware team. The project has three focus areas: fine-grained configuration management requirements traceability, and automated testing. It builds on recent research in the SVRC on fine-grained configuration management and automated testing, and will apply previous research results with the goal of enhancing product quality and productivity. The main research challenge is to make the three focus areas tie together, to provide effective support for managing change - at the level of individual requirements - right through the develop- ment, test and maintenance lifecycle. Work in 1999 has focused on evaluating current Foxboro practices in the three focus areas, and commencement of three pilot projects to trial process improvements in each of the areas.
Empirical evaluation of the usability of software engineering diagrams
This ARC-funded project will consider the usability of software engineering diagrams (specifically UML class and collaboration diagrams) from the point of view of human comprehension. Both the aesthetic layout of the diagrams, and their common notations will be empirically investigated. Preliminary work already completed includes empirical studies of the aesthetic layout of non-UML graph drawings, of the automatic graph layout algorithms that may be used for producing graph drawings, and of user preferences for the aesthetic layout of UML class and collaboration diagrams. Two experiments on UML class diagrams are currently being performed: the first considers the relative effectiveness (from a human comprehension point of view) of the differing syntactic notations found in UML texts, the other considers the relative effectiveness of aesthetic layout variation. Other semantic domains that could be considered as part of this project are entity-relationship diagrams, and social and transport networks. Peripheral issues associated with this project that are also being considered is the formal quantification of aesthetic presence by way of computational metrics, the perception of the aesthetics, and the distribution and correlation of these aesthetic measures.
Purchase, H.C., Effective information visualisation: a study of graph drawing aesthetics and algorithms, Interacting with Computers, 13(2), pp 477-506, 2000.
Purchase, H.C. and Allder, J-A. and Carrington, D., User preference of Graph Layout Aesthetics: a UML study, Proceedings of the Graph Drawing symposium, Marks, J. (ed), Lecture notes in Computer Science,Springer Verlag, 2000
Purchase, H.C. and Carrington, D. and Allder, J-A., Experimenting with aesthetics-based graph layout, Proceedings of the Theory and Application of Diagrams conference, Anderson, M. and Cheng, P. and Haarslev, V. (eds), Lecture notes in Artificial Intelligence 1889, Springer Verlag, 2000.
Assessing the usefulness of software aids
This project will empirically consider the usefulness of various learning and assistance aids that are provided with common software packages: online help, tutorials, agents, prompts, hints, printed documentation etc. Many users express dissatisfaction with the aids currently provided: this project will attempt to identify the specific problems with the current implementation of user support through empirical evaluation, and will propose design solutions. A preliminary study has investigated the usefulness of the theoretical research that prescribes how online help ought to be designed, and the design features that are implemented in existing applications (and which currently dictate users' expectations). This subsequent project will broaden the scope of this preliminary study, considering aids other than online help, and providing proposal for more effective user support.
Qu-Prolog
Qu-Prolog is an extended Prolog designed as an implementation language for interactive theorem provers. It includes built-in support for quantifiers, object variables and substitutions. Recently, Qu-Prolog has been further extended with multi-threading and very-high-level communication. This makes it an ideal prototyping language for applications such as intelligent agent systems (a research interest of Keith Clark) and for cooperative work environments for interactive theorem provers. Research on Qu-Prolog now focusses on these kinds of applications.
Phil Cook and Peter Robinson, Multithreading in an Interactive Theorem Prover, Technical Report 99-01, SVRC
Peter Robinson and Richard Hagen, Qu-Prolog 4.3 Reference Manual, Technical Report 99-03, SVRC
Keith Clark, Peter Robinson and Richard Hagen, Multi-Threading and Message Communication in Qu-Prolog, Technical Report 99-41, SVRC
Ergo
Ergo is an interactive theorem prover implemented in Qu-Prolog. The Ergo 5 prover is a generic sequent calculus prover and includes the Gumtree tactic language. Gumtree provides users with the ability to add a degree of automa- tion to proofs. Current research interests include the following.
An optimizing compiler for Gumtree.
Gumtree support for Window Inference.
Translation of theories and proofs from such provers as Ergo 4 and Isabelle to Ergo 5.
Cooperative work environments and background processing (see Qu-Prolog).
An Object-Oriented Refinement Calculus
The refinement calculus is a notation and set of rules developed to allow programs to be correctly derived from specifications. Object-orientation is a programming approach that is "based on an intuitive correspondence between a software simulation of a physical system and the physical system itself" [Abadi and Cardelli, A Theory of Objects]. Object calculi have been developed to provide a semantics for a range of object-oriented language features. Examples of object calculi are presented in Abadi and Cardelli's "A Theory of Objects." It is intended to base a refinement calculus on an object calculus. It is believed that this will result in a more natural, easier to use calculus than is currently available using existing encodings of objects in terms of functions. The aim is to produce a refinement calculus that is similar to Morgan/Back style refinement calculi for procedural refinement with additional techniques for object-oriented refinement.
Combining Graphical and Formal Specification Techniques
Formal specification techniques provide a systematic approach to produce a precise and analyzable software specification and to prove properties of the specification before implementation. However, the notations provided by most formal specification techniques are difficult to use and understand for most people. In contrast, graphical specification techniques produce specifications that are easy to use and understand. However, the lack of a precise semantic basis for the notations used in most graphical specification techniques limits the use of specifications for rigorous analysis. Also the simplicity of the notations has a limitation to express user requirements precisely. Studies to overcome these limitations have combined graphical specification techniques with formal specification techniques. These studies show that an integration approach is beneficial for both techniques. From the graphical techniques' point of view, formal specification techniques can be used to provide a precise semantic basis for their notation. Also it is possible to reason about graphical specifications by translating them to formal specifications. On the other hand, graphical specification techniques can be used with formal specification techniques in two different ways: for an initial conceptual model and as an alternative representation of the formal specification. Using diagrams for conceptual modelling can help the translation of real world problems to mathematical expressions. Also representing formal specifications using appropriate diagrams can improve understanding of the formal specifications for non- specialists. The goals of this project are:
to provide a precise semantic basis for graphical specification techniques, and
to define a set of graphical notations that can assist developing formal specifications and finally developing precise transformation rules between them.
This project also includes the development of a prototype tool to support automatic transformations.
Soon-Kyeong Kim and David Carrington, Formalizing the UML class diagram using Object-Z, UML'99
Soon-Kyeong Kim and David Carrington, Visualization of formal specifications, APSEC'99
<%-- end content --%><%@ include file="/include/footer.inc.jsp" %>