Parametric systems arise in different application domains, such as software, cyber-physical systems or tasks scheduling. A key challenge is to estimate the values of parameters that guarantee the desired behaviours of the system. In this paper, we propose a novel approach based on an extension of the IC3 algorithm for infinite-state transition systems. The algorithm finds the feasible region of parameters by complement, incrementally finding and blocking sets of “bad” parameters which lead to system failures. If the algorithm terminates we obtain the precise region of feasible parameters of the system. We describe an implementation for symbolic transition systems with linear constraints and perform an experimental evaluation on benchmarks taken from the domain of hybrid systems. The results demonstrate the potential of the approach.

Parameter Synthesis with IC3 / Cimatti, A.; Griggio, A.; Mover, S.; Tonetta, S.. - (2013). (Intervento presentato al convegno Formal Methods in Compuiter-Aided Desisgn 2013 tenutosi a Portland, OR, USA nel October 20-23, 2013).

Parameter Synthesis with IC3

Cimatti A.;Griggio A.;Mover S.;Tonetta S.
2013-01-01

Abstract

Parametric systems arise in different application domains, such as software, cyber-physical systems or tasks scheduling. A key challenge is to estimate the values of parameters that guarantee the desired behaviours of the system. In this paper, we propose a novel approach based on an extension of the IC3 algorithm for infinite-state transition systems. The algorithm finds the feasible region of parameters by complement, incrementally finding and blocking sets of “bad” parameters which lead to system failures. If the algorithm terminates we obtain the precise region of feasible parameters of the system. We describe an implementation for symbolic transition systems with linear constraints and perform an experimental evaluation on benchmarks taken from the domain of hybrid systems. The results demonstrate the potential of the approach.
2013
Formal Methods in Computer-Aided Design
-
New York
IEEE
Cimatti, A.; Griggio, A.; Mover, S.; Tonetta, S.
Parameter Synthesis with IC3 / Cimatti, A.; Griggio, A.; Mover, S.; Tonetta, S.. - (2013). (Intervento presentato al convegno Formal Methods in Compuiter-Aided Desisgn 2013 tenutosi a Portland, OR, USA nel October 20-23, 2013).
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/11572/343084
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 43
  • ???jsp.display-item.citation.isi??? 28
social impact