Aaronprojects

Spec Illustration

The ERATO MMSD project is developing tools to apply formal logic to industrial applications, notably self-driving vehicles. In order for it to see adoption in industry, it is deemed paramount to make formal logic more intuitive to lay people. As part of my work in this project, I therefore developed a tool to visualise the semantics of specifications in Signal Temporal Logic (STL). As the name implies, this kind of logic allows for reasoning over time, making it useful to reason about vehicle movement over time, for instance.

Owing in part to its embedding at the National Institute of Informatics (国立情報学研究所) in Tokyo, Japan, the project saw many industrial partners. During the development of this tool, some pilots were held to fine-tune in accordance with potential end-users' demands. This made for a dynamic development process.

The screenshots below depict an example of a workspace in the tool. It shows how a specification is parsed and applied to several named signals, resulting in a particular series of semantics. These semantics are visualised in a tree structure, thereby indicating where the logic has (un)intended consequences. Understanding these semantics is paramount before moving on from relatively simple specifications to more extensive conjunctions of logic. In future research, we would like to put this to the test.

Example workspace

Additional screenshots