  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.
