Abstract
We have demonstrated that clocked synchronous logic can be developed within a formal software framework. The advantage of this approach is that it allows abstraction, animation and proof of refinement. The B-Toolkit supports these activities and has a VHDL generator. The validation tests can be agreed and carried out during animation early in the development cycle (a common technique in software). Proof of refinement may be important for critical applications. The AWE plans to explore the proof of their Arming System Processor with the techniques over-viewed in this paper.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Abrial, J-R. The B-Book: Assigning Programs to Meaning, Cambridge University Press, 1997.
Ashenden, P. T. “The Designer’s Guide to VHDL”, Morgan Kaufmann, 1996.
Breuer P. T., Kloos C. D., Lopez A M, Madrid N M (1997) (University Politecnica de Madrid) “A Refinement Calculus for the Synthesis of Verified Hardware Descriptions in VHDL”, A CM Transactions on Programming Languages and Systems, Vol. 19, No. 4, Pages 586–616, July 1997.
Draper Jonathan. “Applying the B-Method to Avionics Software: An Initial Report on the MIST Project”, GEC-Marconi Avionics, Airport Works Rochester, ME1 2XX, UK (Jonathan.Draper@gecm.com), 1997.
Ifill W. “MSc Thesis: Formal Development of An Example Processor (AEP) in AMN, C and VHDL”, Computer Science Department, Royal Holloway, University of London, Egham, Surrey TW20 OEX, 1999.
MoD. Def.-Stan.: “00–55 Requirements for Safety Related Software in Defence Equipment”, Issue 2, 1 August 1997.
Schneider S CS357: Advanced Methods for Software Engineering Lecture Notes, Computer Science Department, Royal Holloway, University
Sorensen I. “Translation Rules: AMN to VHDL”, B-Core (UK) Ltd. (delivered to AWE) 1st Aug 1998.
Sorensen I, Neilson D. “Towards Zero Defect Software”, HIS’99.
Sorensen I. “The Formal Design of ASP”, B-Core (UK) Ltd, (delivered to AWE), 27th. April 1999.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer Science+Business Media New York
About this chapter
Cite this chapter
Ifill, W., Sorensen, I., Schneider, S. (2001). The Use of B to Specify, Design and Verify Hardware. In: Winter, V.L., Bhattacharya, S. (eds) High Integrity Software. The Kluwer International Series in Engineering and Computer Science, vol 577. Springer, Boston, MA. https://doi.org/10.1007/978-1-4615-1391-9_3
Download citation
DOI: https://doi.org/10.1007/978-1-4615-1391-9_3
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4613-5530-4
Online ISBN: 978-1-4615-1391-9
eBook Packages: Springer Book Archive