Preliminary Design of BML: A Behavioral Interface Specification Language for Java Bytecode

Lilian Burdy; Marieke Huisman; Mariela Pavlova

doi:10.1007/978-3-540-71289-3_18

Preliminary Design of BML: A Behavioral Interface Specification Language for Java Bytecode

Lilian Burdy, Marieke Huisman, Mariela Pavlova

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

17 Citations (Scopus)

Abstract

We present the Bytecode Modeling Language (BML), the Java bytecode cousin of JML. BML allows the application developer to specify the behaviour of an application in the form of annotations, directly at the level of the bytecode. An extension of the class file format is defined to store the specification directly with the bytecode. This is a first step towards the development of a platform for Proof Carrying Code, where applications come together with their specification and a proof of correctness. BML is designed to be closely related with JML. In particular, JML specifications can be compiled into BML specifications. We briefly discuss the tools that are currently being developed for BML, and that will result in a tool set where an application can be validated throughout its development, both at source code and at bytecode level.

Original language	English
Title of host publication	Fundamental Approaches to Software Engineering, 10th International Conference, FASE 2007, Held as Part of the Joint European Conferences, on Theory and Practice of Software, ETAPS 2007, Braga, Portugal, March 24 - April 1, 2007, Proceedings
Editors	Matthew B. Dwyer, Antónia Lopes
Publisher	Springer
Pages	215-229
Number of pages	15
ISBN (Electronic)	978-3-540-71289-3
ISBN (Print)	978-3-540-71288-6
DOIs	https://doi.org/10.1007/978-3-540-71289-3_18
Publication status	Published - 2007
Externally published	Yes
Event	10th International Conference on Fundamental Approaches to Software Engineering, FASE 2007 - Braga, Portugal Duration: 24 Mar 2007 → 1 Apr 2007 Conference number: 10

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	4422

Conference

Conference	10th International Conference on Fundamental Approaches to Software Engineering, FASE 2007
Abbreviated title	FASE
Country/Territory	Portugal
City	Braga
Period	24/03/07 → 1/04/07

Access to Document

10.1007/978-3-540-71289-3_18

Cite this

Burdy, L., Huisman, M., & Pavlova, M. (2007). Preliminary Design of BML: A Behavioral Interface Specification Language for Java Bytecode. In M. B. Dwyer, & A. Lopes (Eds.), Fundamental Approaches to Software Engineering, 10th International Conference, FASE 2007, Held as Part of the Joint European Conferences, on Theory and Practice of Software, ETAPS 2007, Braga, Portugal, March 24 - April 1, 2007, Proceedings (pp. 215-229). (Lecture Notes in Computer Science; Vol. 4422). Springer. https://doi.org/10.1007/978-3-540-71289-3_18

Burdy, Lilian ; Huisman, Marieke ; Pavlova, Mariela. / Preliminary Design of BML: A Behavioral Interface Specification Language for Java Bytecode. Fundamental Approaches to Software Engineering, 10th International Conference, FASE 2007, Held as Part of the Joint European Conferences, on Theory and Practice of Software, ETAPS 2007, Braga, Portugal, March 24 - April 1, 2007, Proceedings. editor / Matthew B. Dwyer ; Antónia Lopes. Springer, 2007. pp. 215-229 (Lecture Notes in Computer Science).

@inproceedings{2d0c05f8aae740a88463cbc507eca6b4,

title = "Preliminary Design of BML: A Behavioral Interface Specification Language for Java Bytecode",

abstract = "We present the Bytecode Modeling Language (BML), the Java bytecode cousin of JML. BML allows the application developer to specify the behaviour of an application in the form of annotations, directly at the level of the bytecode. An extension of the class file format is defined to store the specification directly with the bytecode. This is a first step towards the development of a platform for Proof Carrying Code, where applications come together with their specification and a proof of correctness. BML is designed to be closely related with JML. In particular, JML specifications can be compiled into BML specifications. We briefly discuss the tools that are currently being developed for BML, and that will result in a tool set where an application can be validated throughout its development, both at source code and at bytecode level.",

author = "Lilian Burdy and Marieke Huisman and Mariela Pavlova",

year = "2007",

doi = "10.1007/978-3-540-71289-3_18",

language = "English",

isbn = "978-3-540-71288-6",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "215--229",

editor = "Dwyer, {Matthew B.} and Ant{\'o}nia Lopes",

booktitle = "Fundamental Approaches to Software Engineering, 10th International Conference, FASE 2007, Held as Part of the Joint European Conferences, on Theory and Practice of Software, ETAPS 2007, Braga, Portugal, March 24 - April 1, 2007, Proceedings",

address = "Germany",

note = "10th International Conference on Fundamental Approaches to Software Engineering, FASE 2007, FASE ; Conference date: 24-03-2007 Through 01-04-2007",

}

Burdy, L, Huisman, M & Pavlova, M 2007, Preliminary Design of BML: A Behavioral Interface Specification Language for Java Bytecode. in MB Dwyer & A Lopes (eds), Fundamental Approaches to Software Engineering, 10th International Conference, FASE 2007, Held as Part of the Joint European Conferences, on Theory and Practice of Software, ETAPS 2007, Braga, Portugal, March 24 - April 1, 2007, Proceedings. Lecture Notes in Computer Science, vol. 4422, Springer, pp. 215-229, 10th International Conference on Fundamental Approaches to Software Engineering, FASE 2007, Braga, Portugal, 24/03/07. https://doi.org/10.1007/978-3-540-71289-3_18

Preliminary Design of BML: A Behavioral Interface Specification Language for Java Bytecode. / Burdy, Lilian; Huisman, Marieke; Pavlova, Mariela.
Fundamental Approaches to Software Engineering, 10th International Conference, FASE 2007, Held as Part of the Joint European Conferences, on Theory and Practice of Software, ETAPS 2007, Braga, Portugal, March 24 - April 1, 2007, Proceedings. ed. / Matthew B. Dwyer; Antónia Lopes. Springer, 2007. p. 215-229 (Lecture Notes in Computer Science; Vol. 4422).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Preliminary Design of BML: A Behavioral Interface Specification Language for Java Bytecode

AU - Burdy, Lilian

AU - Huisman, Marieke

AU - Pavlova, Mariela

N1 - Conference code: 10

PY - 2007

Y1 - 2007

N2 - We present the Bytecode Modeling Language (BML), the Java bytecode cousin of JML. BML allows the application developer to specify the behaviour of an application in the form of annotations, directly at the level of the bytecode. An extension of the class file format is defined to store the specification directly with the bytecode. This is a first step towards the development of a platform for Proof Carrying Code, where applications come together with their specification and a proof of correctness. BML is designed to be closely related with JML. In particular, JML specifications can be compiled into BML specifications. We briefly discuss the tools that are currently being developed for BML, and that will result in a tool set where an application can be validated throughout its development, both at source code and at bytecode level.

AB - We present the Bytecode Modeling Language (BML), the Java bytecode cousin of JML. BML allows the application developer to specify the behaviour of an application in the form of annotations, directly at the level of the bytecode. An extension of the class file format is defined to store the specification directly with the bytecode. This is a first step towards the development of a platform for Proof Carrying Code, where applications come together with their specification and a proof of correctness. BML is designed to be closely related with JML. In particular, JML specifications can be compiled into BML specifications. We briefly discuss the tools that are currently being developed for BML, and that will result in a tool set where an application can be validated throughout its development, both at source code and at bytecode level.

U2 - 10.1007/978-3-540-71289-3_18

DO - 10.1007/978-3-540-71289-3_18

M3 - Conference contribution

SN - 978-3-540-71288-6

T3 - Lecture Notes in Computer Science

SP - 215

EP - 229

BT - Fundamental Approaches to Software Engineering, 10th International Conference, FASE 2007, Held as Part of the Joint European Conferences, on Theory and Practice of Software, ETAPS 2007, Braga, Portugal, March 24 - April 1, 2007, Proceedings

A2 - Dwyer, Matthew B.

A2 - Lopes, Antónia

PB - Springer

T2 - 10th International Conference on Fundamental Approaches to Software Engineering, FASE 2007

Y2 - 24 March 2007 through 1 April 2007

ER -

Burdy L, Huisman M, Pavlova M. Preliminary Design of BML: A Behavioral Interface Specification Language for Java Bytecode. In Dwyer MB, Lopes A, editors, Fundamental Approaches to Software Engineering, 10th International Conference, FASE 2007, Held as Part of the Joint European Conferences, on Theory and Practice of Software, ETAPS 2007, Braga, Portugal, March 24 - April 1, 2007, Proceedings. Springer. 2007. p. 215-229. (Lecture Notes in Computer Science). doi: 10.1007/978-3-540-71289-3_18

Preliminary Design of BML: A Behavioral Interface Specification Language for Java Bytecode

Abstract

Publication series

Conference

Access to Document

Fingerprint

Cite this