Implementing and verifying MSC specifications using PROMELA/XSPIN

We discuss a translation of Message Sequence Charts (MSCs) into the language PROMELA (we call this translation anìmplementation') that is consistent with the formal semantics we have previously deened for Message Flow Graphs and Message Sequence Charts, which handled the syntactic features with mathematical import from ITU-T recommendation Z.120. We report on experiments executing the PROMELA code using the XSPIN sim-ulator and validator. In previous work we found that potential process divergence and non-local choice situations impose problems on implementations of MSCs, and we discuss how these impact our PROMELA translation and suggest solutions. Finally, we show how to model-check liveness requirements imposed on MSC speciications. We use the PROMELA models obtained from our implementation, describe how to use control state propositions based on these models, use Linear Time Temporal Logic formulas to specify the liveness properties, and demonstrate the use of XSPIN as a model checker for these properties.