Master thesis assignments

Below you find a number of examples of potential assignments for a master thesis. In general there are far more assignments than can be listed here. It is always more fruitful to do a master thesis assignment that matches your interests. Therefore, I invite you to discuss your particular desires with me. Please note that it is wise to at least start with organizing your master thesis two months in advance. Students in Embedded Systems that first have to do a premaster assignment should contact me well before. Doing the premaster assignment beside other courses in part time is very well possible.

• The GITO (Generiek Integraal Tunnel Ontwerp) is a legal prescription how tunnels must look like. It prescribes an architecture of the software of Dutch road tunnels. The LTS (Landelijke TunnelStandaard) is a more detailed description of the software of tunnels. The software architectures in these do not coincide, leading to the question on what the natural structure of the software architecture in tunnels should be. Within Rijkswaterstaat this is currently a major discussion. It would be very worthwhile, as an input for this discussion, when a study is made to the form and shape of this software architecture. This could typically be done in the context of master thesis.
• The company Verum is one of the leading companies in providing tools for proven correct embedded software development. Using their tools many thousands of verified software components have been generated from model based description languages. This has been done at various companies such as ASML, Philips, Thermo-Fisscher, etc.
  One of the leading principles of their domain specification languages ASD and Dezyne is that controllers cannot base their decisions on data that is passed on through the controllers. Only restricted control data can be used for such a purpose. This helps in avoiding the state space explosion problem, and as such is of tremendous help in providing formally verified software.
  However, there are many cases where it is necessary that controllers base their decisions on data that is passed on. For instance at ASML, the wafer data contains information on which chuck it must be processed. Currently, users of ASD and Dezyne use laborious and ugly coding tricks to avoid this restriction.
  There are ideas at Verum on enabling the use of data to influence control decisions and still allow verifications. This assignment is intended to experiment with the proposed language extensions and investigate the influence on verifiability.
• At Philips in Best software is being redesigned continuously. Currently, this is done using model based design using the languages ASD and Dezyne developed at Verum. An interesting question is whether the newly designed software behaves exactly as the original software. It appears that model based testing is the excellent way to go ahead, where the old software is tested for compliance with the new models. The research question is to see whether this is viable by applying model based testing on a recently renewed piece of software. In particular, it is necessary to first make a model that reflects the software precisely, such that model based testing is possible. Your assigment is to make such a model. NEW: THERE IS NOW A CONCRETE SYSTEM TO BE REDESIGNED, NAMELY THE PEDALLING CONTROL OF AN XRAY SCANNER (February 2023).
• Control of wafersteppers at ASML is largely programmed using formal models written in the specification language ASD. One of the components takes care of scheduling the wafers such that they are properly and timely measured and projected upon. Sometimes the scheduling is disturbed because of an unexpected event, for instance because some component emits an unexpected error message. In such a case a rescheduling is necessary. The question is how to implement such a rescheduling such that rescheduling does satisfy a number of correctness properties. These properties have been proven for static scheduling, but it is not so clear how to do it for dynamic rescheduling. Persons involved at the side of ASML are Erik Kouters, Sander de Putter and Arthur Swaving. At the side of the TU/e are Thomas Neele and Jan Friso Groote.
• Modelling and analysing systems with hard real time constraints is hard. At ASML, where large parts of the software is currently designed using model driven design, there is a desire to be able to model and analyse systems where hard real time constraints play a role. Such requirements vary from input signals that must be processed within a particular time interval, robot arms that must have moved out of a critical region within a certain time, to wafers that must have been processed in time. There are various methods and tools available to do such analyses, but the question is whether such methods will be able to provide concrete insights in concrete real time systems. Your assignment will be to model concrete real time behaviour of concrete systems at ASML and see which methods are most effective in proving that those systems satisfy the required real time properties.
• Probabilistic behaviour is very interesting. This is the reason that the mCRL2 toolset supports probabilities. Checking probabilistic modal formulas is a challenging endeavour of which the basic techniques to do so are known. This master assignment is about making the available theory concrete in a tool. The basic steps are to define the basic modal property language and to define the translation towards PRESs, the probabilistic counterpart of PBESs. If there is sufficient time available, an algorithm to solve the PRESs is also very desirable.
• Plain probabilistic bisimulation is provided with a very efficient algorithms to calculate whether two states are equal. The situation is different when combined transitions are also allowed. If there are two nondeterministic transitions a.s and a.t, then a combined transition is a.(p s+(1-p) t), or in words, after the action a, state s can be reached with probablity p and state t can be reached with probability (1-p). Combined probabilistic bisimulation takes such combined transitions into account. The question is whether an efficient algorithm can be found and implemented that determines whether two states are combined probabilistically bisimilar.