Weakest precondition based modelling and verification of a class of concurrent systems
Anup Kumar Bandyopadhyay · International Journal of Artificial Intelligence and Soft Computing · 2010
A weakest precondition based modelling and verification technique for a class of concurrent systems is proposed. A system in this class is defined by a set of non-terminating interactive sequential processes. The constituent processes are allowed to include both if-then-else and terminating while-do type control structures. The properties of the system are verified by proving the invariance of logical formulae. The technique is illustrated by considering Dekker's two process mutual exclusion algorithm as an example.