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.
展开▼
