Observable behavior of distributed systems: component reasoning for concurrent objects

DOI10.1016/J.JLAP.2012.01.003MaRDI QIDQ444466zbMATH OpenOpenAlexFDO

Authors Crystal Chang Din, Johan Dovland, Einar Broch Johnsen, Olaf Owe

Publication date 14 August 2012

Published in The Journal of Logic and Algebraic Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.jlap.2012.01.003

zbMATH Keywords

distributed systemsHoare logiccompositional reasoningconcurrent objectsobject-orientation

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Logic in computer science (03B70) Distributed systems (68M14) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Observable behavior of dynamic systems: component reasoning for concurrent objects
• A sound and complete reasoning system for asynchronous communication with shared futures
• Compositional reasoning about active objects with shared futures
• Compositional Reasoning about Shared Futures
• A shared-variable concurrency analysis of multi-threaded object-oriented programs

Cites work

• scientific article; zbMATH DE number 4039251 (Why is no real title available?)
• scientific article; zbMATH DE number 54048 (Why is no real title available?)
• scientific article; zbMATH DE number 1759367 (Why is no real title available?)
• A Complete Guide to the Future
• A Hoare logic for dynamic networks of asynchronously communicating deterministic processes
• A proof technique for parallel programs
• A syntax-directed Hoare logic for object-oriented programming concepts.
• A system for compositional verification of asynchronous objects
• Axiomatic semantics of communicating sequential processes
• Behavioral interface description of an object-oriented language with futures and promises
• Defining liveness
• Formal Methods for Components and Objects
• Lazy behavioral subtyping
• Object-oriented specification and open distributed systems
• Observable behavior of distributed systems: component reasoning for concurrent objects
• Observable behavior of dynamic systems: component reasoning for concurrent objects
• Programming Languages and Systems
• Specification and Development of Interactive Systems
• Ten Years of Hoare's Logic: A Survey—Part I
• Ten years of Hoare's logic: A survey. II: Nondeterminism

Cited in

(16)

• A sound and complete reasoning system for asynchronous communication with shared futures
• Observable behavior of dynamic systems: component reasoning for concurrent objects
• Observing Distributed Computation. A Dynamic-Epistemic Approach
• Observable behavior of distributed systems: component reasoning for concurrent objects
• Compositional reasoning about active objects with shared futures
• scientific article; zbMATH DE number 1787169 (Why is no real title available?)
• Dynamic rebinding for concurrent object groups: theory and practice
• An operational semantics for object-oriented concepts based on the class hierarchy
• Analysis of executable software models
• On detecting over-eager concurrency in asynchronously communicating concurrent object systems
• Proving the safety of highly-available distributed objects
• A secrecy-preserving language for distributed and object-oriented systems
• Modeling actor systems using dynamic I/O automata
• Predicting the behaviour of three-tiered applications: dealing with distributed-object technology and databases
• A proof system for adaptable class hierarchies
• Key-ABS: a deductive verification tool for the concurrent modelling language ABS

Describes a project that uses

Uses Software

• Java Jr
• ABS
• JCobox

This page was built for publication: Observable behavior of distributed systems: component reasoning for concurrent objects

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