Model-Checking of Real-Time Systems: A Telecommunications Application (Experience Report)
Abstract
We describe the application of model checking tools to analyze a real-time software challenge in the design of Lucent Technologies' 5ESS telephone switching system.We use two tools: COSPAN for checking real-time properties, and TPWB for checking probabilistic specifications.We report on the feedback given by the tools, and based on our experience, discuss the advantages and the limitations of the approach used.
BibTeX
@inproceedings{Alur-al:ICSE97,
author = {Rajeev Alur and
Lalita Jategaonkar Jagadeesan and
Joseph J. Kott and
James Von Olnhausen},
title = {{Model-Checking} of {Real-Time} Systems: A Telecommunications Application {(Experience} Report)},
booktitle = {ICSE},
pages = {514--524},
publisher = {{ACM}},
year = {1997},
}