Title :
Temporal Refinement in Co-Design
Author :
Aljer, Ammar ; Boulanger, Jean-Louis ; Devienne, Philippe
Author_Institution :
HeuDiaSyC Lab., Technol. Univ. of Compiegne, Compiegne
Abstract :
This paper shows how it is possible to employ refinement concept of B formal method in hardware design. The structural, logical and temporal properties of a Hardware Description Language that is enriched with annotations of the Property Specification language are projected into B model. Then the generated B image is analyzed, using B method tools, in order to prove the initial properties. This technique produces a correct by design component.
Keywords :
hardware description languages; logic CAD; B formal method; hardware description language; hardware design; property specification language; temporal refinement; Circuits; Design methodology; Embedded system; Formal specifications; Hardware design languages; Image generation; Laboratories; Logic; Paper technology; Specification languages; B method; PSL; Refinement; VHDL;
Conference_Titel :
Information and Communication Technologies: From Theory to Applications, 2008. ICTTA 2008. 3rd International Conference on
Conference_Location :
Damascus
Print_ISBN :
978-1-4244-1751-3
Electronic_ISBN :
978-1-4244-1752-0
DOI :
10.1109/ICTTA.2008.4530351
