Importance of Liveness Specifications

When reasoning about the correctness of a distributed system, it is really important to specify both safety as well as liveness specifications.

The examples in Tutorials show how to specify both safety and liveness specifications using P Monitors.

Always specify both safety and liveness specifications

Only specifying safety property for a system is not enough, this is mainly because, a system model may be incorrect and in the worst case drop all requests on to the ether and not perform any operation. Such a system trivially satisfies all correctness specifications! Hence, it becomes essential to combine that safety property with liveness properties to check that the system is making progress and servicing the requests. Running the checker on models that have both safety and liveness properties ensures that for all executions explored by the checker, requests are eventually serviced by the system (by sending responses potentially) and all the responses sent by the system satisfy the desired correctness safety specification. This helps ensure that your models are not doing something trivially incorrect like always doing nothing , in which case running the checker on such a model adds no value.

For example, in the case of the client server example, the BankBalanceIsAlwaysCorrect safety property checks that the response sent by the bank server is always correct and combining it with the GuaranteedWithDrawProgress liveness property ensures that system will always eventually send a response which will be checked for correctness by the safety property.