The very exciting ICSE 2008 (International Conference on Software Engineering) is going to begin in the beautiful Leipzig, Germany. Luckily my paper was accepted at the conference and scheduled in the Telecom Experience Track.

The paper is an abstract of my thesis work done at Queen's University which relates to apply model checking techniques on real industry scale software.

Model checking has been claimed to provide comprehensive coverage to the system it verifies. However, there were few critical studies of the application of model checking to industrial scale software systems by people other than the model checker's own authors. In the paper, I reported my experience in applying the SPIN model checker to the validation of the failover protocols of a commerical telecommunication system, WebArrow.

In my experiment, I used SPIN model checker as the tool as it is the most heavily optimized model checker in the field. The methodology I used as follows:
1. Summarize the failover protocol with UML activity digrams
2. Build Promela (the input language of SPIN model checker) models
3. Check for deadlock
4. Express properties in LTL (Linear Temporal Logic)
5. Verify LTL properties in the SPIN
6. Optimize and simplify the model
7. Debug model using counter-examples
8. Record results

The key study results are that I found there to be a significant gap between the promise of model checking and the reality. Rather than enjoying fully automated checking of properties versus declarative system models, I battled problems of tracebility in the model checker. In addition, the time to create and check the models was incompatible with realities of time-to-market demands. Furthermore, the creation of the model itself took a big chunk of effort as well.

From the results, I can see that there are still some areas in the model checking community that the model checker authors can improve.

Labels: QA