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 -