Concurrency: State Models and Java Programs

2017-07-07 02:10:07

A.4 Properties

Table A.4: Safety and progress properties
Safety property	A safety property P defines a deterministic process that asserts that any trace including actions in the alphabet of P is accepted by P.
Progress progress	progress P = {a₁,a₂..a_n} defines a progress property P which asserts that in an infinite execution of a target system, at least one of the actions a₁,a₂..a_n will be executed infinitely often.