The language ¿ has been developed for modeling of industrial systems. Its simulator has been successfully used in many industrial areas for obtaining performance measures. For functional analysis simulation is less applicable and such analysis can be done in other environments. The purpose of this paper is to describe an automatic translator from ¿ to Promela, the input language of the well known model-checker Spin. We highlight the differences between the two languages and show, in a step by step manner, how some of them can be resolved. We conclude by giving a translation scheme and apply the translator in a small industrial case study.
|Title of host publication||Formal Methods and Software Engineering (Proceedings 8th International Conference on Formal Engineering Methods, ICFEM 2006, Macao, China, November 1-3, 2006)|
|Editors||Z. Liu, Z. He|
|Place of Publication||Berlin|
|Publication status||Published - 2006|
|Name||Lecture Notes in Computer Science|
Trcka, N. (2006). Verifying Chi models of industrial systems with Spin. In Z. Liu, & Z. He (Eds.), Formal Methods and Software Engineering (Proceedings 8th International Conference on Formal Engineering Methods, ICFEM 2006, Macao, China, November 1-3, 2006) (pp. 132-148). (Lecture Notes in Computer Science; Vol. 4260). Springer. https://doi.org/10.1007/11901433_8