Realizability - checking whether a specification can be implemented by an open system - is a fundamental step in the design flow. However, if the specification turns out not to be realizable, there is no method to pinpoint the causes for unrealizability. In this paper, we address the open problem of providing diagnostic information for realizability: we formally define the notion of (minimal) explanation of (un)realizability, we propose algorithms to compute such explanations, and provide a preliminary experimental evaluation. © 2008 Springer-Verlag Berlin Heidelberg.
Diagnostic Information for Realizability / Cimatti, Alessandro; Roveri, Marco; Schuppan, Viktor; Tchaltsev, Andrei. - 4905:(2008), pp. 52-67. ( 9th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2008 San Francisco, USA 07/01/2008-09/01/2008) [10.1007/978-3-540-78163-9_9].
Diagnostic Information for Realizability
Alessandro Cimatti;Marco Roveri;
2008-01-01
Abstract
Realizability - checking whether a specification can be implemented by an open system - is a fundamental step in the design flow. However, if the specification turns out not to be realizable, there is no method to pinpoint the causes for unrealizability. In this paper, we address the open problem of providing diagnostic information for realizability: we formally define the notion of (minimal) explanation of (un)realizability, we propose algorithms to compute such explanations, and provide a preliminary experimental evaluation. © 2008 Springer-Verlag Berlin Heidelberg.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione
