Signal Temporal Logic (STL) is used to reason about the behavior of continuous
signals. Due to its expressivity and algorithms to generate signal monitors, it is used
to define monitoring rules for hardware and software systems. However, it is a hard
task to define an STL formula that describes the system behavior. An expert of the
monitored system should write the formula and optimize its parameters to minimize
the monitoring errors (false alarms and missed alarms). To simplify and disseminate
the use of formal monitors, its necessary to automate the formula writing process,
which motivates this study. In this dissertation, we study the problem of synthesizing
STL formulas from a labeled set of system traces.
The datasets from different fields may vary in size and can be quite large. In order
to handle such cases, we developed a parallel formula synthesis method based on
genetic algorithms. The proposed method does not require any expertise guidance;
it generates formula structure and optimizes the formula parameters simultaneously.
In addition, in order to find the local optimum around an individual, we developed a
randomized search over the parameter space, which is shown to speed up the
convergence of the proposed method.