An explanatory presentation of composition rules for assumption- commitment specifications

DOI10.1016/0020-0190(94)90041-8MaRDI QIDQ1321833zbMATH OpenOpenAlexFDO

Authors Pierre Collette

Publication date 10 January 1995

Published in Information Processing Letters (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0020-0190(94)90041-8

zbMATH Keywords

concurrencyassumption-commitment specificationscompositional methods

Mathematics Subject Classification ID

Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) (68Q10) Specification and verification (program logics, model checking, etc.) (68Q60) Distributed algorithms (68W15)

Recommendations

• Composition of assumption-commitment specifications in a UNITY style
• scientific article; zbMATH DE number 3905833
• Transformations for compositional verification of assumption-commitment properties
• A compositional specification theory for component behaviours
• Automatic Synthesis of Assumptions for Compositional Model Checking
• Automated Assumption Generation for Compositional Verification
• Automated assumption generation for compositional verification
• Compositional specification in rewriting logic
• Partial specifications and compositional verification

Cites work

• scientific article; zbMATH DE number 3926220 (Why is no real title available?)
• A generalization of Owicki-Gries's Hoare logic for a concurrent while language
• A logical view of composition
• P-A logic - a compositional proof system for distributed programs
• Proofs of Networks of Processes
• Tentative steps toward a development method for interfering programs

Cited in

(5)

• Preserving Contract Satisfiability Under Non-monotonic Composition
• Parallel composition of assumption-commitment specifications: A unifying approach for shared variable and distributed message passing concurrency
• Composition of assumption-commitment specifications in a UNITY style
• Assumption-commitment support for CSP model checking
• Theory and methodology of assumption/commitment based system interface specification and architectural contracts

This page was built for publication: An explanatory presentation of composition rules for assumption- commitment specifications

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