TLtoSQL: Rapid post-mortem verification using temporal logic to SQL code generation in the Eclipse PDE

This paper addresses the need for formal specification and high-level verification of requirements of complex reactive system of systems. It describes a technique and the associated TLtoSQL tool-set that consists of four plugins for the popular Eclipse environment: (i) a database tool that records JUnit tests in an JDBC compliant database, (ii) a graphical editor for propositional linear-time temporal logic (PLTL) and metric temporal logic (MTL) formal specifications, (iii) an automatic code generator that converts such PLTL and MTL specifications into Standard Query Language (SQL) code, (iv) a database engine that executes the generated SQL of (iii) on database tables of (i) thereby yielding a form of verification we call post-mortem verification.