An introduction to assertional reasoning for concurrent systems

摘要: This is a tutorial introduction to assertional reasoning based on temporal logic. The objective provide working familiarity with the technique. We use simple system model and proof system, we keep minimum treatment of issues such as soundness, completeness, compositionality, abstraction. concurrent by state transition fairness requirements. reason about systems using Hoare logic subset linear-time logic, specifically, invariant assertions leads-to assertions. apply method several examples.