Cyber-physical systems (CPSs) are everywhere, from autonomous vehicles to medical devices to smart buildings. Designing such CPSs that achieve complex tasks is a tedious and error prone process. During the design, high-level specifications describing desired functionalities, safety measures, physical properties and restrictions, and optimality criteria have to be considered. Furthermore, as people’s life may depend on CPSs, their correctness is of critical importance. This project will investigate the design aspect focusing on subsets of Timed Automata (TA) as a modeling formalism and Metric Linear Temporal Logic (MITL) as a high-level specification language.

This project aims at developing new theory and novel academic tools to make possible the design of such systems in an automated way from a set of given descriptions and specifications with optimality and correctness guarantees.

1. Construction of a partial TA from system descriptions and specifications

In this part, we focus on generating a partial TA from system descriptions and specifications given in structured natural language. While TA synthesis from natural language is quite an ambitious goal, in this project, we are contributing to this goal by developing a tool for generating a partial TA from a set of system description and specification templates.

The first version of our tool is able to generate a TA (that can be imported to UPPAAL) from descriptors. We require detailed descriptors in this phase. In the upcoming versions, we will simplify this and we will try to construct TA from higher level descriptors (closer to natural language).

The tool is available at gitlab.

2. Synthesis of parameters and control strategies for TA

In this part, we will work on generating the “optimal” timed automata from a parametric partial model by both tuning its parameters and synthesizing controllers at the same time.

Part 1 and part 2, combined, present a fully automated framework to synthesize TA from descriptions and specifications.

“This project has received funding from the European Union’s Horizon 2020 research and innovation programme under the Marie Sklodowska-Curie grant agreement No 798482”.