2022-08-01
From symbolic constraint automata to Promela
Publication
Publication
Journal of Logical and Algebraic Methods in Programming , Volume 128 p. 100794:1- 100794:19
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.
| Additional Metadata | |
|---|---|
| doi.org/10.1016/j.jlamp.2022.100794 | |
| Journal of Logical and Algebraic Methods in Programming | |
| Organisation | Centrum Wiskunde & Informatica, Amsterdam (CWI), The Netherlands |
|
Feng, H., Bonsangue, M., & Lion, B. (2022). From symbolic constraint automata to Promela. Journal of Logical and Algebraic Methods in Programming, 128, 100794:1–100794:19. doi:10.1016/j.jlamp.2022.100794 |
|
