In this paper we introduce a new automata based test generation algorithm implemented in SPECPRO, our library for supporting analysis and development of formal requirements in cyber-physical systems. We consider specifications written in Linear Temporal Logic (LTL) from which we extract automatically trap properties representing the expected behaviour of the system under development. With respect to manual generation, the main advantage of SPECPRO is that it frees the developer from the burden of generating tests in order to achieve stated coverage targets. Our goal is to have SPECPRO handle specifications of small-but-critical components in an effective way.

Automata based test generation with SpecPro / Vuotto, S.; Narizzano, M.; Pulina, L.; Tacchella, A.. - (2019), pp. 13-16. (Intervento presentato al convegno 6th IEEE/ACM International Workshop on Requirements Engineering and Testing, RET 2019 tenutosi a can nel 2019) [10.1109/RET.2019.00010].

Automata based test generation with SpecPro

Vuotto S.;Pulina L.;
2019-01-01

Abstract

In this paper we introduce a new automata based test generation algorithm implemented in SPECPRO, our library for supporting analysis and development of formal requirements in cyber-physical systems. We consider specifications written in Linear Temporal Logic (LTL) from which we extract automatically trap properties representing the expected behaviour of the system under development. With respect to manual generation, the main advantage of SPECPRO is that it frees the developer from the burden of generating tests in order to achieve stated coverage targets. Our goal is to have SPECPRO handle specifications of small-but-critical components in an effective way.
2019
978-1-7281-2274-8
Automata based test generation with SpecPro / Vuotto, S.; Narizzano, M.; Pulina, L.; Tacchella, A.. - (2019), pp. 13-16. (Intervento presentato al convegno 6th IEEE/ACM International Workshop on Requirements Engineering and Testing, RET 2019 tenutosi a can nel 2019) [10.1109/RET.2019.00010].
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11388/239899
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 1
  • ???jsp.display-item.citation.isi??? 0
social impact