DeepSTL -- From English Requirements to Signal Temporal Logic

TL;DR

DeepSTL is a novel tool that uses neural translation techniques to convert informal English requirements into formal Signal Temporal Logic specifications, aiming to make formal methods more accessible.

Contribution

It introduces a two-step workflow combining synthetic data generation and transformer-based neural translation for English to STL conversion.

Findings

High translation accuracy for well-trained English requirement patterns

Synthetic data generation effectively supports training neural translation models

Workflow shows promise for extending to more complex translation tasks

Abstract

Formal methods provide very powerful tools and techniques for the design and analysis of complex systems. Their practical application remains however limited, due to the widely accepted belief that formal methods require extensive expertise and a steep learning curve. Writing correct formal specifications in form of logical formulas is still considered to be a difficult and error prone task. In this paper we propose DeepSTL, a tool and technique for the translation of informal requirements, given as free English sentences, into Signal Temporal Logic (STL), a formal specification language for cyber-physical systems, used both by academia and advanced research labs in industry. A major challenge to devise such a translator is the lack of publicly available informal requirements and formal specifications. We propose a two-step workflow to address this challenge. We first design a grammar-based generation technique of synthetic data, where each output is a random STL formula and its associated set of possible English translations. In the second step, we use a state-of-the-art transformer-based neural translation technique, to train an accurate attentional translator of English to STL. The experimental results show high translation quality for patterns of English requirements that have been well trained, making this workflow promising to be extended for processing more complex translation tasks.