Leiden University Scholarly Publications

Persistent URL of this record https://hdl.handle.net/1887/3485524

In Collections

This item can be found in the following collections:

Feng, H.; Bonsangue, M.M.; Lion, B. (2022)

From symbolic constraint automata to Promela

Article / Letter to editor
In this paper, we study a subclass of constraint automata with local variables. The fragment denotes an executable subset of constraint automata for which synchronization and data constraints are expressed in an imperative guarded command style, instead of a denotational style as in the coordination language Reo. To demonstrate the executability property, we provide a translation scheme from symbolic constraint automata to Promela, the language of the model checker Spin. As a proof of concept, we model in Reo a software defined network circuit, and use the Spin model checker to verify that our model satisfies some temporal properties. (C) 2022 The Author(s). Published by Elsevier Inc.
All authors
Feng, H.; Bonsangue, M.M.; Lion, B.
Date
2022-08-01
Journal
Journal of Logical and Algebraic Methods in Programming
Volume
128
DOI
doi:10.1016/j.jlamp.2022.100794