\input zb-basic
\input zb-ioport
\iteman{io-port 02214848}
\itemau{Bortnik, E.; Tr\v cka, N.; Wijs, A.J.; Luttik, B.; Van De Mortel-Fronczak, J.M.; Baeten, J.C.M.; Fokkink, W.J.; Rooda, J.E.}
\itemti{Analyzing a $\chi$ model of a turntable system using Spin, CADP and Uppaal.}
\itemso{J. Log. Algebr. Program. 65, No. 2, 51-104 (2005).}
\itemab
Summary: Nowadays, due to increasing system complexity and growing competition and costs, industry makes high demands on powerful techniques used to design and analyze manufacturing systems. One of the most popular techniques to do performance analysis is simulation. However, simulation-based analysis cannot guarantee the correctness of a system, so it is less suitable for functional analysis. Our research focuses on examining other methods to do performance analysis and functional analysis, and trying to combine the two. One of the approaches is to translate a simulation model that is used for performance analysis to a model written in an input language of an existing verification tool. We translate a $\chi$ simulation model of a turntable system into models written in the input languages of the tools CADP, Spin and Uppaal, and do a functional analysis with each of them. This allows us to evaluate the usefulness of these tools for the functional analysis of $\chi$ models. We compare the input formalisms, the expressiveness of the temporal logics, and the algorithmic techniques for model checking that are used in those tools.
\itemrv{~}
\itemcc{}
\itemut{}
\itemli{doi:10.1016/j.jlap.2005.05.001}
\end