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.

DOI: 10.1504/IJAISC.2010.032516

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 Full-text access for subscribers Purchase this article Comment on this article