Weakest precondition semantics for time and concurrency

DOI10.1016/0020-0190(92)90116-DzbMath0769.68086MaRDI QIDQ1195491

H. S. M. Zedan, David Scholefield

Publication date: 29 November 1992

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

Full work available at URL: https://doi.org/10.1016/0020-0190(92)90116-d

zbMATH Keywords

verification; formal semantics; real-time systems; refinement calculus; concurrency; predicate transformers; real-time concurrent language; weakest precondition semantics

Mathematics Subject Classification ID

68Q10: Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.)

68Q55: Semantics in the theory of computing

Related Items

Automatic generation of path conditions for concurrent timed systems, Weakest precondition semantics for time and concurrency, A specification-oriented semantics for the refinement of real-time systems, Transformational vs reactive refinement in real-time systems, Real-time refinement in Manna and Pnueli's temporal logic, A theory of Orwellian specifications with NewThink

Cites Work

• A theoretical basis for stepwise refinement and the programming calculus
• Weakest precondition semantics for time and concurrency
• Real-time refinement in Manna and Pnueli's temporal logic
• An axiomatic basis for computer programming
• Unnamed Item
• Unnamed Item