Formal object-oriented development of a voting system test oracle

J. Paul Gibson; Jean Luc Raffy; Eric Lallet

doi:10.1007/s11334-011-0167-y

Formal object-oriented development of a voting system test oracle

J. Paul Gibson
, Jean Luc Raffy
, Eric Lallet

T and MSP

Research output: Contribution to journal › Article › peer-review

Abstract

We report on the formal development of a test oracle for an electronic-voting system, detailing our approach which was based on a lightweight integration of Event-B, UML, and Java. This lightweight integration focuses on a coherent development process rather than on formal integration at the model/language level. We then briefly review alternative development approaches involving the use of JML and OCL. We conclude that the use of the OCL would offer few benefits, if any, in our formal development process.

Original language	English
Pages (from-to)	237-245
Number of pages	9
Journal	Innovations in Systems and Software Engineering
Volume	7
Issue number	4
DOIs	https://doi.org/10.1007/s11334-011-0167-y
Publication status	Published - 1 Dec 2011
Externally published	Yes

Keywords

Event-B
JUnit
Java
UML

Access to Document

10.1007/s11334-011-0167-y

Cite this

@article{e839310eb41c41f6a9e3d3806ed28fe0,

title = "Formal object-oriented development of a voting system test oracle",

abstract = "We report on the formal development of a test oracle for an electronic-voting system, detailing our approach which was based on a lightweight integration of Event-B, UML, and Java. This lightweight integration focuses on a coherent development process rather than on formal integration at the model/language level. We then briefly review alternative development approaches involving the use of JML and OCL. We conclude that the use of the OCL would offer few benefits, if any, in our formal development process.",

keywords = "Event-B, JUnit, Java, UML",

author = "Gibson, \{J. Paul\} and Raffy, \{Jean Luc\} and Eric Lallet",

year = "2011",

month = dec,

day = "1",

doi = "10.1007/s11334-011-0167-y",

language = "English",

volume = "7",

pages = "237--245",

journal = "Innovations in Systems and Software Engineering",

issn = "1614-5046",

number = "4",

}

TY - JOUR

T1 - Formal object-oriented development of a voting system test oracle

AU - Gibson, J. Paul

AU - Raffy, Jean Luc

AU - Lallet, Eric

PY - 2011/12/1

Y1 - 2011/12/1

N2 - We report on the formal development of a test oracle for an electronic-voting system, detailing our approach which was based on a lightweight integration of Event-B, UML, and Java. This lightweight integration focuses on a coherent development process rather than on formal integration at the model/language level. We then briefly review alternative development approaches involving the use of JML and OCL. We conclude that the use of the OCL would offer few benefits, if any, in our formal development process.

AB - We report on the formal development of a test oracle for an electronic-voting system, detailing our approach which was based on a lightweight integration of Event-B, UML, and Java. This lightweight integration focuses on a coherent development process rather than on formal integration at the model/language level. We then briefly review alternative development approaches involving the use of JML and OCL. We conclude that the use of the OCL would offer few benefits, if any, in our formal development process.

KW - Event-B

KW - JUnit

KW - Java

KW - UML

UR - https://www.scopus.com/pages/publications/80855130550

U2 - 10.1007/s11334-011-0167-y

DO - 10.1007/s11334-011-0167-y

M3 - Article

AN - SCOPUS:80855130550

SN - 1614-5046

VL - 7

SP - 237

EP - 245

JO - Innovations in Systems and Software Engineering

JF - Innovations in Systems and Software Engineering

IS - 4

ER -

Formal object-oriented development of a voting system test oracle

Abstract

Keywords

Access to Document

Other files and links

Fingerprint

Cite this