05875468

a

05875468 K\"onighofer, Robert Hofferek, Georg Bloem, Roderick Debugging unrealizable specifications with model-based diagnosis. Barner, Sharon (ed.) et al., Hardware and software: verification and testing. 6th international Haifa verification conference, HVC 2010, Haifa, Israel, October 4--7, 2010. Revised selected papers. Berlin: Springer (ISBN 978-3-642-19582-2/pbk). Lecture Notes in Computer Science 6504, 29-45 (2011). 2011 Berlin: Springer EN

doi:10.1007/978-3-642-19583-9_8

Summary: Creating a formal specification for a reactive system is difficult and mistakes happen frequently. Yet, aids for specification debugging are rare. In this paper, we show how model-based diagnosis can be applied to localize errors in unrealizable specifications of reactive systems. An implementation of the system is not required. Our approach identifies properties and signals that can be responsible for unrealizability. By reduction to unrealizability, it can also be used to debug specifications which forbid desired behavior. We analyze specifications given as one set of properties, as well as specifications consisting of assumptions and guarantees. For GR(1) specifications we describe how realizability and unrealizable cores can be computed quickly, using approximations. This technique is not specific to GR(1), though. Finally, we present experimental results where the error localization precision is almost doubled when compared to the presentation of just unrealizable cores.