Diagnostic information for realizability. (English) Zbl 1138.68442
Logozzo, Francesco (ed.) et al., Verification, model checking, and abstract interpretation. 9th international conference, VMCAI 2008, San Francisco, USA, January 7–9, 2008. Proceedings. Berlin: Springer (ISBN 978-3-540-78162-2/pbk). Lecture Notes in Computer Science 4905, 52-67 (2008).
Summary: 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.
For the entire collection see [Zbl 1134.68006].
For the entire collection see [Zbl 1134.68006].
MSC:
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
References:
| [1] | Abadi, M.; Lamport, L.; Wolper, P.; Ronchi Della Rocca, S.; Ausiello, G.; Dezani-Ciancaglini, M., Realizable and unrealizable specifications of reactive systems, Automata, Languages and Programming, 1-17 (1989), Heidelberg: Springer, Heidelberg · doi:10.1007/BFb0035748 |
| [2] | European Railway Agency. Feasibility study for the formal specification of ETCS functions. Sep, Invitation to tender (2007), http://www.era.europa.eu |
| [3] | Behrmann, G., et al.: UPPAAL-Tiga: Time for playing games! In: Damm and Hermanns [11], pp. 121-125. |
| [4] | Bloem, R., et al.: RAT: Formal analysis of requirements. In: Damm and Hermanns [11], pp. 263-267. |
| [5] | Bloem, R.; Lauwereins, R.; Madsen, J., Interactive presentation: Automatic hardware synthesis from specifications: A case study, DATE, 1188-1193 (2007), New York: ACM Press, New York |
| [6] | Bontemps, Y.; Schobbens, P.; Löding, C., Synthesis of open reactive systems from scenario-based specifications, Fundam. Inform., 62, 2, 139-169 (2004) · Zbl 1082.68064 |
| [7] | Clarke, E.; Halbwachs, N.; Peled, D. A., NuSMV: A new symbolic model verifier, Computer Aided Verification, 495-499 (1999), Heidelberg: Springer, Heidelberg · Zbl 1046.68587 |
| [8] | Cimatti, A., et al.: Diagnostic information for realizability. Technical Report FBK-092007-01, Fondazione Bruno Kessler (2007), http://es.fbk.eu/people/roveri/tests/vmcai08 · Zbl 1138.68442 |
| [9] | Cimatti, A., et al.: Boolean abstraction for temporal logic satisfiability. In: Damm and Hermanns [11], pp. 532-546 · Zbl 1135.68469 |
| [10] | Clarke, E.; Veith, H.; Dershowitz, N., Counterexamples Revisited: Principles, Algorithms, Applications, Verification: Theory and Practice, 208-224 (2004), Heidelberg: Springer, Heidelberg · Zbl 1274.68179 |
| [11] | Damm, W.; Hermanns, H., Computer Aided Verification (2007), Heidelberg: Springer, Heidelberg · Zbl 1119.68005 |
| [12] | Groce, A.: Error Explanation and Fault Localization with Distance Metrics. PhD thesis, Carnegie Mellon University (2005) · Zbl 1126.68477 |
| [13] | Lynce, I., Marques Silva, J.: On computing minimum unsatisfiable cores. In: SAT (2004) |
| [14] | Pill, I.; Sentovich, E., Formal analysis of hardware requirements, DAC, 821-826 (2006), New York: ACM Press, New York |
| [15] | Pnueli, A.; Piterman, N.; Sa’ar, Y.; Emerson, E. A.; Namjoshi, K. S., Synthesis of Reactive(1) Designs, Verification, Model Checking, and Abstract Interpretation, 364-380 (2005), Heidelberg: Springer, Heidelberg · Zbl 1176.68126 |
| [16] | Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: 16th Annual ACM Symposium on Principles of Programming Languages, pp. 179-190 (1989) · Zbl 0686.68015 |
| [17] | Safra, S., On the complexity of omega-automata, FOCS, 319-327 (1988), Los Alamitos: IEEE, Los Alamitos |
| [18] | Tripakis, S.; Altisen, K.; Wing, J. M.; Woodcock, J. C.P.; Davies, J., On-the-Fly Controller Synthesis for Discrete and Dense-Time Systems, FM’99 - Formal Methods (1999), Heidelberg: Springer, Heidelberg · Zbl 1037.93522 · doi:10.1007/3-540-48119-2_15 |
| [19] | http://www.prosyd.org |
| [20] | Yoshiura, N., Finding the causes of unrealizability of reactive system formal specifications, SEFM, 34-43 (2004), Los Alamitos: IEEE Computer Society Press, Los Alamitos |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
