Internship | Visualization of Formal Verification Findings
About this position
The Machinaide project is a cooperation of TNO, Cordis SUITE, TU/e, Additive Industries, Lely Industries and KE-works. Machinaide aims at the development of digital twins for small- and medium-sized companies; Machinaide specifically targets digital twins of system control applications. Basis of Machinaide’s digital twins is the Cordis SUITE low-code platform, a platform for specification and code generation for system control. Cordis SUITE is being extended with data collection and visualization functionality developed in Machinaide.
What will be your role?
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.
What we expect from you
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.
What you'll get in return
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.
TNO as an employer
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.
The selection process
After the first CV selection, the application process will be conducted by the concerning department. TNO will provide a suitable internship agreement. If you have any questions about this vacancy, you can contact the contact person mentioned below.
Due to Covid-19 and the consequent uncertainties and restrictions, students who are not residing in the Netherlands may currently not be able to start an internship or graduation project at TNO.
Has this job opening sparked your interest?
Then we’d like to hear from you! Please contact us for more information about the job or the selection process. To apply, please upload your CV and covering letter using the ‘apply now’ button.