The initialization of complex cyber-physical systems often requires the interaction of various components that must start up with strict timing requirements on the provision of signals (power, refrigeration, light, etc.). In order to safely allow an independent development of components, it is necessary to ensure a safe decomposition, i.e. the specification of local timing requirements that prevent later integration errors due to the dependencies. We propose a high-level formalism to model local timing requirements and dependencies. We consider the problem of checking the consistency (existence of an execution satisfying the requirements) and compatibility (absence of an execution that reaches an integration error) of the local requirements, and the problem of synthesizing a region of timing constraints that represents all possible correct refinements of the original specification. We show how the problems can be naturally translated into a model checking and synthesis problem for timed automata with shared variables. Exploiting the linear structure of the requirements, we propose an encoding of the problem into SMT. We evaluate the SMT-based approach using MathSAT and show how it scales better than the automata-based approach using Uppaal and nuXmv.

Safe Decomposition of Startup Requirements: Verification and Synthesis / Cimatti, Alessandro; Geatti, Luca; Griggio, Alberto; Kimberly, Greg; Tonetta, Stefano. - 12078:(2020), pp. 155-172. ((Intervento presentato al convegno TACAS 2020: Tools and Algorithms for the Construction and Analysis of Systems tenutosi a Dublin, Ireland nel April 25–30, 2020 [10.1007/978-3-030-45190-5_9].

Safe Decomposition of Startup Requirements: Verification and Synthesis

Alessandro Cimatti;Alberto Griggio;Stefano Tonetta
2020

Abstract

The initialization of complex cyber-physical systems often requires the interaction of various components that must start up with strict timing requirements on the provision of signals (power, refrigeration, light, etc.). In order to safely allow an independent development of components, it is necessary to ensure a safe decomposition, i.e. the specification of local timing requirements that prevent later integration errors due to the dependencies. We propose a high-level formalism to model local timing requirements and dependencies. We consider the problem of checking the consistency (existence of an execution satisfying the requirements) and compatibility (absence of an execution that reaches an integration error) of the local requirements, and the problem of synthesizing a region of timing constraints that represents all possible correct refinements of the original specification. We show how the problems can be naturally translated into a model checking and synthesis problem for timed automata with shared variables. Exploiting the linear structure of the requirements, we propose an encoding of the problem into SMT. We evaluate the SMT-based approach using MathSAT and show how it scales better than the automata-based approach using Uppaal and nuXmv.
Tools and Algorithms for the Construction and Analysis of Systems- 26th International Conference, (TACAS) 2020, Held as Part of theEuropean Joint Conferences on Theory and Practice of Software, (ETAPS) 2020, Dublin, Ireland, April 25-30, 2020, Proceedings, Part (I)
Cham, Switzerland
Springer
Cimatti, Alessandro; Geatti, Luca; Griggio, Alberto; Kimberly, Greg; Tonetta, Stefano
Safe Decomposition of Startup Requirements: Verification and Synthesis / Cimatti, Alessandro; Geatti, Luca; Griggio, Alberto; Kimberly, Greg; Tonetta, Stefano. - 12078:(2020), pp. 155-172. ((Intervento presentato al convegno TACAS 2020: Tools and Algorithms for the Construction and Analysis of Systems tenutosi a Dublin, Ireland nel April 25–30, 2020 [10.1007/978-3-030-45190-5_9].
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/342975
 Attenzione

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

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