My name is Ruben Jonk. Within the Electronic Systems research group of the Department of Electrical Engineering, I focus on the timing analysis of component-based software systems. In collaboration with ASML, we explore the modelling, analysis and verification of the timing- and performance-related behavior of complex systems such as TWINSCAN lithography machines. The goal is to add new tools to help the high-tech community guarantee quality during the development phase.
Timing analysis is performed on models constructed from execution traces. To ensure both the productivity and quality of these complex cyber-physical systems, strict and often repetitive timing requirements must be met. The research is developing techniques for the verification of these requirements and, in the case of a violation, root-cause analysis to identify its origin. If the response time of a control action violates its requirement, there may have been some delay early in the execution. Manually finding this delay and relating it to the violation is extremely time-consuming.
To execute this task automatically, we use an execution trace from a machine to construct a model that captures the timing of the functions executed. These models contain millions of events. This is too big to use directly, so the first step towards analyzing the data is extracting the pieces of the model which is directly related to the timing requirement. Once this model is prepared, the verification and root-cause analysis techniques can be applied.
The approach taken for verification is to encode the model and a timing requirement in a constraint satisfaction problem, utilizing the interactions between function executions to efficiently encode the verification question. Root-cause analysis, meanwhile, makes use of repetitive patterns to identify where delays occur. We then compute the impact of each of these delays on the overall timing of the execution.
Challenges remain, such as in finding a formalism that captures all of the relevant concepts found in component-based software systems and presenting them in a model upon which we can build scalable timing analysis techniques. Computing the impact of delays on the actual requirement is also difficult: delays in one part of the system may cause the critical path to change, making function executions that are usually not potential causes of the violation. This makes it tough to identify the correct function(s).
The first step in obtaining a model which is amenable to scalable timing analysis has now been finalised. This serves as the basis for the verification and root-cause analysis techniques. The timing verification research has yielded an MTL verification technique for message sequence charts which is able to verify relevant properties in the real world. A prototype of the root-cause analysis technique has also been shown to be able to accurately pinpoint the root causes of timing violations.
Currently, this technique is being incorporated into an in-house tool at ASML, showing that these techniques are scalable and effective in real use-cases. The ultimate result will be that developers can spend less time on identifying points of improvement and instead focus their efforts on the quality of high-tech systems. This will then improve the competitiveness of the high-tech industry as a whole.