Property Specification Patterns (PSPs) have been proposed to solve recurring specification needs, to ease the formalization of requirements, and enable automated verification thereof. In this paper, we extend PSPs by considering Boolean as well as atomic numerical assertions. This extension enables us to reason about functional requirements which would not be captured by basic PSPs. We contribute an encoding from constrained PSPs to LTL formulae, and we show experimental results demonstrating that our approach scales on requirements of realistic size generated using a probabilistic model. Finally, we show that our extension enables us to prove (in)consistency of requirements about an embedded controller for a robotic manipulator.

Consistency of property specification patterns with boolean and constrained numerical signals / Narizzano, Massimo; Pulina, Luca; Tacchella, Armando; Vuotto, Simone. - 10811:(2018), pp. 383-398. (Intervento presentato al convegno 10th International Symposium on NASA Formal Methods, NFM 2018 tenutosi a usa nel 2018) [10.1007/978-3-319-77935-5_26].

Consistency of property specification patterns with boolean and constrained numerical signals

VUOTTO, Simone
2018-01-01

Abstract

Property Specification Patterns (PSPs) have been proposed to solve recurring specification needs, to ease the formalization of requirements, and enable automated verification thereof. In this paper, we extend PSPs by considering Boolean as well as atomic numerical assertions. This extension enables us to reason about functional requirements which would not be captured by basic PSPs. We contribute an encoding from constrained PSPs to LTL formulae, and we show experimental results demonstrating that our approach scales on requirements of realistic size generated using a probabilistic model. Finally, we show that our extension enables us to prove (in)consistency of requirements about an embedded controller for a robotic manipulator.
2018
9783319779348
Consistency of property specification patterns with boolean and constrained numerical signals / Narizzano, Massimo; Pulina, Luca; Tacchella, Armando; Vuotto, Simone. - 10811:(2018), pp. 383-398. (Intervento presentato al convegno 10th International Symposium on NASA Formal Methods, NFM 2018 tenutosi a usa nel 2018) [10.1007/978-3-319-77935-5_26].
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/209406
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 13
  • ???jsp.display-item.citation.isi??? 9
social impact