The public defense of Francisco Pozo's licentiate thesis in Computer Science and Engineering
Doctoral thesis and Licentiate seminars
Plats: Mälardalen University, room Gamma, Västerås.
The public defense of Francisco Pozo's licentiate thesis in Computer Science and Engineering will take place at Mälardalen University on April 6, 2017, at 14.00 PM in room Gamma, Västerås.
Title: “Synthesis of Extremely Large Time-Triggered Network Schedules”.
Serial number: 255.
The examining committee consists of Professor Zdenek Hanzalek, Czech Technical University; Senior Lecturer Radu Dobrin, MDH; Professor Mikael Sjödin, MDH. Among the members of the examining committee, Professor Zdenek Hanzalek has been appointed the faculty examiner. Reserve: Professor Björn Lisper, MDH.
For a long time now, computers have been able to coordinate their operation by exchanging information through communication networks. In some applications it is important not only that the information arrives to its intended destination, but also that the information arrives in time. For example, the airbags in a car are developed to be activated when an accident is about to happen, to avoid injury of driver and passengers. If the airbags are activated too late, they could cause harm by blowing up in the face of the persons they are supposed to save, and if they are inflated too soon they will not have any effect, nor prevent an injury as intended. The airbag is activated by a sensor that detects the impact and sends a signal over a communication network to the airbag controller. As one can understand from this example, the timing of the network communication is essential for the correctness of the airbag system.
The networks that are able to guarantee communication of these characteristics, are known as real-time networks. In such networks, messages are transmitted between computers in ways that are predictable, so the communication delays can be determined and specific timing requirements can be satisfied. A well established method to implement predictable network communication is with time-triggered frames. These frames are sent periodically, for example every 10ms, to satisfy the timing requirements of the applications. The periods and transmission instants of the frames can be determined offline, before the system is deployed, thus generating a so-called static schedule, which all frames must follow. We can think of this offline schedule as a train time table: a time-triggered frame is like a train that should travel from point A to point B, crossing several intermediate stations, and the time table (the schedule) specifies the departure time at each station. It is important that the train follows the time table, because it has been calculated to avoid collisions or delays caused by other trains, and it guarantees that the train arrives in time at its destination.
In this thesis, we focus on developing offline time-triggered schedules for large networks, with more than 1,000 computers and millions of frames. Generating schedules for such large systems is not simple. Our solution uses a two-steps approach. First, we divide the problem in several smaller problems that we call segments, representing different parts of a complete schedule; for example, frames to be sent during a specific second can be grouped within the same segment. In this manner, a large problem is divided into a number of smaller problems, which are usually easier to handle. This is a common approach in engineering to reduce complex problems, popularly known as “divide and conquer”. Second, we translate the scheduling problem into mathematical equations and use an available solver – a SMT solver – to obtain the timing of all the time-triggered frames in each small segment. Once the scheduling of all segments has been solved, we put them back together to build our final offline schedule, including the timing of all the time-triggered frames in the network. We have evaluated our solution in a large number of experiments, which show that our approach indeed can solve the complex scheduling we set out to solve, and which previously existing methods cannot handle.