Implementing discrete time in Promela and Spin

MaRDI QIDQ2763581zbMATH OpenFDO

Authors Dragan Bošnjački

Publication date 20 January 2002

zbMATH Keywords

discrete timeimplementationPromelaSpin

Mathematics Subject Classification ID

Parallel algorithms in computer science (68W10)

Review text

An implementation of discrete time in Promela and Spin is described. (Promela is a high level modeling language for specification of concurrent systems. Originally, Promela and Spin have been developed for analysis and validation of communication protocols.) In order to obtain better quantitative estimation for the interval between the events, time is divided in slices indexed by natural numbers. Promela predefined statement \textbf{timeout} is adopted as a mechanism for process synchronization. The main part of implementation is described by using Promela macro definitions. PAR protocol is used for the demonstration the usage of new-developed constructs. The whole implementation should be tested and examined in more details.NEWLINENEWLINEFor the entire collection see [Zbl 0977.00022].

Recommendations

• Translation of timed Promela to timed automata with discrete data
• Principles of the SPIN model checker. Foreword by Gerard J. Holzmann
• scientific article; zbMATH DE number 1982206
• scientific article; zbMATH DE number 1497794
• scientific article; zbMATH DE number 1629963

Cited in

(1)

• Translation of timed Promela to timed automata with discrete data

This page was built for publication: Implementing discrete time in Promela and Spin

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2763581)