Saturday, May 10, 2008
Experience of applying model checking on industrial software
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.
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
Comments:
<< Home
It's quite important for college students to know advices from https://justdomyhomework.com/blog/finish-homework-fast. It will help you to finishing your homework fast
Hi there. I like to visit different sites. I like to look for different information. I always use this site https://bestwritingservice.com/essays/Justice/classical-and-administrative-decision-making.html. He is very interesting. It helps me have good grades. I have extra help on any topic.
Important article. I'm glad I visited your site. I would recommend this site to all my friends. My friends and I found facts about plagiarism https://theplagiarism.com/articles/plagiarism-facts. This helps us to do our homework quickly.
When I was in college I try software engineering jobs in many companies finally I got a job in a company I'm working with nursing assignment help writers to learn how they are working.
The algorithmic analysis of programs to prove the properties of their executions is known as software model checking. get law assignment uk at UK assignment help
Rammafoundation establishment fix team of experienced laborers hand-burrow all establishment and sobbing waterproof foundation edmonton tile undertakings to guarantee greatest dependability of the fixes without the requirement for costly
I am working as a senior writer at cheap essay help, which is popular among people because of its perfect assignment. It is one of the best assignment writing services that you can find in today’s writing world.
It's intriguing to see how model checking, such as your use of the SPIN model checker, is utilized in industrial software. Such studies provide useful insights, particularly for complicated systems like WebArrow. Similarly, fields such as nursing benefit from detailed validation, which is frequently backed by services such as nursing dissertation writing service to ensure academic rigor.
Post a Comment
<< Home
