TY - BOOK
T1 - Translating Chi models to UPPAAL timed automata
AU - Bortnik, E.M.
AU - Mortel - Fronczak, van de, J.M.
AU - Rooda, J.E.
PY - 2007
Y1 - 2007
N2 - 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.
AB - 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.
M3 - Report
T3 - SE report
BT - Translating Chi models to UPPAAL timed automata
PB - Technische Universiteit Eindhoven
CY - Eindhoven
ER -