Journal of Information Organization


Vol No. 10 ,Issue No. 1 2020

Formal Specifications using Linear Temporal Lo
Simone Vuotto
Universit‘a degli Studi di Genova & Universit‘a degli Studi di Sassari
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.
Keywords: Formal Specifications, Lineare Temporal Logic Formal Specifications using Linear Temporal Lo
DOI:https://doi.org/10.6025/jio/2020/10/1/13-21
Full_Text   PDF 1.53 MB   Download:   14  times
References:

[1] Baier, C., Katoen, J. P. (2008). Principles of model checking. MIT press.
[2] Broy, M., Jonsson, B., Katoen, J. P., Leucker, M., Pretschner, A. (2005). Model-based testing of reactive systems. In: Volume 3472 of Springer LNCS. Springer.
[3] Duret-Lutz, A., Lewkowicz, A., Fauchille, A., Michaud, T., Renault, E., Xu, L. (2016). Spot 2.0 - framework for LTL and ω automata manipulation. In: Proceedings of the 14th International Symposium on Automated Technology for Verification and Analysis (ATVA’16). Lecture Notes in Computer Science, 9938, 122-129. Springer (October).
[4] Faymonville, P., Finkbeiner, B., Tentrup, L. (2017). Bosy: An experimentation framework for bounded synthesis. In: Proceedings of CAV. LNCS, vol. 10427, 325-332. Springer.
[5] Filiot, E., Jin, N., Raskin, J. F. (2013). Exploiting structure in ltl synthesis. International Journal on Software Tools for Technology Transfer 15 (5-6) 541-561.
[6] Fraser, G., Wotawa, F., Ammann, P. E. (2009). Testing with model checkers: a survey. Software Testing, Verification and Reliability 19 (3) 215-261.
[7] Jacobs, S., Klein, F., Schirmer, S. (2016). A high-level ltl synthesis format: Tlsf v1. 1. arXiv preprint arXiv:1604.02284.
[8] Meyer, P. J., Sickert, S., Luttenberger, M. (2018). Strix: Explicit reactive synthesis strikes back! In: Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part I. pp. 578-586.
[9] Narizzano, M., Pulina, L., Tacchella, A., Vuotto, S. (2018). Consistency of property specification patterns with boolean and constrained numerical signals. In: NASA Formal Methods: 10th International Symposium, NFM 2018, Newport News, VA, USA, April 17-19, 2018, Proceedings. 10811, 383-398. Springer.
[10] Narizzano, M., Pulina, L., Tacchella, A., Vuotto, S. (2019). Property specification patterns at work: verification and inconsistency explanation. Innovations in Systems and Software Engineering, p. 1-17.
[11] Pnueli, A., Manna, Z. (1992). The temporal logic of reactive and concurrent systems. Springer 16, 12.
[12] Vuotto, S., Narizzano, M., Pulina, L., Tacchella, A. (2019). Automata based test generation with specpro. In: Proceedings of the 6th International Workshop on Requirements Engineering and Testing. 13-16. IEEE Press.
[13] Zeng, B., Tan, L. (2016). Test reactive systems with bnuchi-automaton-based temporal requirements. In: Theoretical Information Reuse and Integration, 31-57. Springer.