Model checking parameterized by the semantics in maude

Abstract

Model checking is an automatic verification technique for analyzing whether some properties hold in a model. Maude is a high-performance logical framework and model checking tool where many different concurrent programming languages have been specified and analyzed. However, the counterexample generated by Maude when a property fails does not correspond to the language being specified but to the Maude rules, which makes it difficult to understand. In this paper we present two metalevel transformations for relating counterexamples and semantics when dealing with the semantics of concurrent languages, hence allowing users to model check real code while easing the interpretation of the counterexamples. These transformations can be applied to any semantics following a message-passing or a shared memory approach. These transformations have been implemented in a Maude prototype; we illustrate the tool with examples.