Debugging unrealizable specifications with model-based diagnosis

Abstract

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. © 2011 Springer-Verlag Berlin Heidelberg.