Internship | Improving the readability of synthesized supervisor guards

Introduction
Cyber-physical systems consist of mechatronic components that are controlled by software. This control software typically includes a supervisory controller that orchestrates the interaction between the various system components. For industrial-scale systems the supervisory controller may be highly complex and non-trivial to develop correctly.
 
To help manage the complexity of guaranteeing safe control, synthesis-based engineering (SBE) provides assistance by combining model-based engineering with computer-aided design. SBE builds on the synthesis procedure: (symbolically) computing a correct-by-construction controller from models of the to-be-controlled system and associated requirements. For an example of SBE see: https://eclipse.dev/escet/cif/synthesis-based-engineering/example.html.

What will you be doing?
Readability of synthesized supervisors is important for engineers to be able to comprehend and easily work with them. However, synthesized supervisors are currently not always easy to read. This research project aims to improve their readability and conciseness. Having readable guards would help explainability, such that an engineer can comprehend and trust the results generated by the synthesis procedure. And it helps faster evaluation of the guards, which makes a translation to PLC code easier.

Eclipse ESCET provides a model-based approach and toolkit for developing supervisory controllers. The symbolic synthesis algorithms of Eclipse ESCET compute supervisors that assign to each controllable event an extra guard. These extra guards ensure that the corresponding events can only occur whenever this does not lead to any requirement violations. To make these guards readable, they are converted from an internal symbolic representation (Binary Decision Diagrams, or BDDs) to a more readable representation in the CIF modeling language. Currently, either a Conjunctive Normal Form (CNF) or Disjunctive Normal Form (DNF) is used. Although simple, this conversion may lead to lengthy guards that are not always very readable.

In this project, you will explore alternative strategies for computing and/or converting extra guards for controllable events, to improve their conciseness and readability. One idea could be to use alternative binary representations, such as MDDs (multi-valued decision diagram), to resolve any binary encoding details that may arise with BDDs. Another idea could be to reuse results from related fields, like multi-level logic circuit optimization. You will investigate existing literature, shape your own ideas based on the literature, implement the ideas, and validate the approach. If successful, the results could be incorporated into the Eclipse ESCET open source project.

You are an MSc student in Computer Science or Mathematics looking for a graduation assignment of 6-9 months. You have an affinity with formal methods as well as programming (in Java) and know the basics of event-based systems. You speak and write English on a sufficient level, are a team player but also capable of independent work, have an open and enthusiastic mindset, and strive for high-quality research and with real industrial impact.

You want an internship opportunity on the precursor of your career; an internship 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. Furthermore, we provide:

• A highly professional, innovative internship environment, within a team of top experts.
• A suitable internship allowance (615 euro for wo-, hbo- and mbo-students, for a full-time internship).
• Possibility of eight hours of free leave per internship month (for a full-time internship).
• A free membership of Jong TNO, where you can meet other TNO professionals and join several activities, such as sports activities, (work-related) courses or the yearly ski-trip.
• Use of a laptop.
• An allowance for travel expenses in case you don’t receive an OV-card.

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.

At TNO we encourage an inclusive work environment, where you can be yourself. Whatever your story and whatever unique qualities you bring to the table. It is by combining our unique strengths and perspectives that we are able to develop innovations that make a real difference in society. Want to know more? Read what steps we are taking in the area of diversity and inclusion.

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.

Important to be aware of before applying:

• Before the start of the internship, the internship agreement from TNO needs to be signed. For students at a college or university based in the Netherlands, TNO uses the UNL-template (supplemented with a number of specific agreements from TNO). For students of foreign and MBO educational institutions, the TNO internship agreement applies. TNO does not sign any other internship agreements.
• Before the start of the internship, the educational institution will need to confirm in writing that:
  • you are enrolled at the educational institution during the internship, and;
  • the internship takes place as part of the programme of the study.
• The confirmation of educational institution takes place by signing the UNL template or forms prepared by TNO.
• Interns at TNO must be in possession of a Dutch residential address at the start of the internship. Performance of internship activities from abroad is not possible.