Chapter 17. Embedded C Code


“The purpose of analysis is not to compel belief but rather to suggest doubt.”

 --(Imre Lakatos, Proofs and Refutations)

SPIN, versions 4.0 and later, support the inclusion of embedded C code into PROMELA models through the following five new primitives:

c_expr, c_code, c_decl, c_state, c_track

The purpose of these new primitives is primarily to provide support for automatic model extraction from C code. This means that it is not the intent of these extensions to be used in manually constructed models. The primitives provide a powerful extension, opening SPIN models to the full power of, and all the dangers of, arbitrary C code. The contents of the embedded code fragments cannot be checked by SPIN, neither in the parsing ...

Get Spin Model Checker, The: Primer and Reference Manual now with O’Reilly online learning.

O’Reilly members experience live online training, plus books, videos, and digital content from 200+ publishers.