On verifying reactive rules using rewriting logic

Abstract

Rule-based programming has been gaining a lot of interest in the industry lately, through the growing use of rules to model the behavior of software systems. A demand for verifying and analyzing rule based systems has thus emerged. In this paper we propose a methodology, based on rewriting logic specifications written in CafeOBJ, for reasoning about structural errors of systems whose behavior is expressed in terms of reactive rules and verifying safety properties within the same framework. We present our approach through a simple but illustrative example of an e-commerce web site. © 2014 Springer International Publishing.