Building extensible specifications and implementations of promela with AbleP

Yogesh Mali, Eric Van Wyk

Research output: Chapter in Book/Report/Conference proceedingConference contribution

7 Scopus citations


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 languageEnglish (US)
Title of host publicationModel Checking Software - 18th International SPIN Workshop, Proceedings
Number of pages18
StatePublished - 2011
Event18th International SPIN Workshop on Model Checking of Software, SPIN 2011 - Snowbird, UT, United States
Duration: Jul 14 2011Jul 15 2011

Publication series

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


Other18th International SPIN Workshop on Model Checking of Software, SPIN 2011
Country/TerritoryUnited States
CitySnowbird, UT

Bibliographical note

Funding Information:
★ This material is based on work partially supported by NSF Awards No. 0905581 and No. 1047961 and DARPA and the United States Air Force (Air Force Research Lab) under Contract No. FA8650-10-C-7076.


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

Cite this