Lukman Ab. Rahim
ABSTRACT
Model checking has always been associated with a scalability problem when verifying systems with large state spaces. This problem can be addressed using techniques that reduce the state space during verification. This paper proposes guidelines to identify suitable reduction techniques from design patterns. The selection of suitable state space reduction techniques is demonstrated using a complex concurrent system as case study. Using this case study, we discuss the reasons and conditions for selecting a reduction technique when a design pattern is used. The proposed guidelines are evaluated by checking if the selected reduction techniques reduces the number of states; implying that these techniques are suitable. The result of this evaluation shows that suitable reduction techniques can be identified from design patterns.
- L. Bass, P. Clements, and R. Kazman. Software Architecture in Practice, 2nd Edition. Addison Wesley, 2003. Google Scholar
Digital Library
- A. Betin-Can and T. Bultan. Highly Dependable Concurrent Programming using Design for Verification. Formal Aspects of Computing, 19(2):243--268, June 2007. Google ScholarCross Ref
- A. Betin-Can, T. Bultan, and X. Fu. Design for Verification for Asynchronously Communicating Web Services. In Proceedings of The 14th International World Wide Web Conference, pages 750--759. ACM, 2005. Google ScholarDigital Library
- E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking. The MIT Press, 1999. Google ScholarDigital Library
- M. B. Dwyer, G. S. Avrunin, and J. C. Corbett. Property Specification Patterns for Finite-State Verification. In Proceedings on the 2nd Workshop on Formal Methods in Software Practice, pages 7--15. ACM, 1998. Google ScholarDigital Library
- C. A. Furia. A Compositional World: A Survey of Recent Works on Compositionality in Formal Methods, 2005.Google Scholar
- E. Gamma, R. Helm, R. Johnson, and J. M. Vlissides. Design Patterns: Elements of Reusable Object-Oriented Software. Addison-Wesley, 2000. Google ScholarDigital Library
- Global Security.org. Joint Tactical Radio System. http://www.globalsecurity.org/military/systems/ground/jtrs.htm.Google Scholar
- P. Mehlitz and J. Penix. Design for Verification with Dynamic Assertions. In 29th Annual IEEE/NASA Software Engineering Workshop, pages 285--292. IEEE, July 2005. Google ScholarDigital Library
- A. Miller, A. F. Donaldson, and M. Calder. Symmetry in Temporal Logic Model Checking. (ACM Computing Survey), 38(3), 2006. Google ScholarDigital Library
- N. Sharygina, J. C. Browne, and R. P. Kurshan. A Formal Object-Oriented Analysis for Software Reliability: Design for Verification. In Proceedings of 4th International Conference on Fundamental Approaches to Software Engineering, volume 2029 of LNCS, pages 318--332. Springer, 2001. Google ScholarDigital Library
- W. Visser, C. S. Păsăreanu, and S. Khurshid. Test input generation with Java PathFinder. In ISSTA '04: Proceedings of the 2004 ACM SIGSOFT International Symposium on Software Testing and Analysis, pages 97--107, New York, NY, USA, 2004. ACM. Google ScholarDigital Library
Index Terms
- Identifying state space reduction techniques from behavioural design patterns
Recommendations
Optimistic synchronization-based state-space reduction
Reductions that aggregate fine-grained transitions into coarser transitions can significantly reduce the cost of automated verification, by reducing the size of the state space. We propose a reduction that can exploit common synchronization disciplines, ...
Reduction of state space in reinforcement learning by sensor selection
Much research has been conducted on the application of reinforcement learning to robots. Learning time is a matter of concern in reinforcement learning. In reinforcement learning, information from sensors is projected on to a state space. A robot learns ...
Optimistic synchronization-based state-space reduction
TACAS'03: Proceedings of the 9th international conference on Tools and algorithms for the construction and analysis of systemsReductions that aggregate fine-grained transitions into coarser transitions can significantly reduce the cost of automated verification, by reducing the size of the state space. We propose a reduction that can exploit common synchronization disciplines, ...
Comments