A monitoring tool for linear-time μHML▪

We present detectEr , a monitoring tool that targets software applications written for Erlang/OTP. The tool runtime checks specifications expressed in a safety fragment of the linear-time modal μ -calculus called ▪, used to describe properties about the current system execution. Our technical development is founded on previous theoretical results that are lifted to a first-order setting, where systems produce executions containing events that carry data. We overview the main features of detectEr , showing how properties can be flexibly written and synthesised as executable Erlang monitors that can be instrumented with the running system. • detectEr is a scalable runtime verification tool for monitoring Erlang applications. • detectEr uses a linear-time monitorable logic fragment of the modal μ -calculus. • This linear-time logic fragment describes properties about the current system execution. • detectEr synthesises correct runtime monitors from properties expressed in this logic. • Monitors are instrumented via source-level weaving to induce minimal runtime overhead.