Title: Weakest precondition based modelling and verification of a class of concurrent systems
Authors: Anup Kumar Bandyopadhyay
Addresses: Department of Electronics and Telecommunication Engineering, Jadavpur University, Kolkata 700032, India
Abstract: 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.
Keywords: weakest precondition; program proving; program correctness; reactive systems; concurrent systems; verification; interactive sequential processes; mutual exclusion; mathematical modelling.
International Journal of Artificial Intelligence and Soft Computing, 2010 Vol.2 No.1/2, pp.115 - 131
Published online: 04 Apr 2010 *Full-text access for editors Access for subscribers Purchase this article Comment on this article