A verified development of hardware using CSP||B

In this paper, we show a combination of the process algebra CSP and the state-based formalism B, combined into a single notation called CSP________B (pronounced CSP parallel B) being used in the formal development of reconfigurable hardware, implemented in. Handel-C. The use of CSP________B and associated tools is demonstrated using a significant, realistic application. This paper is the first recorded use of CSP________B in hardware development although it has been previously used for software. The contribution of this paper may be summarised as follows:Demonstration of formal CSP________B development, guided by engineering intuition and domain knowledge.Evidence that CSP________B forms a feasible technology upon which to build high assurance hardware systems.Examples of proof techniques and tool usage for CSP________B in giving these high levels of assurance.Development is top-down and piece-wise: refinement is from. an abstract sequential specification into a highly concurrent implementation. Justification of refinement steps employs the use of control loop invariants, which are used to show the consistency of the interaction of the CSP and the B components.In introducing concurrency, additional requirements appear which could be met by software, dedicated hardware components, or by custom hardware on an FPGA. The piece-wise nature of the development allow for this choice to be postponed while other components are implemented- possibly in different technologies. The choice of where concurrency may be introduced in order to meet timing requirements, whilst still attaining reasonable area usage is guided by a knowledge of the application domain and the target FPGA platform. Safety and functional properties of the abstract specification are automatically verified; theoretical results concerning refinement guarantee that these hold for the implementation. Proof obligations are discharged using the CSP model-checker FDR and the theorem prover B-Toolkit.The central conclusion of this paper is that CSP________B forrns the basis of a valid technology for the exploration and development of high assurance hardware and software systems. Further research is to investigate co-design, understand how a design calculus may be incorporated, and how further automatic tool support may be provided in discharging CLI proofs