Integrating real-time into Spin: a prototype implementation

D. Bosnacki, D.R. Dams

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

Abstract

We present a discrete-time extension of Promela, a high level modelling language for the specification concurrent systems, and the associated Spin model checker. Our implementation is fully compatible with Spin's partial order reduction algorithm, which is indeed one of its main strengths. The real time package is for most part orthogonal to the other features of the tool, resulting in a modular extension. We have evaluated it by several experiments, with encouraging results.
Original languageEnglish
Title of host publicationFormal Description Techniques and Protocol Specification, Testing and Verification (Proceedings FORTE/PSTV'98, Paris, France, November 3-6, 1998)
EditorsS. Budkowski, A.R. Cavalli, E. Najm
Place of PublicationDordrecht
PublisherKluwer
Pages423-438
ISBN (Print)0-412-84760-4
Publication statusPublished - 1998

Publication series

NameIFIP Conference Proceedings
Volume135
ISSN (Print)1571-5736

Fingerprint

Dive into the research topics of 'Integrating real-time into Spin: a prototype implementation'. Together they form a unique fingerprint.

Cite this