Formal Methods in Software Engineering

Verifying Reachability-Logic Properties on Rewriting-Logic Specifications

Year2015
TypeConference
StatusProceedings
AuthorsDorel Lucanu, Vlad Rusu, Andrei Arusoaie, David Nowak

Links

Abstract

Rewriting Logic is a simply, flexible, and powerful framework for specifying and analysing concurrent systems. Reachability Logic is a recently introduced formalism, which is currently used for defining the operational semantics of programming languages and for stating properties about program executions. Reachability Logic has its roots in a wider-spectrum framework, namely, in Rewriting Logic Semantics. In this paper we show how Reachability Logic can be adapted for stating properties of transition systems described by Rewriting-Logic specifications. We propose a procedure for verifying Rewriting-Logic specifications against Reachability-Logic properties. We prove the soundness of the procedure and illustrate it by verifying a communication protocol specified in Maude.

BibTeX

@inproceedings{LucanuRAN15, author = {Dorel Lucanu and Vlad Rusu and Andrei Arusoaie and David Nowak}, title = {Verifying Reachability-Logic Properties on Rewriting-Logic Specifications}, booktitle = {Logic, Rewriting, and Concurrency - Essays dedicated to Jos{'{e}} Meseguer on the Occasion of His 65th Birthday}, series = {Lecture Notes in Computer Science}, volume = {9200}, publisher = {Springer}, year = {2015}, pages = {451--474}, year = {2015}, url = {http://dx.doi.org/10.1007/978-3-319-23165-5_21 [LRC]}, doi = {10.1007/978-3-319-23165-5_21} }