Student Project Proposals 2008

This page provides information on student projects proposed by Dr. Luettgen. Each project proposal is accompanied by a suggested reading list; for selecting a project, it is usually sufficient to have a quick glance at this referred work.

List of Proposed Student Projects

GL/01: Application of modern design tools to the analysis of mode confusion [MEng, MMath] Description.
The confusion of operating modes is a persisting problem in today's complex systems, for example in the "glass cockpits" of modern aircraft, and is the cause of many automation surprises. For example, lateral and vertical guidance modes have different meaning depending on the aircraft's flight angle. A number of approaches have been suggested by academics to investigate mode confusion potential during the design of such systems. Model checking is one such approach which has recently been integrated in industrial tools for designing and programming avionics software, such as Esterel Studio(tm) and SCADE(tm).

The aim of this project is to investigate how state-of-the-art design tools, in particular Esterel Studio and SCADE, can be used for the analysis of models of dependable systems regarding their mode confusion potential. The project involves developing state-machine models that capture the relevant system aspects required for such an analysis. These models can for example elaborate on existing models of parts of aircraft cockpits, such as mode logics of flight-guidance systems, and existing usage models. Of particular interest here is how the "features" of the human user of the system can be appropriately considered and what facets of mode-confusion problems may be analysed using the model-checking facilities of Esterel Studio and SCADE. In this way, the project will contribute in assessing industrial design environments for analysing mode confusion potential. The project shall be evaluated against related work by measuring the number and kinds of mode-confusion issues revealed by the chosen modelling approach.

Reading:
- G. Luettgen and V. Carreno. Analyzing mode confusion via model checking. In Theoretical and Practical Aspects of SPIN Model Checking (SPIN '99), vol. 1680 of LNCS, pp. 120-135, Springer-Verlag, 1999.
- K. Loer. Model-based automated analysis for dependable interactive systems, YCST-2003-06, Department of Computer Science, University of York, UK, 2003.
- A. Degani and A. Kirlik. Modes in human-automation interaction: Initial observations about a modelling approach. In Proc. of the IEEE International Conference on Systems, Man and Cybernetics, pp. 3443-3450, IEEE Computer Society Press, 1995.
- A. Degani and M. Heyman. Formal verification of human-automation interaction, Human Factors Journal, 2002.
- J. Rushby. Analyzing cockpit interfaces using formal methods. ENTCS, vol. 43, Elsevier Science Publishers, 2001.
GL/02: Using hard disk storage in automated verification [MScSWE] Description.
Modern automated verification algorithms often rely on the computation of the reachable state space of the system under consideration. Saturation is a state-of-the-art algorithm for computing reachable state spaces of systems defined via Petri nets, which has proved to be orders of magnitude more time- and memory-efficient than other state-space generators. Nevertheless, memory is still at a premium due to the complexity of today's digital systems and their high degree of concurrency. Most verification algorithms require states to be stored in main memory for quick access.

This project shall explore whether the unique features of Saturation permit one to efficiently store parts of the state space under computation on a hard disk. Heuristics shall be devised for deciding what portions of the state space should be swapped onto disk and when. An according prototypic algorithm shall be developed and implemented in C. In order for this algorithm not to interrupt the computation of the state space, it shall be designed as a separate thread under the Pthreads library. Benchmarking shall be carried out to compare the developed algorithm to running the standard Saturation algorithm on a machine equipped with very large main memory.

The ideal project student will have a good background in programming in C, as well as an interest in conducting experimental research.

Reading:
GL/03: Visualising the workings of historical mechanical calculators [CS, CS/M] Description.
Mechanical calculators, such as the Stepped Drum designed by Leibniz in 1674, have been fascinating people for several hundreds of years, until they have been ousted by electronic machines.

The aim of this project is to develop an interactive software for simulating and visualising the operation of some of these historical machines (to be chosen at the beginning of the project). This should help people in understanding and appreciating the various algorithms for implementing basic arithmetic operations, including addition and division. The produced software will be evaluated using reviewing and testing techniques.

The ideal project student will have an interest in arithmetic and calculators, as well as in computer graphics and computer simulation.

Reading:
- Arithmeum - Museum for historical mechanical calculating machines.
- History of mechanical calculators.
- P.E. Dunne. Mechanical calculators prior to the 19th century. Lecture notes, Department of Computer Science, University of Liverpool, 2000.
- E. Angel. Interactive computer graphics: A top-down approach with OpenGL. Addison Wesley, 2003.
GL/04: Implementing a model-theoretic semantics for Statecharts [MEng, MMath] Description.
Statecharts is a popular visual design notation for embedded systems, which extends state machines with concepts of concurrency, hierarchy, and priority. It is increasingly used by control engineers for developing embedded-systems software. One shortcoming of the operational semantics for Harel's original Statecharts variant is its lack of support for component-based design, validation and code generation. Recent research has suggested a new model-theoretic semantics supporting composability. This semantics structurally reads Statecharts as propositional formulas which are interpreted in a simple fragment of intuitionistic logic. Distinguished models of these formulas, which are called response models, then correspond to executable steps of the Statechart under consideration.

The aim of this project is to investigate how this model-theoretic semantics can best be implemented. One way would be to characterise response models as a set of constraints in propositional logic and to compute such models by utilising the computational power of modern SAT solvers. Another way would be to exploit the observation that response models are essentially the stable models studied in answer-set programming, which is a sub-discipline of logic programming.

The former implementation strategy entails the evaluation of available SAT packages and requires basic skills in the C programming language. The latter implementation strategy entails the evaluation of available logic programming languages and requires an understanding of mathematical logics. The project student shall explore which strategy is more promising, and conduct and evaluate an according prototypic implementation.

Reading:
- D. Harel. Statecharts: A visual formalism for complex systems. Science of Computer Programming, 8:231-274, 1987.
- A. Pnueli and M. Shalev. What is in a step: On the semantics of Statecharts. In Proc. of Theoretical Aspects of Computer Software, LNCS 526, pp. 244-264, Springer-Verlag, 1991.
- G. Luettgen and M. Mendler. Statecharts: From visual syntax to model-theoretic semantics. In Proc. of the Workshop on Integrating Diagrammatic and Formal Specification Techniques, pp. 615-621, Austrian Computer Society, 2001.
- M.W. Moskewicz et al. Chaff: Engineering an efficient SAT solver. In Proc. of the 38th Design Automation Conference, ACM Press, 2001.
- Answer set programming. Wikipedia entry, 2007.
GL/05: A framework for statically analysing ELF executables [MScSWE] Description.
Within a research project carried out in the Department, a prototypical tool for the static analysis of Linux executables is being developed. The research focuses on validating and verifying memory safety properties, such as invalid pointer dereferences, on automatically generated abstractions of Linux device drivers compiled for the IA-32 architecture. In a next step, the existing toolkit shall be extended in order to make it usable for generic binaries that are available in the Executable and Linkable Format (ELF) for various architectures.

The aim of this project is to re-design and re-implement the existing prototype. The resulting program or function library shall provide an easily extensible framework for statically analysing ELF binaries, including dynamic linking, interfaces for program abstraction, instrumentation and visualisation, as well as a protected environment for program simulation. Fulfilling this task will require a student to employ their knowledge in requirements engineering, software architecture and software implementation. The produced software will be evaluated using reviewing and testing techniques.

Students selecting to this research project should have a good knowledge of the UNIX or Linux operating system and excellent programming skills in C. The developed tool is likely to be made available to the open-source community in some form.

Reading:
- Description of the overall research project (PhD Qualifying Dissertation)
- Nielson et al. Principles of program analysis, 2nd edition. Springer-Verlag, 2005.
- Corbet et al. Linux device drivers. O'Reilly, 2005.
- IA-32. Wikipedia entry, 2007.
- Tool Interface Standard (TIS) Executable and Linking Format (ELF) specification version 1.2. TIS Committee, 1995.
GL/06: Visualising abstractions and traces on ELF executables [MScSWE] Description.
Within a research project carried out in the Department, a prototypical tool for the static analysis of Linux executables is being developed. The research focuses on validating and verifying memory safety properties, such as invalid pointer dereferences, on automatically generated abstractions of Linux device drivers compiled for the IA-32 architecture. In order to make the tool more understandable and usable for practitioners, a visualisation environment is needed. There are several different attributes of a program under consideration that would require visualisation. Examples include:
- Control flow and data flow;
- Comparison of the abstract program to the original program on assembly level and on source-code level;
- Error traces on assembly level and on source-code level;
- Code coverage.
The aim of this project is (a) to provide a conceptual design and a prototypical implementation of a tool generating easily understandable illustrations of the above attributes, and (b) to interface this tool to the existing verification framework. Fulfilling this task will require a student to employ their knowledge in requirements engineering, software architecture and software implementation. The produced software will be evaluated using reviewing and testing techniques.

Students selecting this research project should have a good knowledge of the UNIX or Linux operating system and good programming skills in C. The developed tool is likely to be made available to the open-source community in some form.

Reading:
- Description of the overall research project (PhD Qualifying Dissertation)
- Nielson et al. Principles of program analysis, 2nd edition. Springer-Verlag, 2005.
- Corbet et al. Linux device drivers. O'Reilly, 2005.
- IA-32. Wikipedia entry, 2007.
- Tool Interface Standard (TIS) Executable and Linking Format (ELF) specification version 1.2. TIS Committee, 1995.