Formal Methods for Open Object-Based Distributed Systems

DOI10.1007/b94120zbMath1253.68249OpenAlexW4205898334MaRDI QIDQ5902548

Kazuhiro Ogata, Kokichi Futatsugi

Publication date: 12 January 2010

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/b94120

zbMATH Keywords

verificationalgebraic specificationCafeOBJobservational transition systemproof scoresthe NSLPK authentication protocol

Mathematics Subject Classification ID

Abstract data types; algebraic specification (68Q65) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Authentication, digital signatures and secret sharing (94A62)

Related Items (10)

Generic Proof Scores for Generate & Check Method in CafeOBJ ⋮ Principles of proof scores in CafeOBJ ⋮ Twenty years of rewriting logic ⋮ From hidden to visible: a unified framework for transforming behavioral theories into rewrite theories ⋮ Incremental Proofs of Termination, Confluence and Sufficient Completeness of OBJ Specifications ⋮ Verifying the Design of Dynamic Software Updating in the OTS/CafeOBJ Method ⋮ Mechanical Analysis of Reliable Communication in the Alternating Bit Protocol Using the Maude Invariant Analyzer Tool ⋮ Theorem Proving Based on Proof Scores for Rewrite Theory Specifications of OTSs ⋮ A Maude environment for CafeOBJ ⋮ Generate & Check Method for Verifying Transition Systems in CafeOBJ

This page was built for publication: Formal Methods for Open Object-Based Distributed Systems