Formal Requirements Toolkit for Testing and Monitoring Temporal Logic-based Specifications

Testing and verification is an essential procedure to assert a system adheres to some notion of safety. To validate such assertions, monitoring has provided an effective solution to verifying the conformance of complex systems against a set of properties describing what constitutes safe behavior. In authoring such properties, Temporal Logic (TL) has become a widely adopted specification language in many monitoring applications because of its ability to formally capture time-critical behaviors of reactive systems. This broad acceptance into the verification community and others, however, has naturally led to a lack of TL-based requirement elicitation standards as well as increased friction in tool interoperability. In this thesis, I propose a standardization of TL-based requirement languages through the development of a Formal Requirements Toolkit (FoRek): a modular, extensible, and maintainable collection of TL parsers, translators, and interfaces. To this end, six propositional TL languages are supported in addition to their appropriate past-time variants to provide a framework for a variety of applications using TL as a specification language. Furthermore, improvements to the Pythonic Formal Requirements Language (PyFoReL) tool are performed in addition to a formal definition on the structure of a PyFoReL program. And lastly, to demonstrate the results of this work, FoRek is integrated into an offline monitor to showcase its intended use and potential applications into other domains.