HOME       UP       PREV       FURTHER NOTES       NEXT (ABD - PSL Four-Level Syntax Structure)  

ABD - PSL Assertion, General Structure

PSL - Property Specification Language

»www.project-veripage.com/psl_tutorial_2.php


General structure of a PSL assertion
As in most temporal logics, there are three main directives:
  1. always and never,
  2. next (family of them),
  3. eventually!

The always directive is the most frequently used and it specifies that the following property expression should be checked every clock.

The next directive relates successive state properties, as qualified by the clocking event and qualifying guard.

The eventually! directive is for liveness properties that must happen at some time in the future.

(C) 2008-10, DJ Greaves, University of Cambridge, Computer Laboratory.