VERIFICATION OF TIMED CHI MODELS USING UPPAAL

E. M. Bortnik, D. A. van Beek, J. M. van de Mortel-Fronczak, J. E. Rooda

2005

Abstract

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 χ 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 paper, we represent a translation scheme that is used to translate simulation models written in χ language to UPPAAL timed automata and show a small example of the translation. Future work includes defining an equivalence relation between χ and UPPAAL transition systems, implementing the translator as a part of the χ toolset, and applying it for verification of models of manufacturing systems.

Paper Citation

in Harvard Style

M. Bortnik E., A. van Beek D., M. van de Mortel-Fronczak J. and E. Rooda J. (2005). VERIFICATION OF TIMED CHI MODELS USING UPPAAL . In Proceedings of the Second International Conference on Informatics in Control, Automation and Robotics - Volume 4: ICINCO, ISBN 972-8865-30-9, pages 486-492. DOI: 10.5220/0001191204860492

in Bibtex Style

@conference{icinco05,
author={E. M. Bortnik and D. A. van Beek and J. M. van de Mortel-Fronczak and J. E. Rooda},
title={VERIFICATION OF TIMED CHI MODELS USING UPPAAL},
booktitle={Proceedings of the Second International Conference on Informatics in Control, Automation and Robotics - Volume 4: ICINCO,},
year={2005},
pages={486-492},
publisher={SciTePress},
organization={INSTICC},
doi={10.5220/0001191204860492},
isbn={972-8865-30-9},
}

in EndNote Style

TY - CONF
JO - Proceedings of the Second International Conference on Informatics in Control, Automation and Robotics - Volume 4: ICINCO,
TI - VERIFICATION OF TIMED CHI MODELS USING UPPAAL
SN - 972-8865-30-9
AU - M. Bortnik E.
AU - A. van Beek D.
AU - M. van de Mortel-Fronczak J.
AU - E. Rooda J.
PY - 2005
SP - 486
EP - 492
DO - 10.5220/0001191204860492