Specification, Algebra, and Software : Essays Dedicated to Kokichi Futatsugi / edited by Shusaku Iida, José Meseguer, Kazuhiro Ogata.

Format:

Book

Contributor:

Iida, Shusaku, editor.

Meseguer, José, editor.

Ogata, Kazuhiro, editor.

SpringerLink (Online service)

Series:

Computer Science (Springer-11645)

LNCS sublibrary. Theoretical computer science and general issues ; SL 1, 8373.

Theoretical Computer Science and General Issues ; 8373

Language:

English

Subjects (All):

Computer logic.

Logic, Symbolic and mathematical.

Software engineering.

Programming languages (Electronic computers).

Logics and Meanings of Programs.

Mathematical Logic and Formal Languages.

Software Engineering.

Programming Languages, Compilers, Interpreters.

Local Subjects:

Logics and Meanings of Programs.

Mathematical Logic and Formal Languages.

Software Engineering.

Programming Languages, Compilers, Interpreters.

Physical Description:

1 online resource (XXII, 657 pages) : 115 illustrations.

Edition:

First edition 2014.

Contained In:

Springer eBooks

Place of Publication:

Berlin, Heidelberg : Springer Berlin Heidelberg : Imprint: Springer, 2014.

System Details:

text file PDF

Summary:

This Festschrift volume, published in honor of Kokichi Futatsugi, contains 31 invited contributions from internationally leading researchers in formal methods and software engineering. Prof. Futatsugi is one of the founding fathers of the field of algebraic specification and verification and is a leading researcher in formal methods and software engineering. He has pioneered and advanced novel algebraic methods and languages supporting them such as OBJ and CafeOBJ and has worked tirelessly over the years to bring such methods and tools in contact with software engineering practice. This volume contains contributions from internationally leading researchers in formal methods and software engineering.

Contents:

Domain Endurants: An Analysis and Description Process Model

On Formal Definition and Analysis of Formal Verification Processes

CafeOBJ Traces

Parchments for CafeOBJ Logics

Incremental Proofs of Termination, Confluence and Sufficient Completeness of OBJ Specifications

The Versatile Synchronous Observer

Model Checking TLR* Guarantee Formulas on Infinite Systems

Towards a Combination of CafeOBJ and PAT.-Negative Variables and the Essence of Object-Oriented Programming

Reasoning (on) Service Component Ensembles in Rewriting Logic

Dynamic Validation of Maude Prototypes of UML Models

Inspecting Rewriting Logic Computations (in a Parametric and Stepwise Way)

The Semantics of Datalog for the Evidential Tool Bus (Extended Abstract)

Synthesis of Infinite-State Abstractions and Their Use for Software Validation

Behavioral Rewrite Systems and Behavioral Productivity

Functional Logic Programming in Maude

Confluence: The Unifying, Expressive Power of Locality

Foundations for Ensemble Modeling - The Helena Approach: Handling Massively Distributed Systems with ELaborate ENsemble Architectures

Behaviour, Interaction and Dynamics

Partially Ordered Knowledge Sharing and Fractionated Systems in the Context of other Models for Distributed Computing

Extending Operation Semantics to Enhance the Applicability of Formal Refinement

An Institution for Imperative RSL Specifications

8k-ary Grid Graph Models of Tabular Forms

Everlasting Challenges with the OBJ Language Family

Formal Modeling and Analysis of Google's Megastore in Real-Time Maude

EHRA: Specification and Analysis of Energy-Harvesting Wireless Sensor Networks

Some Engineering Applications of the OTS/CafeOBJ Method

Verifying the Design of Dynamic Software Updating in the OTS/CafeOBJ Method

On Automation of 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.

Other Format:

Printed edition:

ISBN:

978-3-642-54624-2

9783642546242

Access Restriction:

Restricted for use by site license.