Unity properties and sequences of states, some observations

DOI10.1016/0020-0190(93)90077-MMaRDI QIDQ688444zbMATH OpenOpenAlexFDO

Authors R. T. Udink, Joost N. Kok

Publication date 20 March 1994

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

Full work available at URL https://doi.org/10.1016/0020-0190(93)90077-m

zbMATH Keywords

specificationstepwise refinementunityverification

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Review text

We examine the expressive power of Unity properties in relation to execution sequences of Unity programs. One might expect that if two programs have the same unless and leadsto properties, then they have the same execution sequences. We show that this is not true. We examine whether this difference vanishes if we adopt a stronger notion of fairness, or use ensures properties instead of leadsto properties (possibly adopting a stronger fairness notion also). We show by a simple example that both approaches are not successful. Hence, properties are not expressive enough to characterize execution sequences, and it is not clear what execution model corresponds to Unity properties. As a consequence, the notion of property preserving program refinement differs from the notion of decreasing nondeterminism.

Recommendations

• On the logic of UNITY
• DUALITY: A simple formalism for the analysis of UNITY
• Data refinement of mixed specifications: A generalization of UNITY
• UNITY and Büchi automata
• Properties of concurrent programs

Cites work

• A simple proof of a completeness result for \(leads\)-\(to\) in the UNITY logic
• scientific article; zbMATH DE number 194539 (Why is no real title available?)
• scientific article; zbMATH DE number 194642 (Why is no real title available?)
• Unity properties and sequences of states, some observations

Cited in

(3)

• A foundation for modular reasoning about safety and progress properties of state-based concurrent programs
• Coordinating action systems
• Unity properties and sequences of states, some observations

Describes a project that uses

Uses Software

• UNITY

This page was built for publication: Unity properties and sequences of states, some observations

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