PATTERNS FOR TEMPORAL REQUIREMENTS ENGINEERING - A Level Crossing Case Study

A. Mekki, M. Ghazel, A. Toguyeni

2010

Abstract

This work presents a method for verifying temporal requirements of time-constrained systems. The method predates by establishing a new time constraints (properties) taxonomy. Then, a basis of observation patterns relative to the predefined requirements is developed. Our approach allows the automated verification of temporal requirements, initially expressed in a semi-formal formalism, through model transformation and model-checking. The contributions of the paper are string: the definition of a new time constraints (properties) typology as well as a basis of appropriate State Machines (SM) observation patterns. The second contribution consists in developing an algorithm for transforming UML SM with time annotations into Timed Automata (TA). In practice, in order to verify the temporal aspects of a given specification, the observation patterns relative to the investigated properties are instantiated to make appropriate observers. Then using our transformation algorithm, the system specification (denoted in the shape of an UML SM model) with time annotations as well as the obtained observers are translated into TA models. The TA system model is next synchronized with the TA observers. Thereby, the verification process is reduced to a reachability analysis.

Paper Citation

in Harvard Style

Mekki A., Ghazel M. and Toguyeni A. (2010). PATTERNS FOR TEMPORAL REQUIREMENTS ENGINEERING - A Level Crossing Case Study . In Proceedings of the 7th International Conference on Informatics in Control, Automation and Robotics - Volume 1: ICINCO, ISBN 978-989-8425-00-3, pages 45-52. DOI: 10.5220/0002947500450052

in Bibtex Style

@conference{icinco10,
author={A. Mekki and M. Ghazel and A. Toguyeni},
title={PATTERNS FOR TEMPORAL REQUIREMENTS ENGINEERING - A Level Crossing Case Study},
booktitle={Proceedings of the 7th International Conference on Informatics in Control, Automation and Robotics - Volume 1: ICINCO,},
year={2010},
pages={45-52},
publisher={SciTePress},
organization={INSTICC},
doi={10.5220/0002947500450052},
isbn={978-989-8425-00-3},
}

in EndNote Style

TY - CONF
JO - Proceedings of the 7th International Conference on Informatics in Control, Automation and Robotics - Volume 1: ICINCO,
TI - PATTERNS FOR TEMPORAL REQUIREMENTS ENGINEERING - A Level Crossing Case Study
SN - 978-989-8425-00-3
AU - Mekki A.
AU - Ghazel M.
AU - Toguyeni A.
PY - 2010
SP - 45
EP - 52
DO - 10.5220/0002947500450052