A Refinement Calculus for Promela

The use of formal methods for developing software is increasing. However in many cases only a model of the system is validated against a set of specifications. The actual implementation may thus not correspond to the formal model. One approach to this problem is to directly verify the actual implementation. Another solution is to provide a refinement scheme for the model. In this paper we present a method for refining a given Promela model to an implementation in C. We show that our refinement preserves the temporal properties (specified in LTL) of the original model. We give a new dual action semantics for a minimal core of Promela (called Featherweight Promela). The operational semantics of Featherweight Promela makes it easier to define the refinement calculus as a set of structural rules. Based on our calculus, we derive syntax directed translation rules for refinement of Promela models to C programs. These translation rules are easier to apply and generate an implementation which is a refinement of the formal model. We have applied our approach on existing Promela models and a larger case study of the cardiac pacemaker challenge.