A rewriting logic-based computation and deduction approach to avoid reactive system malfunctions

Abstract

Maude is, a powerful formal declarative programming language based on rewriting logic. Because of the reflective characteristic of the rewriting logic, Maude is considered by the scientific community as a universal model of computation and a state-of-the-art formal method in the field of algebraic specification and concurrency modeling. In this paper we show that reactive systems can easily be prototyped using Maude language. A computation and deduction scheme will be presented to prove the feasibility of rewriting logic to deal with verification systems. Experimental results are obtained from the application of the developed tool to an e-business procedure based on an IEC (International Electrotechnical Commission) standard 625-1 1979 interface protocol for programmable measuring instruments.