Master Thesis Proposals
A Tool-Chain to Optimize Message Transmission in Vehicular NetworksContact person: Unmesh Bordoloi
Modern-day cars are essentially a complex embedded system. They are equipped with tens of ECUs (Electronic Control Units) that are basically embedded processors. These processors communicate with each other via some fieldbus like CAN, FlexRay, LIN etc. However, these field-buses do not offer enough bandwidth that can support the connection to the outside world or the ever increasing demand on by new applications running on the cars. This has led to emergence of new alternatives to in-vehicle communication networks. In this project, we will focus on one such next generation in-vehicle bus protocol.
The overall goal of the project is to implement an optimization framework for message packing. The optimization framework will be given to you. However, you will have the freedom and will be encouraged to propose changes to it and develop your own theories, if you wish.
The thesis will involve the following steps.
- Background study to gain a thorough understanding of the protocol.
- Implement the code in a language of your choice (such as Java/C/C++).
- Implement the code to build an experimental setup.
- Conduct experiments and document the results.
- Good knowledge of a high level programming language is mandatory.
Date Added: Jan 23, 2014
Systematically checking concurrent codeContact person: Ahmed Rezine
Powerful Multicore computers are now widespread and more and more concurrent code is being produced in order to get the most of these platforms. The problem is that designing, implementing, testing and debugging concurrent programs can be much more challenging and intricate than for sequential ones. Typically, concurrent programs allow for a huge number of possible interleavings between their concurrent sequential parts. Many bugs only appear in a fraction of these possible interleavings. Traditional testing approaches would only explore a tiny portion of these interleavings, leading to embarrassing hidden bugs mysteriously appearing at the customer site.
This situation resulted in an important amount of work that looked for effective ways to hunt such bugs and to validate the concurrent code. The available techniques range from monitoring tools that record certain aspects (accesses, race conditions, etc) of the program behavior during runtime to verification tools that aim at proving correctness of the programs. These approaches strike different balances between scalability and resulting guaranty. Monitoring tools handle large and realistic programs but explore only a tiny fraction of the possible interleavings, namely the one that happens to be executed when executing the program under test. Verification tools typically either generate too many false positives (or false alarms, spurious errors that do not exist in the code), or do not scale. A middle approach, which gained a lot of interest lately, monitors and tests concurrent programs by methodologically controlling the interleavings to be executed in order to boost the explored state space and to reproduce the bugs if any are found.
This thesis will be conducted in cooperation with Ericsson-Linkoping. The student(s) will start by gaining familiarity with a number of tools (with available source code) for the systematic testing of concurrent programs. An important part of the work will then be to collect a set of benchmarks of concurrent code, either from existing work, from open source applications, or from Ericsson applications. It is expected that an important part of the code will be in a language different from the one handled by the targeted tools. The benchmarks might therefore have to be rewritten to C# and Java. The thesis will leverage on the availability of the source code in order to modify the tools and to experiment with different heuristics, combining with user supplied hints or with other verification or static analysis techniques.
This 30 hp thesis can be carried by one or two Masters students that:
- Have very good programming skills (C#, Java)
- Are familiar with Visual Studio and with concurrent programming
- Took Courses in Logics and Discrete mathematics (optional but definitely a plus)
Date Added: Oct 01, 2012
A Tool-Chain to Analyze Ethernet Based Vehicular NetworksContact person: Unmesh Bordoloi
Modern-day cars are essentially a complex embedded system. They are equipped with tens of ECUs (Electronic Control Units) that are basically embedded processors. These processors communicate with each other via some fieldbus like CAN, FlexRay, LIN etc. However, these field-buses do not offer enough bandwidth that can support the connection to the outside world or the ever increasing demand on by new applications running on the cars. This has led to emergence of ethernet as a possible alternative to in-vehicle communication networks. While several variants of real-time ethernet have been proposed Time-Triggered Ethernet (TTEthernet) seems to be gaining traction and is being currently standardized by Society of Automotive Engineers.
The overall goal of the project is to develop a framework to optimize traffic flows on TTEthernet. This involves the following steps.
- Background study to gain a thorough understanding of TTEthernet MAC layer.
- Write code to develop a simulator of TTEthernet. This can be done from scratch or an existing TTEthernet simulator can be studied and then used, if it is useful.
- Final step to develop a framework that optimizes the traffic flows on the TTEthernet.
- Good knowledge of C, C++ is mandatory
- Experience with OMNeT++ or SystemC is beneficial
Date Added: May 10, 2012
Incremental Inductive Verification, Does It Work? Does It Scale?Contact person: Ahmed Rezine
Modern Multicore Computers are able to deliver a greater computing power for programs that can be run in parallel. This generated a great amount of work in coming up with ways to run programs in parallel. This project explores using Multicores to perform verification tasks.
As opposed to testing and simulation, verification aims at exploring all possible scenarios before validating a program or a design. Verification typically targets safety critical systems (transportation, medical instruments, etc). The price of the supplied guaranty is a complexity that often limits verification efforts to only target (relatively) small and simple computer systems. An important amount of work aims at coming up with clever verification techniques and algorithms that allow to handle larger and more complex systems.
Among the newly developed algorithms for the verification of computer systems, some are particularly well suited for performing parallel verification. This project will experiment possibilities of running them on a multicore platform.
More details are available here [pdf]
- Enjoy discrete mathematics and logics (related courses)
- Very good programming skills (for instance in c++)
- Good knowledge in scripting and in functional programming is a plus
Date Added: Mar 22, 2012
Updated on: Apr 28, 2014
Verification of Synchronization patterns of GPU programsContact person: Ahmed Rezine
More and more programs involve pieces of code
targeting GPU platforms. This is particularity true for programs
that allow for highly parallel computations. The problem is that
the sought after gain is only achieved with low level tuning at
threads level. This entails a degree of intricacy that
make writing such programs extremely error prone and difficult to
Testing and simulation based debugging are typically difficult in this context
due to the concurrent and intricate nature of these programs.
Promissing verification techniques already exist. This project is part of
an effort that aims at verifying the absence of certain synchronization
errors. For this, GPU programs need to be parsed and relevant
synchronization parts need to be isolated. This project
aims at isolating the synchronization patterns in typical GPU programs.
- Strong skills in compilers and good skills in OpenCl/CUDA programming.
- Good skills in Discrete mathematics is a plus.
Date Added: Mar 15, 2012
Analyzing the Quality of Service for Stream Processing ApplicationsContact person: Unmesh Bordoloi
Background and Project Description
The high-level goal of the Master's thesis is to provide a framework to analyze the quality of service (QoS) in stream processing applications on-board unmanned aerial vehicles (UAVs). An example application could be processing video streams to detect traffic violations for a UAV monitoring an urban area. Since the computational resources on a UAV are limited, there is a need to analyze how to best use these resources in order to guarantee the QoS of the given application. The framework should support both the analysis of the QoS of a particular stream processing application and design space exploration for classes of stream processing applications.
For more information, click here [pdf].
Date Added: Jun 21, 2011
Designing a Tool-Chain for Evaluating Automotive NetworksContact person: Unmesh Bordoloi
Background and Project Description
The proliferation of electronic devices has revolutionized the modern day car. However, automotive applications are safety-critical, and must perform under strict timing constraints. In this project, the goal is to build a tool to evaluate the timing properties of modern automotive networks.
FlexRay is now widely accepted as a next-generation automotive protocol and has been already deployed in few cars. The goal of this project is to build a simulator using a modeling language like SystemC.
There will be a possibility to extend the project further. This would be to compare the results of the simulator with measurements taken on a real setup where 4 Electronic Control Units are connected by the FlexRay bus.
The project can be assigned to one or two students.
Strong C++ skills are mandatory. Prior experience in SystemC is not required.
Date Added: May 12, 2011
Evaluating Design Tradeoffs of Customizable Processors in Multi-Core PlatformsContact person: Unmesh Bordoloi
Background and Project Description
Customizable processors are becoming increasingly popular because they provide the flexibility of tuning the instruction set according to the characteristics of the applications. Such processors can be run in multiple configurations where each configuration offers a tradeoff between performance and area costs. In multi-core platforms multiple customizable processors must configured in a synergistic fashion to strike the right balance between performance and area.
In this project, we will use the tool-chain provided by Tensilica for customizing processors. We will utilize their tool (Xpres) to evaluate the performance versus area tradeoffs in a multi-core platform. Standard benchmarks will be used for the experiments.
Programming in C.
Environment for the Verification of Embedded Systems using Petri nets and Timed AutomataContact Person: Petru Eles
Embedded systems are currently used in the most diverse contexts from automobiles and aeronautics to home appliances, medical equipment, multimedia and communication devices. Such systems are typically characterized by their dedicated function, real-time behavior, and high requirements on reliability and correctness. The interest in formal methods aiming at verifying embedded systems has increased recently due to the important role of correctness in such systems.
One of the ongoing research works at the Embedded Systems Lab (ESLAB) deals with the problem of formal verification of embedded systems. We use, as internal design representation, an extended timed Petri net model, called PRES+. PRES+ allows to capture relevant characteristics of this kind of systems, e.g. explicit timing information.
We have developed an approach that allows the verification of systems represented in PRES+. In order to make use of existing model checking tools, we translate the Petri net model into timed automata and use available tools like Uppaal.
The translation procedure from Petri nets to timed automata has been defined, but so far, it is done manually. The main task of the proposed project is the development of an environment for the automatic translation from PRES+ into time automata. Such a tool shall:
- Automatically translate PRES+ models into timed automata.
- Handle the format of existing tools (SimPRES--a simulator for PRES+--and Uppaal--a model checker for timed automata) such that the interaction between tools is possible.
The student developing this project should have a good knowledge of programming environments.
A extensible textual specification language for Petri Nets, Coloured Petri Nets, Timed Petri Nets, (Generalized) Stochastic Petri Nets, (symbolic) (tangible) reachability graphs, as well as for colour definitions, guards, arc expressions, time intervals, probability distributions has to be designed and a parser for it implemented.
As a demonstrator application, the student is supposed to model a multi-processor real-time scheduler using an earlier-deadline-first (EDF) scheduling policy where the task execution times are given as probability distributions and to generate the symbolic TRG for the coloured GSPN.
The student has to be characterized by seriousness, hard-working capacity, very solid experience in C++, OO design and programming, has to have good abstraction capabilities, and a deep dislike of patched, ad-hoc solutions. Some knowledge in compiler techniques may help.
System Modeling for Telecommunication ApplicationsContact person Petru Eles
Embedded systems are currently used in the most diverse contexts from automobiles and aeronautics to home appliances, medical equipment, multimedia and communication devices. Telecommunications are among the most important of all these application areas and industry is extremely interested in tools and methodologies connected to the development of digital systems for telecommunication equipment.
This project is part of an ongoing work in ESLAB with the objective to develop methodologies, algorithms and tools for the computer aided design of embedded systems. In order to proof the utility of our design environment we are currently working on modeling and synthesis of a typical component of modern telecommunication systems: an ATM (Asynchronous Transfer Mode) Network Terminal.
In the current version of our design environment we use VHDL as a system specification language. VHDL is a high-level, ADA-like language, widely used for the specification and simulation of systems consisting of hardware or hardware and software components. However, we are very interested in extending our system with new modern specification and modeling tools. Therefore experiments using new system specification methodologies are needed to offer insight into the advantages and drawbacks of different alternatives.
The main task for this project will be to specify and validate a model of the ATM network terminal. There are several modeling alternatives among which you may choose:
- An object oriented methodology based on the modeling language ROOM (Real Time Object Oriented Modeling).
- A modeling approach based on the ADEPT (Advanced Design Environment Prototype Tool) environment. ADEPT provides a set of predefined VHDL modules which can be used in order to specify more complex systems. It provides both a textual interface and a graphical design tool.
- If you are interested in functional programming, you may choose to specify the network terminal using a functional language, like Haskell.
The project can be assigned to one or two students.
A Front-End for a Hardware/Software Codesign SystemContact person Petru Eles
Embedded systems are currently used in the most diverse contexts from automobiles and aeronautics to home appliances, medical equipment, multimedia and communication devices. They perform a well defined control and/or data communication function as part of a certain equipment and their quality has a decisive influence on the characteristics of the respective product. That's why industry is extremely interested in tools and methodologies connected to the development of embedded systems.
There are several reasons why the design of such a system is an extremely challenging task:
- embedded systems are composed of both hardware and software components which interact in order to perform the given task
- they are distributed over several microprocessors and dedicated hardware structures
- embedded systems often function in safety critical contexts
- the systems have to fulfill real time constraints, as well as constraints concerning power consumption and cost
This project is part of an ongoing work in ESLAB with the objective to develop methodologies, algorithms and tools for the computer aided design of embedded systems.
In the design environment currently under development we use VHDL as a system specification language. VHDL is a high-level, ADA-like language widely used for the specification and simulation of systems consisting of hardware or hardware and software components. During the system design process, however, we use a graph based representation of the system, called the Conditional Process Graph (CPG). Process scheduling, performance estimation and hardware/software partitioning, for example, are performed on the CPG representation.
The main task for the project we are proposing here will be the design and implementation of a VHDL front-end to our design environment for embedded systems:
- The main theoretical aspects behind the specification language (VHDL) and the CPG representation, as well as the basics of system-level design have to be studied.
- The VHDL to CPG translator has to be designed and implemented. An existing VHDL compiler implemented by our group can be used as a starting point.
The project can be assigned to one or two students.