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

DOI10.1007/978-3-642-54624-2_28MaRDI QIDQ5403083zbMATH OpenOpenAlexFDO

Authors Min Zhang, Kazuhiro Ogata, Kokichi Futatsugi

Publication date 25 March 2014

Published in Specification, Algebra, and Software (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-54624-2_28

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Abstract data types; algebraic specification (68Q65)

Recommendations

• Mutatis mutandis: safe and predictable dynamic software updating
• A Hybrid Model in Dynamic Software Updating for C
• Verification of evolving software via component substitutability analysis
• scientific article; zbMATH DE number 1962762

Cites work

• scientific article; zbMATH DE number 1953034 (Why is no real title available?)
• scientific article; zbMATH DE number 1962761 (Why is no real title available?)
• All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
• CafeOBJ Report. The language, proof techniques, and methodologies for object-oriented algebraicspecification
• Contextual effects for version-consistent dynamic software updating and safe concurrent programming
• Mutatis mutandis: safe and predictable dynamic software updating
• Proof scores in the OTS/CafeOBJ method.
• Some Tips on Writing Proof Scores in the OTS/CafeOBJ Method
• Type-based hot swapping of running modules (extended abstract)

Cited in

(5)

• Verification of evolving software via component substitutability analysis
• A Hybrid Model in Dynamic Software Updating for C
• Mutatis mutandis: safe and predictable dynamic software updating
• On the effectiveness of a message-driven confidence-driven protocol for guarded software upgrading
• On Automation of OTS/CafeOBJ Method

Describes a project that uses

Uses Software

• Maude
• CafeOBJ

This page was built for publication: Verifying the Design of Dynamic Software Updating in the OTS/CafeOBJ Method

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5403083)