Title :
Using CSP to develop trustworthy hardware
Author :
Moore, Andrew P.
Author_Institution :
US Naval Res. Lab., Washington, DC, USA
Abstract :
An overview of a method for formalizing critical system requirements and decomposing them into requirements of the system components and a minimal, possibly empty, set of synchronization requirements is presented. The trace model of communicating sequential processes (CSPs) is the basis for the formal method, and the EHDM verification system is the basis for mechanizing proofs. The results of the application of this method to the top-level implementation of an error-detecting character repeater are discussed. The critical requirements of the repeater are decomposed into the requirements of its components. Provided that the components meet their derived requirements, the repeater has been proven to meet its critical requirements.<>
Keywords :
computer interfaces; formal logic; performance evaluation; program verification; quality control; repeaters; systems analysis; CSP; EHDM verification system; communicating sequential processes; critical system requirements; error-detecting character repeater; formal method; synchronization requirements; system components; top-level implementation; trace model; trustworthy hardware; Circuit simulation; Computational modeling; Computer languages; Concurrent computing; Hardware design languages; Integrated circuit synthesis; Integrated circuit technology; Laboratories; Repeaters; Testing;
Conference_Titel :
Computer Assurance, 1990. COMPASS '90, Systems Integrity, Software Safety and Process Security., Proceedings of the Fifth Annual Conference on
Conference_Location :
Gaithersburg, MD, USA
DOI :
10.1109/CMPASS.1990.175409
