Research Report - Software Engineering
The software engineering research group involves multiple projects with the common theme of improving methods and tools for software development. Some of this research is done in conjunction with the Software Verification Research Centre (SVRC). The following is a list of current projects and project themes.
Specification-based testing techniques identify test cases for software products from information contained in the software's specification. Several projects are investigating specification-based testing and have developed methods and tools for testing object-oriented class implementations, using test cases and oracles generated from formal object-oriented specifications.
A collaborative research project with Foxboro Australia is exploring automated support for verification and validation of control system software. The project has three focus areas: fine-grained configuration management, requirements traceability, and automated testing.
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 and for cooperative work environments for interactive theorem provers.
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 automation to proofs.
An object-oriented refinement calculus is being developed to allow programs to be derived from specifications. The refinement calculus is based on an object calculus to create a calculus that is easier to use than those currently available by encoding objects in terms of functions.
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. Another project brings these two areas of research together in a refinement calculus for logic programming languages, emphasising data abstractions in a wide-spectrum language, data refinement and module refinement.
An ARC-funded project is investigating 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 are being empirically investigated.
Other projects seek to combine graphical and formal specification techniques with the goal of achieving the benefits of both while minimising their limitations. Formal specification techniques provide systematic approaches that produce a precise software specification whose properties can be proved before implementation. However, formal specification notations are difficult to use and understand for many people. In contrast, graphical specification techniques produce specifications that are easier to use and understand but they lack a precise semantic basis, which limits rigorous analysis. Recent collaboration with the University of Waikato, New Zealand has led to some promising results in this area, where two formal methods have been integrated with a graphical language for specifying control systems.
Development of ‘Bahasa’, an open platform for reengineering tool development based on Java, continues as an alternative to the proprietary environment used in former industry R&D projects. Apparently unrelated work on expunging data from higher-order functional programming offers a possible ‘reengineering’ connection as a canonical language for description of software designs as recovered by reverse-engineering tools. Other continuing reengineering work concerns development of binary translation and decompilation tools, based e.g. on UQBT (UQ Binary Translator) which has seen further development at SUN Microsystems.
Software development involves the preparation and verification of many documents, and a well-integrated set of document manipulation tools with an appropriate user interface is vital to success. The generic UQ* document environment extends the concept of documents as syntactic structures with intra and inter-document relations that can be used to represent a wide variety of semantic and process-related aspects of software (complex documents). Research currently focuses on several aspects of complex document support:
1. presentation and understanding of complex documents, including modelling requirements tracing, and
2. fine-grained configuration management of complex documents.
Incremental compilation in language-based environments is a project developing a cohesive set of incremental algorithms that perform many of the tasks traditionally associated with batch compilers. These techniques are being developed with the user's model of program development in mind; in particular they must accommodate modeless interaction, be tolerant of syntactically erroneous and incomplete program fragments, and construct syntactic and semantic representations that are appropriate for user interrogation. Furthermore, each tool in the incremental compilation process need not share the same granularity of evaluation, or frequency of execution. Hence flexible tool integration is required. This is achieved by using shared syntactic and semantic representations, combined with a mechanism to allow each tool to have its own view of the structure of such representations.
To make computers easier to use, computing tasks must be more sensitive to our needs and the context where they are. However as users, computers, data and processes becoming increasingly mobile and the diversity of interacting devices increases, pervasive computations are difficult to predict and to understand due to the complexity and the fluidity of the surrounding contexts. We are building a programming environment that adequately supports pervasive computation on a solid theoretical basis (Ambient Calculus). The programming language will allow us to succinctly describe the interaction between mobile code and environments (context) at destination nodes.
Associated Staff
Prof Paul Bailes
Dr Jay Burmeister
A/Prof David Carrington
Ms Mandy Downing
A/Prof Roger Duke
Dr Doug Goldson
Prof Ian Hayes
Prof Simon Kaplan
Prof Peter Lindsay
Dr Anthony MacDonald
Dr Peter Robinson
Dr Paul Strooper
Dr Stephen Viller
Dr Peta Wyeth
A/Prof John Yesberg
Mr Jihan Zhu
<%@ include file="/include/footer.inc.jsp" %>