Abstract
We present a new methodology that permits to reuse an existing hardware component that has not been developed within the B framework while maintaining a correct design flow. It consists of writing a specification of the component in B and proving that the VHDL description of the component implements the specification using the ACL2 system. This paper focuses on the translation of the B specification into ACL2.
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 meanings. CUP, Cambridge (1996)
Abrial, J.-R., Mussat, L.: Introducing Dynamic Constraints in B. In: Bert, D. (ed.) B 1998. LNCS, vol. 1393, pp. 83–128. Springer, Heidelberg (1998)
Abrial, J.-R., Cansell, D., Méry, D.: A mechanically proved and incremental development of ieee 1394 tree identify protocol. Formal Aspects of Computing 14(3), 215–227 (2003)
Aljer, A., Devienne, P., Tison, S., Boulanger, J.-L., Mariano, G.: B-HDL: Circuit Design in B. In: ACSD 2003, International conference on Application of Concurrency to System Design, pp. 241–242 (2003)
Dunne, S.: A Theory of Generalised Substitutions. In: Bert, D., Bowen, J. P., Henson, M. C., Robinson, K. (eds.) B 2002 and ZB 2002. LNCS, vol. 2272, pp. 270–290. Springer, Heidelberg (2002)
European Organisation for Civil Aviation Equipment, http://www.eurocae.org/
Fox, A.C.J.: Formal specification and verification of ARM6. In: Basin, D., Wolff, B. (eds.) TPHOLs 2003. LNCS, vol. 2758, pp. 25–40. Springer, Heidelberg (2003)
Fuchs, M., Mendler, M.: A Functional Semantics for Delta-Delay VHDL Based on FOCUS. In: Kloos, C.D., Breuer, P.T. (eds.) Formal Semantics for VHDL, pp. 9–42. Kluwer Academic Publishers, Dordrecht (1995)
Hallerstede, S., Zimmermann, Y.: Circuit Design by refinement in EventB. In: Proc. of FDL 2004 (2004)
Hazelhurst, S., Seger, C.-J.H.: Symbolic Trajectory Evaluation. In: Kropf, T. (ed.) Formal Hardware Verification. LNCS, vol. 1287, pp. 3–78. Springer, Heidelberg (1997)
IEEE (ed.): Standard VHDL - Language Reference Manual. IEEE Computer Society Press, USA (1988)
International Electrotechnical Commission, http://www.iec.ch/61508/
Kaufmann, M., Manolios, P., Moore, J.S.: Computer-Aided reasoning: ACL2 An approach, vol. 1. Kluwer Academic Publishers, Dordrecht (2000)
Kaufmann, M., Manolios, P., Moore, J.S.: Computer-Aided reasoning: ACL2 Case Studies, vol. 2. Kluwer Academic Publishers, Dordrecht (2000)
PUSSEE project IST-2000-30103 (2004), http://www.keesda.com/pussee/
Radio Technical Commission for Aeronautics, http://www.rtca.org/
Mermet, J.: UML-B - Specification for Proven Embedded Systems Design. Kluwer Academic Publishers, Bosten (2004) ISBN 1-4020-2866-0
Russinoff, D.M.: A Case Study in Formal Verification of Register-Transfer Logic with ACL2: The Floating Point Adder of the AMD Athlon Processor. In: Johnson, S.D., Hunt Jr., W.A. (eds.) FMCAD 2000. LNCS, vol. 1954, pp. 3–36. Springer, Heidelberg (2000)
SAE International. SAE J1708 revised OCT93, serial data communication between microcomputer systems in heavy-duty vehicule applications (1993), www.sae.org
Srivas, M., Rueß, H., Cyrluk, D.: Hardware Verification Using PVS. In: Kropf, T. (ed.) Formal Hardware Verification. LNCS, vol. 1287, pp. 156–205. Springer, Heidelberg (1997)
Toma, D., Borrione, D.: SHA formalization. In: ACL2 Workshop, USA (2003)
Toma, D., Borrione, D., Al-Sammane, G.: Combining several paradigms for circuit validation and verification. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol. 3362, pp. 229–249. Springer, Heidelberg (2005)
Zimmermann, Y., Hallerstede, S., Cansell, D.: Formal modelling of electronic circuits using event-B, case study: SAE J708 serial communication link. In: Mermet, J. (ed.) UML-B - Specification for Proven Embedded Systems Design. Kluwer Academic Publishers, Boston (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Zimmermann, Y., Toma, D. (2005). Component Reuse in B Using ACL2. In: Treharne, H., King, S., Henson, M., Schneider, S. (eds) ZB 2005: Formal Specification and Development in Z and B. ZB 2005. Lecture Notes in Computer Science, vol 3455. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11415787_17
Download citation
DOI: https://doi.org/10.1007/11415787_17
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-25559-8
Online ISBN: 978-3-540-32007-4
eBook Packages: Computer ScienceComputer Science (R0)