DocumentCode :
2565550
Title :
A verified development of hardware using CSP/spl par/B
Author :
McEwan, Alistair A. ; Schneider, Steve
Author_Institution :
Dept. of Comput., Surrey Univ., Guildford
fYear :
2006
fDate :
27-30 July 2006
Firstpage :
81
Lastpage :
82
Abstract :
Summary form only given. In this paper, we show a combination of the process algebra CSP and the state-based formalism B, combined into a single notation called CSPparB (pronounced CSP parallel B) being used in the formal development of reconfigurable hardware, implemented in Handel-C. The use of CSPparB and associated fools is demonstrated using a significant, realistic application. This paper is the first recorded use of CSPparB in hardware development although it has been previously used for software. The contribution of this paper may be summarised as follows: demonstration of formal CSPparB development, guided by engineering intuition and domain knowledge; evidence that CSPparB forms a feasible technology upon which to build high assurance hardware systems; examples of proof techniques and tool usage for CSPparB in giving these high levels of assurance. Development is top-down and piece-wise: refinement is from an abstract sequential specification info 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 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 concl- - usion of this paper is that CSPparB forms 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
Keywords :
field programmable gate arrays; formal verification; hardware-software codesign; logic CAD; process algebra; reconfigurable architectures; theorem proving; B components; B-Toolkit theorem prover; CSP model-checker; CSPparB; FPGA platform; Handel-C; abstract sequential specification; concurrency; hardware development; process algebra; reconfigurable hardware; state-based formalism; Algebra; Application software; Calculus; Concurrent computing; Field programmable gate arrays; Hardware; Knowledge engineering; Safety; Software systems; Timing;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Formal Methods and Models for Co-Design, 2006. MEMOCODE '06. Proceedings. Fourth ACM and IEEE International Conference on
Conference_Location :
Napa, CA
Print_ISBN :
1-4244-0421-5
Type :
conf
DOI :
10.1109/MEMCOD.2006.1695904
Filename :
1695904
Link To Document :
بازگشت