Checking JML-encoded finite state machine properties

Ijaz Ahmed; Nestor Catano

doi:10.1109/icacs.2018.8333496

Checking JML-encoded finite state machine properties

Ijaz Ahmed
, Nestor Catano

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

1 Citation (Scopus)

Abstract

This paper presents a recent work on the encoding of JML specifications as Finite State Machines (FSM). We show how these specifications can be translated to the input language of the Pulse tool and how they can be checked with the tool. The output given by the tool can help programmers to analyse the concurrent behaviour of the FSM and therefore some errors of the JML specification that originated it. We define a set of rules that encode the translation of a subset of the JML language into the input language of Pulse. We present various translation examples and discuss results.

Original language	Undefined/Unknown
Title of host publication	2018 International Conference on Advancements in Computational Sciences (ICACS)
Publisher	IEEE Computer Society
Pages	1–9
ISBN (Electronic)	9781538621721
ISBN (Print)	9781538621738
DOIs	https://doi.org/10.1109/icacs.2018.8333496
Publication status	Published - 9 Apr 2018
Externally published	Yes

Access to Document

10.1109/icacs.2018.8333496

Cite this

@inproceedings{ec4a4b13db3f4a5ea7db8c9ed766dc8a,

title = "Checking JML-encoded finite state machine properties",

abstract = "This paper presents a recent work on the encoding of JML specifications as Finite State Machines (FSM). We show how these specifications can be translated to the input language of the Pulse tool and how they can be checked with the tool. The output given by the tool can help programmers to analyse the concurrent behaviour of the FSM and therefore some errors of the JML specification that originated it. We define a set of rules that encode the translation of a subset of the JML language into the input language of Pulse. We present various translation examples and discuss results.",

author = "Ijaz Ahmed and Nestor Catano",

year = "2018",

month = apr,

day = "9",

doi = "10.1109/icacs.2018.8333496",

language = "Heb ei ddiffinio/Anhysbys",

isbn = "9781538621738",

pages = "1–9",

booktitle = "2018 International Conference on Advancements in Computational Sciences (ICACS)",

publisher = "IEEE Computer Society",

}

TY - GEN

T1 - Checking JML-encoded finite state machine properties

AU - Ahmed, Ijaz

AU - Catano, Nestor

PY - 2018/4/9

Y1 - 2018/4/9

N2 - This paper presents a recent work on the encoding of JML specifications as Finite State Machines (FSM). We show how these specifications can be translated to the input language of the Pulse tool and how they can be checked with the tool. The output given by the tool can help programmers to analyse the concurrent behaviour of the FSM and therefore some errors of the JML specification that originated it. We define a set of rules that encode the translation of a subset of the JML language into the input language of Pulse. We present various translation examples and discuss results.

AB - This paper presents a recent work on the encoding of JML specifications as Finite State Machines (FSM). We show how these specifications can be translated to the input language of the Pulse tool and how they can be checked with the tool. The output given by the tool can help programmers to analyse the concurrent behaviour of the FSM and therefore some errors of the JML specification that originated it. We define a set of rules that encode the translation of a subset of the JML language into the input language of Pulse. We present various translation examples and discuss results.

U2 - 10.1109/icacs.2018.8333496

DO - 10.1109/icacs.2018.8333496

M3 - Cyfraniad mewn cynhadledd

SN - 9781538621738

SP - 1

EP - 9

BT - 2018 International Conference on Advancements in Computational Sciences (ICACS)

PB - IEEE Computer Society

ER -