ITG Home
 
Current Courses
All Courses Brief
Thesis Suggestions
Research Projects
 
 
 
Impressum
 

Suggestions for Thesis Projects

This is a selection of thesis projects for BSc, MSc or Diploma students which are currently on offer from the Informatics Theory Group. If you are a committed student with mathematical interests who would like to join in foundational research, then the following projects might be of interest to you.

The default language for all projects is German. However, if you feel like it and you are sufficiently fluent, you may also do your project in English. Members of the Theory Group are happy to provide more detailed information about the projects listed below.

Note that this list, which reflects the research interests of the Theory Group, is meant to be an indication only of what sort of projects could be accommodated. You are invited to negotiate other (also programming-oriented) topics within the research areas with us.

 


Design and implementation of a graphical user interface for the ISABELLE theorem prover under windows

Isabelle is a generic (interactive) theorem prover designed around Natural Deduction.

Natural Deduction is an approach to Proof Theory that attempts to provide a formal model of logical reasoning as it “naturally”
occurs:

  1. we make (temporary) assumptions,
  2. we derive new formulae by applying basic rules and
  3. there is a mechanism for discharging assumption.

Since the logic’s syntax and the inference rules are specified declaratively, this allows single-step proof construction. Isabelle provides excellent notational support: new notations can be introduced, using normal mathematical symbols. Proofs can be written in a structured notation based upon traditional proof style, or more straightforwardly as sequences of commands. Definitions and proofs may include TeX source, from which Isabelle can automatically generate typeset documents. Isabelle is closely integrated with the Proof-General user interface, which eases the task of writing and maintaining proof scripts. Proof-General is a generic interface for proof assistants, based on the customizable text editor Emacs. It works with either XEmacs or GNU Emacs.

The motivation of this project is to employ Isabelle Theorem Prover for teaching natural deduction to first year students (MfI course). But, in order to do this a more user-friendly interface is required that allows the students to interact with the system in a way similar to that of the LPL software that is used currently in the course.

Reading

T. Nipkow, L. C. Pauslon, M. Wenzel: Isabelle/Hol: A Proof Assistant for Higher-order Logic. Springer 2002.

See: User Interfaces for Theorem Provers UITP 2005 (A Satellite Workshop of ETAPS 2005)

Design a visual system (Virtual Basketball Coach) that allows the user to edit and simulate game strategies

Develop a communication infrastructure (API) for the Lego Mindstorms infrared communication under the Esterel-Studio and SCADE environments.

Dataflow programming of (stream) flash animations using the functional-synchronous programming language Lucid Synchrone with clock types.

Dataflow programming of business processes modelling using SCADE

Investigate the use of graph algorithms for solving the causal analysis problem in synchronous programming languages

Conformance Testing based on Finite State Machine (FSM) Models

The ability to produce software systems that operate correctly has engaged the attention of researchers and practitioners since the recognition of the software crisis in the 1960's. Lamentably, four decades later, it is still an unresolved concern and the situation is not very promising. According to a study commissioned by the U.S. Department of Commerce, software faults are so prevalent and so detrimental that they cost the U.S. economy an estimated $59.9 billion per year (0.6% of the gross domestic product). The study also found that more than a third of these costs ($22.2 billion) could be eliminated by an improved testing infrastructure.

The basic objective of testing is to verify whether a concrete implementation is doing what it is expected to do. There are, however, a number of perspectives (formal and informal) that can be taken to deal with this and, consequently, there are also a variety of models and approaches related to the notion of testing. In conformance testing, this notion is articulated by means of a conformance relationship between computational objects. In particular, a concrete implementation is subject to experimentation (testing) for conformance to its specification. The precise formulation, which is generally assumed for this relationship, establishes that given a faithful abstract model of the implementation, this model implements (exhibits the same behaviour as) the specification. Evidently, conformance not only depends on the relationship that is assumed, but also depends on the models employed.

To obtain better and more systematic methods, conformance testing demands solid scientific basis and proper support tools. In the broadest sense, the motivation behind this research is to contribute to the challenging subject of conformance testing. The student project will implement an automated testing method based on well-known theoretical results.

The project work consists of the following steps:

  • The student will survey testing methods for FSM, in particular s(he) should investigate the Wp method for FSM.
  • The student should implement or use an existing graphical interface tool for input and editing FSM models. This tool must be able to verify the design-for-test conditions of the method (e.g. minimality of the machine).
  • The student should implement a tool to generate test cases (based on the Wp method) for testing FSM design (specification) against implementation.

Reading

T. S. Chow. Testing Software Design Modeled by Finite-State Machines, IEEE Transactions on Software Engineering, Vol. 4, No. 3, pp. 178-187, 1978.

S. Fujiwara, G. von Bochmann, F. Khendek, M. Amalou and A. Ghedamsi. Test Selection Based on Finite State Models, IEEE Transactions on Software Engineering, Vol. SE-17, No. 6, pp. 591-603, June, 1991.

M. Holcombe and F. Ipate. Correct Systems: Building a Business Process Solution, Springer-Verlag Series on Applied Computing, 1998.

F. Ipate. Complete deterministic stream X-machine testing, Formal Aspects of Computing, Vol. 16, pp. 374-386, 2004.

J. Aguado. Conformance Testing of Distributed Systems: An X-machine based Approach, PhD thesis, University of Sheffield, U.K., 2004.

Visual Games for SyncCharts

Synchronous Programming Languages (SPL) are being developed since the early 1980's (e.g. Esterel, Lustre, Statecharts). They are aimed to design reactive and embedded systems, supported by commercial tools (e.g. Esterel-Studio, Statemate) and popular among engineers (e.g. Airbus, Audi, Dassault Aviation, Eurocopter, General Motors, Texas Instruments) .

Esterel is originally textual, its visual front-end is the state-based synchronous model SyncCharts (C. André). They extend finite-states machines by:

  • Priority: Allowing different levels of precedence among transitions, resolving choices.
  • State hierarchy: Nesting of state-machines, decomposing system behaviour into sequential tasks.
  • Concurrency: Running several state-machines in parallel, decomposing system behaviour into parallel tasks.

Thus, SyncCharts may exhibit complex instantaneous behaviour. Its semantics is constructive and fully compatible with Esterel Semantics. Esterel programs can be mapped into finite two-player games in such a way that the signal statuses is reflected in the computation of winning strategies. The aim of this project is to produce a software tool that computes instantaneous reactions of SyncCharts (solving the co-contravariant fixed point problem) by means of a game-theoretic approach and to animate this game visually in the SyncChart.

The project work consists of the following steps:

  • The student will survey and study different semantics for SyncCharts, where particular attention should be given to the SyncCharts's game semantics.
  • The student should implement or use an existing graphical interface (e.g. Esterel-Studio) tool for input and editing SyncCharts.
  • The student should implement a tool to compute every instantaneous reaction of a SyncChart using for this the game semantics. Moreover, this tool should animate this computation in the form of games played in the graphical interface.

Reading

G. Berry. The Esterel v5 Language Primer, Centre de Mathématiques Appliquées. Ecole de Mines INRIA, 1999.

C. André. Computing SyncCharts Reactions. Electronic Notes in Theoretical Computer Science 88, 2003.

J. Aguado and M. Mendler. A-maze-ing Esterel, Synchronous Languages, Applications, and Programming (SLAP'03), Porto, Portugal, July 2003.

API for Esterel Estudio and Lego MindStorms

MindStorms is a popular environment for constructing and studying simple reactive systems. Reactive systems are characterised by their continuous interaction with their physical environment via sensors and actuators; real-world examples include cruise controllers for cars and industrial production cells. The Lego MindStorms kit essentially consists of a Lego computer brick to which one may connect actuators (e.g., motors, hydraulic elements) and sensors (e.g., touch sensors, light sensors, revolution sensors).

Esterel Studio is a commercial tool marketed by Esterel Technologies for designing and programming embedded reactive systems. Esterel Studio has been extended to facilitate programming for the MindStorms platform. This compiler generates C code which may then be cross-compiled to the LegOS operating system running on the Lego MindStorms brick. Unfortunately, this API does not offer any support regarding to the infrared port. The aim of this project is to develop a new tool (or extend the existing one) in order to support infrared communication between the Lego bricks.

The project work consists of the following steps:

  • The student will survey the various firmware developed for supporting C programming for the MindStorms.
  • The student will investigate and study the various API that have been developed for supporting Esterel/SynchChart programming for the MindStorms.
  • The student should implement or extend an existing API that allows the programmers to use the infrared port in their Esterel/SynchChart designs. This API should allow programmers to employ the other actuators and sensors as the current API developed by X. Fornari.

Reading

T. Baierlein, T. Murko, F. Piel and A. K. Wörrlein. A GCAS example developed using Esterel Studio and Lego MindStorms. (link)

C. Mauras and M. Richard. How to use synchronous languages to play with the Lego Mindstorms ? (link)

Compositional Timing Analysis

Exact timing analysis (ETA) is important in hardware for clock speed optimization and the design of asynchronous circuits, as well as in software for the validation of real-time embedded systems. However, the exponential complexity of data-dependent ETA still prevents realistic applications at large scale.  To cope with this problem and to be more efficient an abundance of approximative (i.e. inexact) timing analyses based on numerous heuristics have been proposed in the literature.  The three major techniques that are being applied are: (i) sophisticated efficient  data-encodings; (ii) Abstraction, i.e. decreasing the level of data-dependency of the timing; (iii) Compositional Methods, i.e. hierarchical decomposition and incremental analysis of complex systems.  The goal of this project is to investigate these techniques in a systematic fashion, develop a rigorous framework for classifying and relating the existing methods, and in doing so discover new ways forward to solve this important hardware and software validation problem.

The project may include some of the following sub-tasks:

  1. Produce a thorough review of the existing literature on timing analyses to identify the current state of the art and the limitations of existing approaches. Based on these findings a classification of existing timing analyses and their characteristic approximations is to be developed that pays particular attention to how the tradeoff between algorithmic efficiency on the one side and exactness and soundness on the other side is fixed in each case.
  2. Investigate and identify abstraction heuristics for making ETA more compositional and hence efficient. This involves the development and implementation of a new semantic model that supports abstraction and refinement.  This will make them especially useful for efficient compositional timing analyses. To prepare for these applications a coherent methodology of abstraction and refinement will be developed. This work would be based on and further develop the constructive timing models designed by the Verification and Testing group (see references below).
  3. The implementation of the timing models will be based on a compact data structure for representing functional and timing behaviour with variable degrees of data-dependency.  To this end a novel kind of Intensional Ordered Binary Decision Diagrams (IOBDDs) is to be developed and implemented that enrich the standard OBDDs, which only represent Boolean functions, with intensional  information for encoding timing delays.  The distinguishing feature of this new kind IOBDDs will be that they support various forms of data and timing abstraction.
  4. A comprehensive suite of typical hardware benchmarks (from the literature or own examples) is to be collated, and used to evaluate the techniques developed in the project.

Reading

K. C. Lam, R. K. Brayton: Timed Boolean Functions. A Unified Formalism for Exact Timing Analysis. Kluwer 1994.

P. C. McGeer, R. K. Brayton: Integrating Functional and Temporal Domains in Logic Design. Kluwer 1991.

M. Mendler: Timing Analysis of Combinational Circuits in Intuitionistic Propositional Logic. Formal Methods in System Design, Vol.17, No.1, pp.5-37, August 2000.

M. Mendler: Characterising Combinational Timing Analyses in Intuitionistic Modal Logic. The Logic Journal of the IGPL, Vol.8, No.6, pp.821-852, November 2000.

M.Mendler, M.Fairtlough: Ternary Simulation: A refinement of binary functions or an abstraction of real-time behaviour? Proceedings of the 3rd Workshop on Designing Correct Circuits (DCC96), M. Sheeran and S. Singh (eds.), Springer Electronic Workshops in Computing, 1996.

Z. Li and Y. Zhao and Y. Min and R. K. Brayton. Timed Binary Decision Diagrams. International Conferenc on Computer Design: VLSI in Computers and Processors (ICCD '97), pp. 352-359, IEEE, October 1997.

Shin-ichi Minato. Binary Decision Diagrams and Applications for VLSI CAD.  Kluwer 1996.

Model Checking and Incremental Code Generation for Statecharts

Statecharts is a popular visual design notation for embedded systems which extends state machines by the concepts of concurrency, hierarchy, and priority. This language is increasingly used by engineers in the areas of automotive, avionics design and becoming a serious competitor to other engineering design languages such as VHDL. Unfortunately, the standard operational semantics of most Statecharts variants that model globally-synchronous and locally-asynchronous systems, such as those occurring in these application areas, is mainly targeted at simulation, rather than for programming and validation. In particular, such semantics often do not possess the compositionality property. Thus, two Statecharts, although they have the same operational behaviour, may not be equivalent when composed with other Statecharts. Compositionality, however, is a necessary prerequisite for the composability of specifications, compositional verification, for incremental code-generation, hardware-software codesign, and hierarchical test input generation.

In this project a new compositional semantics of Statecharts is to be implemented which was recently developed by the Informatics Theory Group in collaboration with York University. Based on this new semantics the project will build a graphical design and automatic validation tool(set) for asynchronous Statecharts that supports, among other things, incremental code generation and compositional model-checking. The research component of the project consists in establishing the semantic foundations of code generation and compositional validation for the new semantics, as well as developing appropriate data-structures for efficiently coding the semantics of Statecharts programs.

Reading

D. Harel: Statecharts: A visual formalism for complex systems. Science of Computer Programming, Vol.8, pp.231-274, 1987.

A. Pnueli, M.Shalev: What is in a Step: On the semantics of Statecharts. Theoretical Aspects of Computer Software (TACS'91), Ito and Meyer (eds.), Springer LNCS 526, pp.244-264, 1991.

G. Luettgen, M. Mendler: The intuitionism behind Statecharts steps. ACM Transactions on Computational Logic, 2001. Also available as technical report, Institute for Computer Applications in Science and Engineering ICASE, NASA Langley Research Center,  Hampton, V.A., USA,  ICASE Report 2000-28, NASA/CR-2000-210302.

G. Luettgen, M. Mendler: Fully-abstract Statecharts Semantics via intuitionistic Kripke models. 27th Int'l Colloquium on Automata, Languages and Programming (ICALP'00), U. Montanari, J. Rolim, and E. Welzl (eds.), Springer LNCS 1853, pp.163--174, 2000.


Abstraction in Logic Programming

The execution of a constraint logic program (CLP) can be seen as consisting of two interrelated tasks: The search for a proof of the goal from the program assumptions (clauses), and the generation (and simplification) of constraints that are collected up on the way. Ordinary logic programming is an instance of this idea, where the constraints are unification constraints that arise from the propositional abstraction of program clauses (dropping all program terms). This principle can be generalised to provide a novel and rather general computational model for logic programming.

The goal of the project is to investigate and evaluate this new computational model. Specifically, the project will implement a flexible and general method of parameter abstraction and refinement for logic programming using ideas from Lax Logic, a constructive predicate logic developed by the Informatics Theory Group in collaboration with Sheffield University. This involves constructing a compiler and constraint solver for logic programs that separates the abstract part of a program, as specified by the user, from the remaining concrete part.  The abstract part can then be executed as a standard logic program, while the concrete part is dealt with by constraint solving.  In this way the abstract program serves as a  high-level guide that explores the search space to approximate a possible solution, while the constraint solving, which may lag behind, fills in the remaining computational details. In this way abstractions can be used to generate completely new search strategies for logic program execution, orthogonal to the standard breadth-first vs. depth-first and forward vs backward distinction.  Through concrete case studies the project will evaluate the potential benefits of such new execution strategies, e.g. by carrying over into Lax Logic some of the proof planning and abstraction techniques found in the Artificial Intelligence literature.

As the implementation language we use Eclipse, a constraint logic programming language developed at Imperial College. To study the effect of different abstractions and the tightness of the coupling between abstract execution and constraint solving systematic experiments with concrete programs should be undertaken.

Reading

M.Fairtlough, M.Mendler, M.Walton: First-order Lax Logic as a Framework for Constraint Logic Programming, Technical Report, University of Passau, MIP-9714, November 1997.

M. Walton: First-order Lax Logic: A Framework for Abstraction Constraints and Refinement. Ph.D.  Thesis,Department of Computer Science,  University of Sheffield, November 1998

F. Giunchilglia, T. Walsh: A Theory of Abstraction. Artificial Intelligence, 57:323-389, 1992.

D. A. Plaisted: Theorem proving with abstraction. Artificial Intelligence, 16:47-108, 1981.

Timing Analysis of Asynchronous Systems

Timing analysis is an important part of asynchronous system design. This has two reasons. Firstly, asynchronous systems are built (among other things) to be faster than conventional synchronous ones, and timing analysis is used to measure the performance gain. Secondly, in the absence of a synchronizing clock, the correct functioning depends crucially on the validation of timing constraints on the relative computation speed of the system's components.

The goal of the project is to implement a collection of automatic timing analyses for asynchronous systems based on simple timing models. This will be done in two ways: (i) By "symbolic" manipulation building a constraint solver for interval constraints (e.g. in Eclipse, a constraint logic programming language). (ii) By implementing a program package for Timed BDDs, i.e. Binary decision diagrams extended by quantitative timing information. This is the "numeric" method. Both the symbolic and the numeric methods will then be evaluated and compared by way of systematic benchmarks.

Binary decision diagrams, BDDs, are a specialised data structure to encode Boolean functions efficiently. BDDs have recently been used very successfully in automatic formal verification systems such as model-checkers to implement NP-complete problems by algorithms with only average case polynomial complexity. The project involves a systematic literature survey on the theory and applications of BDDs, with the aim of producing a classification of the existing different varieties of Numeric BDDs, in terms of their functionality and applications.

Reading

  • Z. Li and Y. Zhao and Y. Min and R. K. Brayton. Timed Binary Decision Diagrams,. International Conference on Computer Design: VLSI in Computers and Processors (ICCD '97), pp. 352-359, IEEE, October 1997.
  • Shin-ichi Minato. Binary Decision Diagrams and Applications for VLSI CAD.  Kluwer 1996.

Semantics Framework for Object-oriented Programming Languages

Centaur is a generic interactive environment generator, that, when given the formal specification of a programming language (syntax and semantics), produces a language-specific environment. With the help of Centaur one can develop structure editors, debuggers, interpreters, and various translators for manipulating programs of the specified language. The project's objective is to adapt and develop Centaur or a similar system (like those currently developed at INRIA, Sophia-Antipolis) further and to build a language environment for a simple Java-like object-oriented programming language (the Language POPPY developed at Sheffield University) that supports program animation and type checking of advanced mechanisms of polymorphism and inheritance.

 

Simulator for the Process Algebra CSA

Description

CSA is an algebraic process language that extends Milner's Calculus of Communicating Systems by multiple clocks. The language is used for the abstract semantic modelling and verification of globally asynchronous, locally synchronous distributed systems. Its semantics is based on labelled transition systems with clock and action labels. In this project first a semantic compiler for CSA is to be developed that generates finite transition systems for regular CSA processes. Based on these transition systems the goal is to build an interactive user-interface to animate CSA processes.

Resources

  North Carolina Workbench, implemented on Unix workstation or PC

Reading
  • R. Cleaveland, G. Luettgen, M. Mendler: An algebraic theory of multiple clocks. In: Proc. Int'l Conf. on Concurrency Theory CONCUR'97, LNCS 1243, Springer 1997.

Multi-Stage Programming

Description

Multi-stage programming is a method for improving the performance of programs through the introduction of controlled program specialisation. Multi-stage languages provide generic constructs for building, combining and executing code fragments, generalising the distinction between compile-time and run-time, and static versus dynamic parameters to multiple levels. The goal of the project is to implement a simple multi-stage programming language that combines open and closed code, binding time analysis and staged computation. The implementation will be done using the interactive environment generator Centaur or a similar such tool.

Reading

  • R. Davies: A temporal-logic approach to binding-time analysis. In 11th LICS, July 1996, IEEE Computer Society Press
  • R. Davies and F. Pfenning: A modal analysis of staged computation. In 23rd POPL, St.Petersburg Beach, Florida, January 1996
  • W. Taha: Multi-Stage Programming: Its Theory and Applications. Ph.D. Thesis, Oregon Graduate Institute of Science and Technology, June 1999.

Simulator for Asynchronous Systems

Asynchronous circuits are a special hardware design technique that may be seen as an implementation of the data-flow principle, by which a computation is controlled by the availability of its input data rather than by a centralised processor clock. Since all data are computed in a parallel and distributed fashion asynchronous circuits are potentially faster and consume less power than conventional synchronous circuits. Just as synchronous circuits are built from primitive gates such as INVERTOR, NAND, and NOR gates, asynchronous circuits are composed of a small number of primitive building blocks, called FORK, MERGE, TOGGLE, SELECT, etc. However, due to the intricacies of parallel and overlapping computation phases the design of such systems is rather more complex than that of synchronous ones. To support the conceptualization of asynchronous operation a window-based simulator for the construction and simulation of asynchronous circuits is to be built in this project.

Reading

  • I.E. Sutherland: Micropipelines. Turing Award Lecture, Communications of the ACM, Vol.32, No.6, June 1989.

Abstraction and Refinement in Higher-Order Logic

Abstraction is a well-known and successful heuristic technique for search problems in planning and theorem proving applications. Rather than proving a complex formula directly, one abstracts away certain parts of the original problem statement and first attempts to solve the simplified problem. The solution to the simplified problem then can often be used as a guide-line to derive a detailed solution to the original problem efficiently. The goal of this project is to implement a window-based user-interface to animate a very general abstraction technique that has been developed by the Informatics Theory Group for Higher-order Lax Logic. The objective of the implementation is to illustrate, by way of a web-based interactive application, the syntactic process of abstraction and refinement of predicate logic formulas. No prior knowledge of logic and theorem-proving is required, as this project is mainly about web interface design. However, for preparation of this project, some reading into the typed lambda-calculus in needed.

Automatic Generation of Dungeons for Computer Games

The generation of content for a games title is expensive and time consuming. For certain game genres, automatic content generation algorithms are possible which drastically decrease the development time (currently 1 team year for 40 game hours)  and permit the necessary variations of a successful game in follow-up editions. Automatic content generation may take place not only at design-time by the developers but also at run-time by the users. This enables each player to have an entirely new experience of the game each time it is played, without ever being able to identify the `story line'. This projects will explore and implement a technique for automatic content generation for dungeon games (such as Doom) based on graph grammars. An important part of the project is to develop ideas for assessing the "fun-value" of the generated dungeons.

Graphical Editor and Typechecker for Component-based Signal-Processing

Typechecking is one of the most successful static validation methods that have found their way into industrial practice. Typechecking, which nowadays is an integral part of many high-level programming languages helps to detect and eliminate many sources for run-time errors already at compile-time, and thus yields a significant increase in programming efficiency. This has been demonstrated impressively e.g. in functional and object-oriented languages. The project explores this idea for a domain-specific programming system.

The goal of this project is to implement a front-end including a graphical editor (GUI) and type-checker for ICONNECT, a component-based programming system tailored to signal-processing and control applications. The tool is quite similar to tools from the Matlab-Simulink, Ptolemy, HP-vee, etc, family. Besides the type-checker the project only involves building a simple user interface for dragging and dropping signal-processing components and for connecting them to signal graphs. It does not require programming any run-time system for executing the signal graphs. The GUI and its components will be based on the existing programming system ICONNECT, which already has some rudimentary type-checking facilities that can be used as a good starting point.