Model-checking of real-time systems
Rajeev Alur, Lalita Jategaonkar Jagadeesan, Joseph J. Kott, James E. Von Olnhausen · 1997
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.