Translating Chi models to UPPAAL timed automata

Due to increasing system complexity and growing competition and costs, powerful techniques are needed 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. Our research focuses on examining other methods to make performance analysis and functional analysis, and combining 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. The process algebraic language Chi is intended for modeling, simulation, verification and real-time control and has been used extensively to simulate large manufacturing systems. Uppaal is an integrated tool environment for modeling, validation and verification of real-time systems and has been applied successfully in case studies ranging from communication protocols to multimedia applications. In this report, we represent a translation scheme that is used to translate simulation models written in Chi language to Uppaal timed automata. As an example we apply the translation scheme to a model of a manufacturing system and show some of the properties that can be verified in Uppaal