Verifying Chi models of industrial systems with Spin

N. Trcka

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

1 Citation (Scopus)


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.
Original languageEnglish
Title of host publicationFormal Methods and Software Engineering (Proceedings 8th International Conference on Formal Engineering Methods, ICFEM 2006, Macao, China, November 1-3, 2006)
EditorsZ. Liu, Z. He
Place of PublicationBerlin
ISBN (Print)3-540-47460-9
Publication statusPublished - 2006

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743


Dive into the research topics of 'Verifying Chi models of industrial systems with Spin'. Together they form a unique fingerprint.

Cite this