Verifying Reachability-Logic Properties on Rewriting-Logic Specifications

Dorel Lucanu 1 Vlad Rusu 2 Andrei Arusoaie 2 David Nowak 3, 4
2 DREAMPAL - Dynamic Reconfigurable Massively Parallel Architectures and Languages
Inria Lille - Nord Europe, CRIStAL - Centre de Recherche en Informatique, Signal et Automatique de Lille (CRIStAL) - UMR 9189
3 2XS - Extra Small Extra Safe
CRIStAL - Centre de Recherche en Informatique, Signal et Automatique de Lille (CRIStAL) - UMR 9189
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.
Type de document :
Communication dans un congrès
Logic, Rewriting, and Concurrency - Festschrift Symposium in Honor of José Meseguer, Sep 2015, Urbana Champaign, United States. Springer Verlag, LNCS, 9200, 2015, Logic, Rewriting, and Concurrency Essays Dedicated to José Meseguer on the Occasion of His 65th Birthday. 〈10.1007/978-3-319-23165-5_21〉
Liste complète des métadonnées

Littérature citée [23 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01158941
Contributeur : Pal Dream <>
Soumis le : mardi 2 juin 2015 - 11:08:50
Dernière modification le : mardi 3 juillet 2018 - 11:41:28
Document(s) archivé(s) le : mardi 25 avril 2017 - 00:03:19

Fichier

festchrift.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Citation

Dorel Lucanu, Vlad Rusu, Andrei Arusoaie, David Nowak. Verifying Reachability-Logic Properties on Rewriting-Logic Specifications. Logic, Rewriting, and Concurrency - Festschrift Symposium in Honor of José Meseguer, Sep 2015, Urbana Champaign, United States. Springer Verlag, LNCS, 9200, 2015, Logic, Rewriting, and Concurrency Essays Dedicated to José Meseguer on the Occasion of His 65th Birthday. 〈10.1007/978-3-319-23165-5_21〉. 〈hal-01158941〉

Partager

Métriques

Consultations de la notice

434

Téléchargements de fichiers

133