Projects

The course PROJ-H-402 is managed by Dr. Mauro Birattari. Please read the description webpage to make sure you comply with the rules of the project: [WebPage].

This project has alredy been attributed !

The cours "INFO-F-102 - Fonctionnement des ordinateurs" is a course for BA1 students in Computer science. It provides an introduction to the basic functionning of a computer, for instance, what is a CPU, what is a memory, what are machine instructions, and so forth... The main support for the course is the book Structured computer organisation by Andrew Tanenbaum.

On of the main chapters of the course deals with the translation of machine instructions to micro-instructions, that are in turn executed internatlly to the CPU. To help the students grasping these rather abstract concepts, a data path simulator has been developped by A. Tanenbaum and is made available with the book. This simulator, however, is rather complex, covers many machine instructions that are not studied at the course, and has a GUI that is not really user friendly.

Another important topic of the course is the Arithmetic Logic Unit (ALU) of the CPU. There again, a simulator exists that can help students to better understand the concept, see the "Knob and Switch simulator" made by Dave Reed [WebSite].

The aim of this project is to realise an open-source, custom tailored and integrated version of these two simulators, that would fit the needs of the "INFO-F-102" course.

Required skills: Fair understanding of the concepts of DataPath and ALU, good programming skills. The emphasis will be put on the usability of the tool, being aimed at first year students. The candidate must be able to realise a very user friendly GUI for the application, which should be usable through a web browser.

More info: The candidates should contact Gilles Geeraerts, to further discuss the practical details.

Computer systems are nowadays often embedded into larger, critical systems, in order to control them (think about automatic underground, or airplane autopilot, for instance). In this case, the correcteness of the software must be ensured by all possible means, as software failure maight have tragic consequences

A classical technique to reason about the correctness of computer systems is first to devise formal (i.e. mathematical) models of both the system and the property that the system should enforce, and then to apply some systematic (i.e. algorithmic) tecnique to prove that the system respects the property, or to detect a bug. One such technique is known as model-checking, and the model used to specify the system is that of finite automata (as seen in the course about language theory and compiling).

Model-checking has proved successful, yet, the modeling of systems as finite state automata has its drawback: these models are quite weak and do not allow to reason about real-time (only the sequence of events can be recorder, but FA provide no means to measure the distance between two events, for instance). An extension to FA has been proposed by Alur, Fix and Henzinger, and is called Event clock automata. In this model, clocks are associated to events that occur in the system. These clocks record the last time each event has occured, and predict the next time one such event will occur. The model of event-clock automata is thus a natural way to reason about real-time in computer systems, and many analysis algorithms are known for them.

We have recently introduced a new datastructure, called the event zones that can be used to efficiently analyse event-clock automata, see: [Paper]. The aim of the project is to implement this datastructure under the form of a library (preferably in C) and to conduct a set of exepriments to assess its efficiency.

Required skills: Good mathematical and programming skills. Be ready to understand some amount of formalism.

More info: The candidates should contact Gilles Geeraerts, to further discuss the practical details.