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.
Original language | English |
---|---|
Title of host publication | Proc. of the 3rd Int. Workshop on Behavioural Modelling - Foundations and Applications, BM-FA2011 - In Collaboration with the 7th European Conf. on Modelling Foundations and Applications, ECMFA 2011 |
Pages | 49-55 |
Number of pages | 7 |
DOIs | |
Publication status | Published - 2011 |
Externally published | Yes |
Event | 3rd International Workshop on Behavioural Modelling - Foundations and Applications, BM-FA2011 - In Collaboration with the 7th European Conference on Modelling Foundations and Applications, ECMFA 2011 - Birmingham, United Kingdom Duration: 6 Jun 2011 → 6 Jun 2011 |
Conference
Conference | 3rd International Workshop on Behavioural Modelling - Foundations and Applications, BM-FA2011 - In Collaboration with the 7th European Conference on Modelling Foundations and Applications, ECMFA 2011 |
---|---|
Country/Territory | United Kingdom |
City | Birmingham |
Period | 6/06/11 → 6/06/11 |
Keywords
- Design pattern
- State space reduction