Internship | Visualization of Formal Verification Findings

System control applications involve many interacting functions running in parallel. Because of their complexity, it is a challenge to verify and validate system control application. In Machinaide, work is being done on model-based verification using formal methods. The focus has been on the development of user-friendly ways to (1) specify desired system properties (TNO, TU/e) and (2) verify these system properties using run-time verification (TNO) and model checking (TU/e). Run-time verification uses data of actual system executions to check whether desired properties are violated; model checking does the same for all possible system executions of a model of the system.

What is lacking is a user-friendly way to report findings of property violations. This is the topic of this assignment. Gantt charts can be used to visualize system behavior over time, typically showing system actions and their dependencies, but sometimes also discrete events and continuous signals. An example of a versatile Gantt chart visualization tool is ESI’s TRACE tool (see https://trace.esi.nl/). Gantt charts can show actual execution traces, but also counterexamples found by run-time verification and model checking.

In this assignment, a method is to be developed to augment execution traces with property-specific elements to (1) highlight violations of user-defined properties and (2) provide feedback to the user why the property was violated. The augmented execution trace is to be visualized as a Gantt chart. This execution trace augmentation involves relating the user-defined properties to the elements in the execution trace shown in the Gantt chart and highlighting the events leading to a property violation.

The assignment will (if circumstances allow) be carried out at TNO's Embedded Systems Innovation department at the High Tech Campus in Eindhoven in cooperation with Cordis SUITE and TU/e.

You are a Computer Science MSc student looking for a graduation assignment of 6-9 months. You have experience with model-driven software engineering and formal methods. You are positively challenged by a multi-disciplinary environment and are motivated to make formal verification methods accessible to an industrial audience.

You want to work on the precursor of your career; a work placement gives you an opportunity to take a good look at your prospective future employer. TNO goes a step further. It’s not just looking that interests us; you and your knowledge are essential to our innovation. That’s why we attach a great deal of value to your personal and professional development. You will, of course, be properly supervised during your work placement and be given the scope for you to get the best out of yourself. Naturally, we provide suitable work placement compensation.

At TNO, we innovate for a healthier, safer and more sustainable life. And for a strong economy. Since 1932, we have been making knowledge and technology available for the common good. We find each other in wonder and ingenuity. We are driven to push boundaries. There is all the space and support for your talent and ambition. You work with people who will challenge you: who inspire you and want to learn from you. Our state-of-the-art facilities are there to realize your vision. What you do at TNO matters: impact makes the difference. Because with every innovation you contribute to tomorrow’s world. Read more about TNO as an employer.