A.4 Properties

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 = {a1,a2..an} defines a progress property P which asserts that in an infinite execution of a target system, at least one of the actions a1,a2..an will be executed infinitely often.