Script: A communication abstraction mechanism and its verification

DOI10.1016/0167-6423(86)90018-3MaRDI QIDQ1064053zbMATH OpenOpenAlexFDO

Authors Nissim Francez, Gadi Taubenfeld, Brent T. Hailpern

Publication date 1986

Published in Science of Computer Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0167-6423(86)90018-3

zbMATH Keywords

abstraction mechanismADAconcurrent programsCSPdeadlockpartial correctnesspatterns of communicationprocessesrolesscriptshared-variable language

Mathematics Subject Classification ID

Theory of operating systems (68N25) Specification and verification (program logics, model checking, etc.) (68Q60)

Review text

We introduce a new abstraction mechanism, called a script, which hides the low-level details that implement patterns of communication. A script localizes the communication between a set of roles (formal processes), to which actual processes enroll to participate in the action of the script. The paper discusses the addition of scripts to the languages CSP and ADA, and to a shared-variable language with monitors. Proof rules are presented for proving partial correctness and freedom from deadlock in concurrent programs using scripts.

Recommendations

• scientific article; zbMATH DE number 3926229
• scientific article; zbMATH DE number 3878340
• scientific article; zbMATH DE number 4011914
• Elucidating concurrent algorithms via layers of abstraction and reification
• On interprocess communication. I: Basic formalism

Cited in

(8)

• A process-calculus-based abstraction for coordinating multi-agent groups
• Some impossibility results in interprocess synchronization
• Fairness and hyperfairness in multi-party interactions
• Two decentralized algorithms for strong interaction fairness for systems with unbounded speed variability
• Corrigenda:Cooperating proofs for distributed programs with multiparty interactions
• On fairness notions in distributed systems. I: A characterization of implementability
• scientific article; zbMATH DE number 3878340 (Why is no real title available?)
• scientific article; zbMATH DE number 3926229 (Why is no real title available?)

Describes a project that uses

Uses Software

• Ada95

This page was built for publication: Script: A communication abstraction mechanism and its verification

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