Towards a formal framework for developing concurrent programs: Modeling dynamic behavior

It is now widely accepted that programming concurrent software is a complex, error-prone task. Therefore, there is a big interest in the specification, verification and development of concurrent programs using formal methods. In our work-in-progress project, we are attempting to make a constructive framework for developing concurrent programs formally. In this paper, we first demonstrate how one can apply an intermediate artifact of our work, a Z-based formalism, to specify the dynamic behavior of a concurrent system. More precisely, we show how one can use this formalism to explicitly specify the nondeterministic interleaving of processes in a concurrent system. Such a specification will constructively result in a functional program involving all allowable interleaved executions of concurrent processes. As the second contribution of the paper, we introduce a verification method to prove safety properties of concurrent systems specified in the proposed Z-based formalism.