Titre :

Verifying Reachability-Logic Properties on Rewriting-Logic Specifications

Auteur(s) :

Lucanu, Dorel [Auteur]
Department of Computer Science [Lasi]
Rusu, Vlad [Auteur]
Dynamic Reconfigurable Massively Parallel Architectures and Languages [DREAMPAL]
Arusoaie, Andrei [Auteur]
Dynamic Reconfigurable Massively Parallel Architectures and Languages [DREAMPAL]
Nowak, David [Auteur]
Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189 [CRIStAL]
Extra Small Extra Safe [2XS]

Titre de la manifestation scientifique :

Logic, Rewriting, and Concurrency - Festschrift Symposium in Honor of José Meseguer

Ville :

Urbana Champaign

Pays :

Etats-Unis d'Amérique

Date de début de la manifestation scientifique :

2015-09-23

Titre de l’ouvrage :

LNCS

Titre de la revue :

Logic, Rewriting, and Concurrency Essays Dedicated to José Meseguer on the Occasion of His 65th Birthday

Éditeur :

Springer Verlag

Date de publication :

2015

Discipline(s) HAL :

Informatique [cs]/Logique en informatique [cs.LO]

Résumé en anglais : [en]

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 ...
Lire la suite >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.Lire moins >

Langue :

Anglais

Comité de lecture :

Oui

Audience :

Internationale

Vulgarisation :

Non

Collections :

• Centre de Recherche en Informatique, Signal et Automatique de Lille (CRIStAL) - UMR 9189

Source :

Harvested from HAL