Department of Information Technology

Topics for Master's theses in our group

This page lists potential Master's thesis topics related to the research done in our group. If you find any of the topics interesting and feel qualified to pursue such a thesis, be sure to get in touch with us. Also, if you have any thesis ideas of your own that you think would fit to our group, and want to be supervised, you are encouraged to contact us!

Craig interpolation for mixed-integer linear programs

Craig interpolation, a principle known to logicians since the 1950s, has recently emerged in formal verification as a practical approximation method. Its applications range from efficient image computations in SAT-based model checking to accelerating convergence of fixpoint calculations for infinite-state systems. In software verification, interpolation is applied to formulae encoding the transition relation of a model underlying a program. In order to support expressive programming languages, much effort has been invested in the design of algorithms that compute interpolants for formulae of various theories.

We have recently developed interpolation procedures for the theory of linear integer arithmetic, and some extensions thereof. Similarly, interpolation procedures for linear rational arithmetic have been known and used for several years. An open question, to be addressed in this thesis, is how formulae in the combined theory of integer and rational arithmetic (mixed-integer arithmetic) can be interpolated. Such procedures would be applicable, for instance, for the verification of timed, hybrid, or cyber-physical systems. The thesis should investigate the design of interpolating calculi, decision procedures, and practical implementations of such procedures for mixed-integer linear arithmetic.

Contact: Philipp Rümmer

Prerequisites: knowledge about linear algebra + optimisation, basic knowledge about logic and theorem proving

Finished or ongoing projects

Resource Sharing in Mixed-Criticality Real-Time Systems (Closed)

An increasing trend in embedded systems is to integrate components with different functionalities into a single hardware platform,
usually multi-cores chips. These different components are usually with different criticality. For example, in an aircraft, the fly-by-wire control function is with high criticality, since it guarantees the aircraft will not crash. On the other hand, the auto pilot function may be with relatively low criticality since an occasional failure in this function won't cause serious disasters. These different functionalities are usually subject to different certificate authorities or agencies, which have different focus and different assumptions to the system. For example, the fly-by-wire control function has to be certified by authorities like US Federal Aviation Authority or European Aviation Safety Agency. These authorities are very conservative, in the sense that they have very pessimistic assumptions on the system behavior (e.g. assuming a large program execution time). But these authorities only focus on the fly-by-wire control function to guarantee the aircraft does not crash, but do not care whether the pilot function works well. On the other hand, the overall system has to be certified by some other less conservative agencies (e.g. assuming a relatively smaller program execution time). The existing research on mixed-criticality real-time systems assumes that all the tasks are independent from each other, which rarely holds in realistic systems. The goal of this thesis is to study the design and analysis of resource sharing protocols for mixed-criticality real-time systems, especially the ones that are deployed on multi-core platforms.

Contact: Nan Guan

Prerequisites: basic knowledge about real-time systems

Performance Isolation for Mixed-Criticality Real-Time Systems on Multi-cores (Closed)

Multicore architectures offer a great computing power on a single hardware platform to host multiple applications, which may be of different criticality levels. We call such systems mixed-criticality systems. For example, consider a design of a mixed-criticality UAV control system on a dual-core processor, in which one core hosts the flight control application,
while another core hosts the sensing data processing application. A key requirement in this design is, the system designer need to analyze the timing behavior of the flight control application in the presence of the interference from the other application. The challenge is that modern multi-core architectures typically employ many fine-grained shared resources among different cores, like shared cache, shared bus, shared memory interface and so on, which are usually accessed in a rather random or speculative way to reduce the hardware implementation cost and improve the average-case throughput. So the interference analysis on these shared resources is extremely difficult.

In this project, we aim to design and implement flexible performance isolation mechanisms on COTS (commercial off-the-shelf) multi-core processors, to address the above challenges. The main idea is to utilize the build-in hardware support of the COTS processors to regulate the access to the shared resources from each core, in order to greatly simplify the timing analysis for mixed-criticality systems. The project participants will implement the software infrastructure (hardware driver, middleware and/or scheduling kernel) on embedded processors (e.g. PowerPC), as well as investigate the modeling and analysis techniques of the system timing behavior in the presence of the performance isolation mechanisms.

Contact: Nan Guan

Prerequisites: basic knowledge about real-time systems

Real-Time Extensions to Xen Hypervisor (Closed)

Virtualization has been a major factor in the general computing domain for decades. The hypervisor layer is becoming a default option in the software system architecture, especially for multi-core systems. Several open-source hypervisors like Xen and KVM have received rapidly increasing attention in both academia research and industry. Recently, there has been a significant demand of supporting real-time systems in virtualized environments, as system integration becomes an increasingly important challenge for complex real-time systems. Although research in real-time resource management like scheduling has been well integrated into operating system development, few work has been done to provide real-time supports in existing hypervisors. This thesis work aims at extending Xen (or KVM) to support various state-of-the-art hierarchical real-time scheduling techniques, with emphasis on the support of deploying real-time systems on multi-cores.

Contact: Nan Guan

Prerequisites: Basic knowledge about real-time systems and Linux kernel.

Predictability analysis of Intel Nehalem cache (Closed)

Hard real-time systems are subjected to strict timing constraints. Therefore, one needs to derive guarantees on the worst-case execution times (WCET) of programs. To derive safe and tight WCET bounds, one has to take into account the cache behavior, i.e., to decide whether each memory access of the program is a hit or a miss. Research in the past twenty years has accumulated successful techniques for caches with a particular replacement policy LRU. But very few results were obtained for other non-LRU replacement, like MRU, FIFO and PLRU. The reason is that these non-LRU replacement policies have more sophisticated behavior and thereby are considered to be hard to analyze (unpredictable). However, in reality very few commercial processors use LRU cache since its hardware implementation is expensive. Instead, most commercial processors choose non-LRU replacement which are cheap in hardware implementation, and thus are more cost friendly and power efficient. For example, the cache replacement in the Intel Nehalem architecture (Intel Core i5 & i7) is a non-LRU replacement policy, which we call MRU.

Recently, there has been some promising work by our group in analyzing MRU for WCET estimation, which indicates that MRU might be also a "predictable" replacement policy. However, there are still many fields subject to further study, include the analysis of data cache, multilevel cache and shared cache with MRU replacement. The goal of this thesis is to advance the analysis technique for MRU in one or several of the above fields. The resulting techniques should be implemented by extending the existing WCET analysis tools.

Contact: Nan Guan

Prerequisites: basic knowledge about real-time systems

Disclosing hardware secrets by automaton learning (Closed)

Modern microprocessors contain many features like caches and pipelines which make system analysis difficult from a hard real-time point of view. The only way to achieve precise analysis results is to have as much information as possible about the detailed inner workings of the processor. However, these details are often kept a secret by hardware vendors, under the premise of giving them a competitive advantage. One example is the cache replacement strategy. Many strategies like LRU, PLRU or MRU are known but may differ in details and CPU vendors are often secretive about the actual implementation. Often, details may only be obtained by signing non-disclosure agreements and/or paying large amounts of money, which is a problem for publication of research results.

Automata learning is a way do gain knowledge of the internal structure of a given black box system. The approach is to send queries to the system under consideration and observe its reactions. The topic of the thesis is to investigate and implement methods for applying learning algorithms to discover hardware secrets in microprocessors. As a first aspect, cache replacement strategies should be investigated: Given a processor with an unknown cache replacement strategy, different memory access patterns can be tried and the system behavior observed (execution time, performance counters, ...) in order to deduce which replacement policy is used. Part of the work is to develop a formal model (e.g. an automata model) that can be used to describe cache replacement strategies and is at the same time suited for learning algorithms.

Contact: Martin Stigge

Prerequisites: Basic knowledge about computer architecture; knowledge about automata learning is useful as well but can be acquired during the thesis work.

SAT-based detection of common defects in embedded software (Closed)

SAT-based bounded model checking techniques are able to efficiently and statically detect the possibility of runtime exceptions in low-level imperative code, e.g., due to erroneous use of pointers, incorrect use of APIs, or arithmetic overflows. Model checking can therefore find bugs at an early stage in software development and provide valuable feedback for developers. An overview of applications and case studies, derived using the bounded model checker CBMC, is given on this page.

This thesis is on the application of SAT-based techniques to detect common classes of software defects in embedded systems; the thesis work includes

  • describing and formalising the defects to be detected, which can be related both to the considered operating system, the considered micro-controller, and libraries. An example would be the (forbidden) termination of task functions in the FreeRTOS system.
  • implementation of a front-end that can handle the considered C dialect and frameworks
  • implementation of a translator that connects the front-end with existing model checking back-ends (e.g., CBMC), by encoding potential defects as logical assertions
  • evaluation using case studies and benchmarks.

Contact: Philipp Rümmer

Prerequisites: basic knowledge about compiler construction, verification, logic, and development of embedded software

Contract-based verification of non-functional properties for embedded systems

Our group has previously designed and developed contract-based verification tools for hierarchical architectural models of embedded systems, partly building on modelling paradigms developed at the University of Manchester. Besides functional properties (e.g., a system generates correct results), we have investigated how basic timing properties can be modelled and verified (e.g., a system generates correct results within a specified time). The topic of this thesis is to investigate how the existing modelling and verification methodology can be generalised to take other forms of non-functional properties into account, such as the allocation or consumption of resources other than time (memory, devices, bandwidth, etc.), or the possibility of hardware failures. To this end, a theory should be developed how such properties can be modelled in contracts, and be verified. The resulting methodology should be implemented by extending the existing contract-based verification tool.

Contact: Philipp Rümmer

Prerequisites: basic knowledge about compiler construction, verification, logic, and development of embedded software

Design of rewriting rules for floating-point expressions (closed)

Decision procedures and efficient SMT solvers are the cornerstone of today's verification and testing tools. One of the most interesting, yet most difficult theories to be handled in decision procedures is that of floating-point arithmetic; there are a number of ongoing research projects on advancing the state of the art. This thesis work is in the context of the Microsoft Research's SMT solver Z3, for which we are currently developing a plug-in for floating-point arithmetic. The goal of the thesis is to develop transformations and rewriting rules to improve the performance of the floating-point plug-in. Rewriting rules have proven to be extremely important to efficiently handle bit-vector (modular) arithmetic, say, 32-bit machine arithmetic, in SMT solvers. Due to the more intricate mathematical properties of floating-point arithmetic, it can be expected that corresponding rewriting rules for floating-point arithmetic are more difficult to formulate, but are expected to achieve similar advances in terms of reasoning performance.

Contact: Philipp Rümmer

Prerequisites: knowledge about logic and SAT/SMT solving

Updated  2018-10-03 10:58:48 by Philipp Rümmer.