A verified development of hardware using CSP||B
McEwan, AA and Schneider, S (2006) A verified development of hardware using CSP||B In: 4th ACM/IEEE International Conference on Formal Methods and Models for Co-Design, 2006-07-27 - 2006-07-30, Napa Valley, CA.
memocode06.pdf - Accepted Version
Available under License : See the attached licence file.
Plain Text (licence)
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.
|Item Type:||Conference or Workshop Item (Paper)|
|Divisions :||Faculty of Engineering and Physical Sciences > Computing Science|
|Date :||11 September 2006|
|Identification Number :||10.1109/MEMCOD.2006.1695904|
|Depositing User :||Symplectic Elements|
|Date Deposited :||29 Sep 2011 11:07|
|Last Modified :||23 Sep 2013 18:45|
Actions (login required)
Downloads per month over past year