Formal Specifications using Linear Temporal Lo
Simone Vuotto
Journal of Information Organization, Vol. 10, No. 1, 2020.
DOI: https://doi.org/10.6025/jio/2020/10/1/13-21
Link: http://www.dline.info/jio/fulltext/v10n1/jiov10n1_2.pdf
Abstract:
The definition of a formal specification is a fundamental step in the design of safety-critical systems. The specification defines the behaviors and constraints that the system under development is required to satisfy. Depending on the system dimension, the specification can be used to verify its correctness or the correctness of its abstract model. In some cases, the system can also be directly synthesized from the specification. However, when the system is too complex for a full verification or for synthesis, developers usually rely on testing to demonstrate the correct operation of the system. In this paper we present our ongoing work on automatic test cases generation, relying on Linear Temporal Logic (LTL) as a specification formalism. The presented algorithm is implemented in SPECPRO, our library for supporting analysis and development of formal requirements in cyber-physical systems.