Student Project Proposals 2007

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: Evaluating caching strategies for symbolic model checking [MScSWE] Description.
  

  Model Checking is a popular technology for verifying whether a finite-state machine satisfies a temporal-logic property, which is implemented in modern tools for embedded-systems design. Symbolic model-checking algorithms work on compact encodings of state spaces using decision diagrams as primary data structure, and have found application in verifying synchronous hardware circuits. Recent research co-conducted by the proposer of this project has advanced these algorithms for dealing with embedded software systems, such as computer protocols, which exhibit asynchronous rather than synchronous behaviour. Key to the run-time efficiency of these algorithms is the use of various caches in order to avoid computing the same information more than once. Given the limited space that is available for storing caches on computers, an important design decision of a caching strategy (such as "least recently used") is when cache entries shall be overwritten if memory becomes scarce.

  The aim of this project is to implement and evaluate various caching strategies for symbolic model-checking algorithms. The implementation needs to be carried out in the programming languages C and C++ and integrated in the verification tool SMART, of which the proposer's symbolic model-checking algorithm is a part. The performance evaluation shall be conducted experimentally by running the SMART model checker on a benchmark of asynchronous system models; such a benchmark already exists but may need extension. The performance measurements shall be carefully analysed and used to optimise the chosen caching strategies, e.g., by tuning the strategies' parameters.

  The ideal project student will have an interest in evaluating algorithms for automated verification, programming in the languages C and C++, and conducting experimental research.

  Reading:

  • G. Ciardo et al. SMART - Stochastic Model Checking Analyzer for Reliability and Timing.
  • G. Ciardo, G. Luettgen, and R. Siminiceanu. Saturation: An efficient iteration strategy for symbolic state-space generation. In Proc. of TACAS 2001, LNCS 2031, pp. 328-342, Springer-Verlag, 2001.
  • K. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.
• GL/02: Virtual Shared Memory (VSM) techniques 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.

  This project shall explore whether the large main memory available across a PC cluster can be utilised for computing state spaces. In order not to substantially change the sequential Saturation algorithm, the idea is to investigate whether Virtual/Distributed Shared Memory (VSM/DSM) toolkits, such as PVM, are suited to this task. VSM is a programming model that allows processors on a distributed-memory machine to be programmed as if they had shared memory. The project will consist of an evaluation of the C/C++ VSM/DSM libraries available and their suitability for parallelising Saturation's data structures. A prototypical implementation of the algorithm using the most suitable library shall then be undertaken. The studied and produced software will be evaluated using reviewing, testing and benchmarking techniques.

  The ideal project student will have an interest in C/C++ and parallel programming.

  Reading:

  • G. Ciardo, G. Luettgen, and R. Siminiceanu. Saturation: An efficient iteration strategy for symbolic state-space generation. In Proc. of TACAS 2001, LNCS 2031, pp. 328-342, Springer-Verlag, 2001.
  • PVM - Virtual Parallel Machine.
  • J. Kowalik, editor. PVM: Parallel Virtual Machine - A users' guide and tutorial for networked parallel computing. MIT Press, 1994.
  • Distributed shared memory. Wikipedia entry, 2007.
• GL/03: 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:

  • G. Ciardo, G. Luettgen, and R. Siminiceanu. Saturation: An efficient iteration strategy for symbolic state-space generation. In Proc. of TACAS 2001, LNCS 2031, pp. 328-342, Springer-Verlag, 2001.
  • M. Hammer and M. Weber. "To store or not to store" reloaded: Reclaiming memory on demand. In Proc. of FMICS 2006, LNCS, Springer-Verlag, 2007. In press.
  • POSIX threads. Wikipedia entry, 2007.
• GL/04: Implementing a model-theoretic semantics for Statecharts [MScSWE] 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.
• GL/07: Specifying and Validating a Heart Pacemaker in Z/Eves [MScSWE] Description.
  

  This student project will tackle one of the current pilot projects for the Grand Challenge in Verified Software - the heart pacemaker.

  The student project's aim is to formally model and validate parts of the pacemaker's specification using Z/Eves which is a freely available theorem prover. The starting point will be the informal specification of a previous generation pacemaker provided by McMaster University's Software Quality Research Laboratory, which is available at url http://www.cas.mcmaster.ca/sqrl/pacemaker.htm . This plain-English specification "defines the functions and operating characteristics, identifies the system environmental performance parameters, and characterizes anticipated uses of the system."

  The student project will subsume the following four work packages:

  • Identifying the scope of the formal model;
  • Modelling the identified parts of the pacemaker specification in Z;
  • Formalising desired properties of the pacemaker;
  • Verifying these properties using Z/Eves.

  This project is suitable for MSc SWE students with a strong interest in Formal Methods. It requires some experience in Z and the Z/Eves theorem prover, such as gained in the Autumn-term FMS module.