nach oben

Erschienen in:

2003 | OriginalPaper | Buchkapitel

Adaptable Translator of B Specifications to Embedded C Programs

verfasst von : Didier Bert, Sylvain Boulmé, Marie-Laure Potet, Antoine Requet, Laurent Voisin

Erschienen in: FME 2003: Formal Methods

Verlag: Springer Berlin Heidelberg

Enthalten in: Professional Book Archive

Zugang erhalten

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract.

This paper presents the results of the RNTL BOM project, which aimed to develop an approach to generate efficient code from B formal developments. The target domain is smart card applications, in which memory and code size is an important factor. The results detailed in this paper are a new architecture of the translation process, a way to adapt the B ₀ language in order to include types of the target language and a set of validated optimizations. An assessment of the proposed approach is given through a case study, relative to the development of a Java Card Virtual Machine environment.

Vorheriges Kapitel Proving the Shalls

Nächstes Kapitel Integrating Model-Checking Architectural Analysis and Validation in a Real Software Life-Cycle

Abrial, J.-R.: The B Book - Assigning Programs to Meanings. Cambridge University Press, Cambridge (August 1996)CrossRef

Behm, P., Benoit, P., Faivre, A., Meynadier, J.-M.: Météor: A Successful Application of B in a Large Project. In: Wing, J.M., Woodcock, J.C.P., Davies, J. (eds.) FM 1999. LNCS, vol. 1708, pp. 369–388. Springer, Heidelberg (1999)CrossRef

Behm, P., Burdy, L., Meynadier, J.-M.: Well Defined B. In: Bert, D. (ed.) B 1998. LNCS, vol. 1393, p. 29. Springer, Heidelberg (1998)CrossRef

Bert, D.: Étude de la traduction B0 vers C: Conventions de nommage. Technical Report D10 (2003), http://lifc.univ-fcomte.fr/~tatibouet/WEBBOM

Bert, D., Potet, M.-L., Rouzaud, Y.: A Study on Components and Assembly Primitives in B. In: Habrias, H. (ed.) Proceedings of the 1st Conference on the B method, pp. 47–62. IRIN, Nantes (1996)

Casset, L.: Development of an Embedded Verifier for Java Card Byte Code using Formal Methods. In: Eriksson, L.-H., Lindsay, P.A. (eds.) FME 2002. LNCS, vol. 2391, pp. 290–309. Springer, Heidelberg (2002)CrossRef

Casset, L., Burdy, L., Requet, A.: Formal Development of an embedded verifier for Java Card Byte Code. In: International Conference on Dependable Systems & Networks (DSN), Washington, D.C., USA, June 2002, pp. 51–58. IEEE Computer Society, Los Alamitos (2002)CrossRef

Casset, L., Lanet, J.-L.: How to Formally Specify the Java Bytecode Semantics using the B Method, Lisbon, June 1999, pp. 1–8 (1999)

ClearSy. B Language Reference Manual, version 1.8.5. Technical report, ClearSy System Engineering (2001), URL: http://www.clearsy.com/

10.

Lanet, J.-L., Requet, A.: Formal Proof of Smart Card Applets Correctness. In: Schneier, B., Quisquater, J.-J. (eds.) CARDIS 1998. LNCS, vol. 1820, pp. 85–97. Springer, Heidelberg (2000)CrossRef

11.

Morgan, C.: On the Refinement Calculus. Springer, Heidelberg (1992)

12.

Motré, S.: A B automaton for Authentification Process. In: WITS: Workshop on Issues in the Theory of Security, Genève, Suisse (2000)

13.

Motré, S., Téri, C.: Using Formal and Semi-Formal Methods for a Common Criteria Evaluation. In: EUROSMART, Marseille, France (2000)

14.

Pnueli, A., Siegel, M., Shtrichman, O.: Translation Validation for Synchronous Languages. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol. 1443, pp. 235–246. Springer, Heidelberg (1998)CrossRef

15.

Potet, M.-L.: Spécifications et développements formels: Etude des aspects compositionnels dans la méthode B. Habilitation à Diriger des Recherches, INPG (2002)

16.

Potet, M.-L., Rouzaud, Y.: Composition and Refinement in the B method. In: Bert, D. (ed.) B 1998. LNCS, vol. 1393, pp. 46–65. Springer, Heidelberg (1998)CrossRef

17.

Requet, A.: A B Model for Ensuring Soundness of the Java Card Virtual Machine (Extended Version). Science of Computer Programming, Elsevier Science 46(3), 283–306 (2003)CrossRef

18.

Requet, A.: Évaluation du traducteur C. Technical Report D11 (2003), http://lifc.univfcomte.fr/~tatibouet/WEBBOM

19.

International Standard. Programming languages - C. ISO/IEC 9899:1999 (E)

20.

Coq Development Team. The Coq Proof Assistant -Reference Manual, Version 7.4. INRIA (February 2003), http://coq.inria.fr/doc-fra.html

Titel: Adaptable Translator of B Specifications to Embedded C Programs
verfasst von: Didier Bert
Sylvain Boulmé
Marie-Laure Potet
Antoine Requet
Laurent Voisin
Verlag: Springer Berlin Heidelberg
Buch: FME 2003: Formal Methods
Print ISBN: 978-3-540-40828-4

Electronic ISBN: 978-3-540-45236-2

Copyright-Jahr: 2003
DOI: https://doi.org/10.1007/978-3-540-45236-2_7

Springer Professional

Abstract.