The University of Adelaide Australia

Software Engineering Honours projects 2008

Bachelor of Engineering (Software Engineering) students who are admitted into the Honours stream are required to complete a 3-unit research project. At present this project will be done as part of the Level 4 course, COMP SCI 4002 Software Engineering Honours Project.

Below are some proposals for possible projects. Feel free to discuss other possible projects with me.

Pair programming and software quality

Level: SE Honours

Supervisor: David Hemer

Outline: Exponents of Agile Methods advocate the use of pair programming, where software engineers develop code (and other software artefacts) in pairs. Claims are made that pair programming can lead to improved software quality, with little nett effect on overall development time. This project will study the effect of pair programming on software code quality. A comparative study will be performed, using students from the Software Engineering and Project course. The study will look certain aspects of software quality (to be determined by the student), comparing groups using pair programming versus groups that do not employ pair programming.

A study of test-driven development

Level: SE Honours

Supervisor: David Hemer

Outline: In test-driven development test cases are written prior to code. The test cases form a contract for the code, in that the code is only deemed to be correct if it satisfies the test cases. The approach is incremental; as new test cases are added, representing perhaps new or more complex requirements, the code may need to be extended or refactored to satisfy the additional requirements. The approach forces the developer to think about testing early, and supports the development of a suite of regression tests.

The question to be answered in this project is whether or not test-driven development is beneficial, in terms of both the resulting code quality, and the amount of effort required to employ such techniques. The project will involve a comparative study using groups from the Software Engineering and Project course, with some groups employing test-driven development and other groups (the control groups) using traditional (or ad-hoc) development and testing approaches.

A comparison of risk identification strategies

Level: SE Honours

Supervisor: David Hemer

Outline: The identification, analysis and management of risks is essential to the success of any Software Engineering project. Without careful management of risks, Software Engineering projects can soon turn to disaster. Key to all of this is the identification of risks; if risks are not identified, they cannot be addressed.

In this project, the student will first do a study of existing risk identification strategies. Then after selecting a small number of these strategies, they will conduct of comparative study of the effectiveness of these strategies. Groups from the Software Engineering and Project course will be used to conduct the comparative study. The student will provide guidance to the groups on how to use a particular risk identification strategy. The results from the risk identification will be compared across various strategies, including against ad-hoc identification strategies.

Cost estimation in project planning

Level: SE Honours

Supervisor: David Hemer

Outline: Estimating the "cost" of a project is notoriously difficult, especially for novice Software Engineerings. Project planning and estimating the duration of tasks tends to be one of the most challenging aspects of the Software Engineering and Project course. From experience almost all groups are miles off the mark with their initial estimates, or simply do not include sufficient details. Some groups improve upon their time estimates as the course proceeds, while others groups continue with plans that are not particular useful and do not reflect the reality of their project.

The purpose of this course is to propose techniques that can be used by groups to improve their cost estimation skills and to study the comparative benefits of applying these techniques. The student will study a number of groups, split into at least three categories where groups within a particular category will all use the same cost estimation techniques. The categories should include: control groups (left to their own devices, and typically using ad-hoc approaches); groups conducting careful time logging, and using this information to refine cost estimates; and groups using more rigorous software cost estimation techniques (e.g. COCOMO) as proposed by the student. The student will compare the accuracy and level of detail that results from using these different techniques.

Honours/Masters projects 2007

Plug-in proof support for formal development environments

Level: Honours

Supervisor: David Hemer

Outline: Developing correct software is important. Faults in software may lead to financial loss, harm to the environment, litigation, or even loss of human life. In cases in which there is significant risk, software of high-integrity is required. This can be achieved through the use of formal methods, in particular formal specification and formal verification. Such methods have a strong grounding in mathematics and enable rigorous mathematical proofs to be constructed to establish certain properties, thus giving a greater level of assurance that software is behaving as intended.

However formal specification and verification are specialised domains, requiring skills beyond most software engineers. To assist software engineers to apply these methods, a number of formal development environments (FDEs), have been developed that provide methods and tool support for producing high-integrity software. Two key phases of the development process are: formally specifying the scope and behaviour of a software system, and ``refining'' this specification to an executable program. During both of these phases, properties, called verification conditions, may be generated that must be verified. The nature of these verification conditions means that it is unreasonable to expect humans to check them by hand; instead tool support is required.

While most FDEs provide built-in theorem-proving support for mechanically checking verification conditions, this support is usually far less mature than the support offered by stand-alone tools, such as interactive and automated theorem provers. In particular, stand-alone theorem provers offer a wider range of theories that have been used, validated and verified by a larger group of expert users. Also, stand-alone theorem provers usually offer better support for extending theories and/or adding user-defined theories in a mathematically sound manner. A great number of stand-alone theorem prover tools have been developed, and they support a wide variety of application domains.

The aim of this project is to develop a framework that supports many-to-many connection between FDEs and existing stand-alone theorem provers. This project will extend previous work in which we have defined an intermediate modelling language used to translate between FDEs and theorem provers, together with the development of a systematic approach to translating between the IML and theorem provers. The focus of this project will be developing a systematic approach to translating from FDEs to the IML, in which we would utilise and extend the Stratego tool chain, a collection of tools purpose built for program translation. The project will also extend the earlier work on IML to theorem prover translation. Finally the project will involve an evaluation of the overall approach.

Automating component adaptation and retrieval

Level: Honours/Masters

Supervisor: David Hemer

Outline: In component-based software engineering (CBSE) programs are not developed from scratch; instead they are developed by combining a number of pre-existing components. This can lead to savings in development time and cost. However it is not always easy to locate a suitable component, and when one is found it rarely meets the exact needs of the user, and thus needs to be adapted in some way. There has already been a fair amount of research focussed on the challenges of retrieving and adapting components. One interesting area is formal-based retrieval techniques, where search queries and library components, specified using formal mathematical notations, are matched. Such techniques overcome the problems, such as ambiguity and imprecision, associated with traditional text-based retrieval strategies. More recently attention has turned to developing adaptation strategies; of particular interest are formalised strategies that can be combined with the aforementioned retrieval techniques. The broad aim of this project is to combine these retrieval and adaptation techniques, so that given a user requirement (the search query), library components can be automatically located and adapted to satisfy the requirement. Possible projects include, but are not limited to:

  • applying the retrieval and adaptation techniques to "real" components (e.g. JavaBeans)
  • developing application specific search and adaptation strategies for automating CBSE.
  • improving the recall of the retrieval tool by developing relaxed matching techniques based on theorem proving technology.
The project will build on the supervisor's existing work.

Read A Formal Approach to Component Adaptation and Composition for more details.

Getting units of measurement correct in software

Level: Honours

Supervisor: David Hemer

Outline: Any program that measures quantities from its physical environment must compute using correct and consistent units of measurement. In many systems, particularly embedded control software, paying inadequate attention to units of measurement can result in catastrophe. An example of incorrect units leading to a costly failure is the Mars orbiter, which is believed to have burnt up in Mars atmosphere. The primary cause of this failure is believed to be inconsistent use of units for a critical measurement. One team used English units (feet), while the other used SI units (metres). As stated in the preliminary investigation:

"The problem here was not the error, it was the failure of NASA's systems engineering, and the checks and balances in our processes to detect the error. That's why we lost the spacecraft."

Unfortunately, current programming languages and tools provide little aid to the programmer attempting to establish or verify that correct units are being used. In earlier work, an analysis technique for inferring and checking the units used within a program has been developed. A prototype tool, which applies unit inference for programs written in C has been developed. However the tool uses a brute force approach, particularly in generating different combinations of units with associative commutative properties. Possible projects include, but are not limited to:

  • developing a more efficient algorithm, based on associative commutative (AC) unification will be designed and implemented. The implementation will be done in the Prolog language.
  • developing preprocessing tool that will massage Java programs into a form that is suitable for input into the unit inference tool. This project will apply parsing and compiler technology to map a Java program into Single Static Assignment (SSA) form, which can then be used as input into the unit inference tool.

David Hemer