Building extensible specifications and implementations of promela with AbleP

Yogesh Mali; Eric Van Wyk

doi:10.1007/978-3-642-22306-8_8

Building extensible specifications and implementations of promela with AbleP

Yogesh Mali, Eric Van Wyk

Computer Science and Engineering

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

5 Scopus citations

Abstract

This paper describes how new language features can be seamlessly added to an extensible specification of Promela to provide new (domain-specific) notations and analyses to the engineer. This is accomplished using ableP, an extensible specification and implementation of Promela, the modeling language used by the spin model checker. Language extensions described here include an enhanced select-statement, a convenient tabular notation for boolean expressions, a notion of discrete time, and extended type checking. ableP and the extensions are developed using the Silver attribute grammar system and the Copper parser and scanner generator. These tools support the modular development and composition of language extensions so that independently developed extensions can be imported into ableP by an engineer with little knowledge of language design and implementation issues.

Original language	English (US)
Title of host publication	Model Checking Software - 18th International SPIN Workshop, Proceedings
Pages	108-125
Number of pages	18
DOIs	https://doi.org/10.1007/978-3-642-22306-8_8
State	Published - Jul 21 2011
Event	18th International SPIN Workshop on Model Checking of Software, SPIN 2011 - Snowbird, UT, United States Duration: Jul 14 2011 → Jul 15 2011

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	6823 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Other

Other	18th International SPIN Workshop on Model Checking of Software, SPIN 2011
Country	United States
City	Snowbird, UT
Period	7/14/11 → 7/15/11

Access

10.1007/978-3-642-22306-8_8

Fingerprint Dive into the research topics of 'Building extensible specifications and implementations of promela with AbleP'. Together they form a unique fingerprint.

Cite this

Mali, Y., & Van Wyk, E. (2011). Building extensible specifications and implementations of promela with AbleP. In Model Checking Software - 18th International SPIN Workshop, Proceedings (pp. 108-125). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 6823 LNCS). https://doi.org/10.1007/978-3-642-22306-8_8

Building extensible specifications and implementations of promela with AbleP. / Mali, Yogesh; Van Wyk, Eric.

Model Checking Software - 18th International SPIN Workshop, Proceedings. 2011. p. 108-125 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 6823 LNCS).

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

Mali, Y & Van Wyk, E 2011, Building extensible specifications and implementations of promela with AbleP. in Model Checking Software - 18th International SPIN Workshop, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 6823 LNCS, pp. 108-125, 18th International SPIN Workshop on Model Checking of Software, SPIN 2011, Snowbird, UT, United States, 7/14/11. https://doi.org/10.1007/978-3-642-22306-8_8

Mali Y, Van Wyk E. Building extensible specifications and implementations of promela with AbleP. In Model Checking Software - 18th International SPIN Workshop, Proceedings. 2011. p. 108-125. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-642-22306-8_8

@inproceedings{77b41ec026bc4c098268b9a41fa834b7,

title = "Building extensible specifications and implementations of promela with AbleP",

abstract = "This paper describes how new language features can be seamlessly added to an extensible specification of Promela to provide new (domain-specific) notations and analyses to the engineer. This is accomplished using ableP, an extensible specification and implementation of Promela, the modeling language used by the spin model checker. Language extensions described here include an enhanced select-statement, a convenient tabular notation for boolean expressions, a notion of discrete time, and extended type checking. ableP and the extensions are developed using the Silver attribute grammar system and the Copper parser and scanner generator. These tools support the modular development and composition of language extensions so that independently developed extensions can be imported into ableP by an engineer with little knowledge of language design and implementation issues.",

author = "Yogesh Mali and {Van Wyk}, Eric",

year = "2011",

month = jul,

day = "21",

doi = "10.1007/978-3-642-22306-8_8",

language = "English (US)",

isbn = "9783642223051",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

pages = "108--125",

booktitle = "Model Checking Software - 18th International SPIN Workshop, Proceedings",

note = "18th International SPIN Workshop on Model Checking of Software, SPIN 2011 ; Conference date: 14-07-2011 Through 15-07-2011",

}

TY - GEN

T1 - Building extensible specifications and implementations of promela with AbleP

AU - Mali, Yogesh

AU - Van Wyk, Eric

PY - 2011/7/21

Y1 - 2011/7/21

N2 - This paper describes how new language features can be seamlessly added to an extensible specification of Promela to provide new (domain-specific) notations and analyses to the engineer. This is accomplished using ableP, an extensible specification and implementation of Promela, the modeling language used by the spin model checker. Language extensions described here include an enhanced select-statement, a convenient tabular notation for boolean expressions, a notion of discrete time, and extended type checking. ableP and the extensions are developed using the Silver attribute grammar system and the Copper parser and scanner generator. These tools support the modular development and composition of language extensions so that independently developed extensions can be imported into ableP by an engineer with little knowledge of language design and implementation issues.

AB - This paper describes how new language features can be seamlessly added to an extensible specification of Promela to provide new (domain-specific) notations and analyses to the engineer. This is accomplished using ableP, an extensible specification and implementation of Promela, the modeling language used by the spin model checker. Language extensions described here include an enhanced select-statement, a convenient tabular notation for boolean expressions, a notion of discrete time, and extended type checking. ableP and the extensions are developed using the Silver attribute grammar system and the Copper parser and scanner generator. These tools support the modular development and composition of language extensions so that independently developed extensions can be imported into ableP by an engineer with little knowledge of language design and implementation issues.

UR - http://www.scopus.com/inward/record.url?scp=79960414854&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=79960414854&partnerID=8YFLogxK

U2 - 10.1007/978-3-642-22306-8_8

DO - 10.1007/978-3-642-22306-8_8

M3 - Conference contribution

AN - SCOPUS:79960414854

SN - 9783642223051

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 108

EP - 125

BT - Model Checking Software - 18th International SPIN Workshop, Proceedings

T2 - 18th International SPIN Workshop on Model Checking of Software, SPIN 2011

Y2 - 14 July 2011 through 15 July 2011

ER -