An Empirical Comparison of Formalisms for Modelling and Analysis of Dynamic Reconfiguration of Dependable Systems

TL;DR

This paper empirically compares three formal modeling formalisms—VDM, CPOGs, and CCS^dp—for their effectiveness in modeling and verifying dynamic reconfiguration in dependable systems through a case study of office workflow reconfiguration.

Contribution

It provides an empirical evaluation of three different formalisms for modeling and verifying dynamic reconfiguration, highlighting their strengths and limitations.

Findings

CPOGs effectively model reconfiguration processes.

VDM is suitable for detailed requirement verification.

CCS^dp offers a formal basis for dynamic process reconfiguration.

Abstract

This paper uses a case study to evaluate empirically three formalisms of different kinds for their suitability for the modelling and analysis of dynamic reconfiguration of dependable systems. The requirements on an ideal formalism for dynamic software reconfiguration are defined. The reconfiguration of an office workflow for order processing is described, and the requirements on the reconfiguration of the workflow are defined. The workflow is modelled using the Vienna Development Method ($\mathrm{VDM}$), conditional partial order graphs ($\mathrm{CPOGs}$), and the basic Calculus of Communicating Systems for dynamic process reconfiguration (basic $\mathrm{CCS^{dp}}$), and verification of the reconfiguration requirements is attempted using the models. The formalisms are evaluated according to their ability to model the reconfiguration of the workflow, to verify the requirements on the workflow's reconfiguration, and to meet the requirements on an ideal formalism.