This paper deals with the problem of the usage of formal techniques, based on model checking, where models are large and formal verification techniques face the combinatorial explosion issue. The goal of the approach is to express and verify requirements relative to certain context situations. The idea is to unroll the context into several scenarios and successively compose each scenario with the system and verify the resulting composition. We propose to specify the context in which the behavior occurs using a language called CDL (Context Description Language), based on activity and message sequence diagrams. The properties to be verified are specified with textual patterns and attached to specific regions in the context. The central idea is to automatically split each identified context into a set of smaller subcontexts and to compose them with the model to be validated. For that, we have implemented a recursive splitting algorithm in our toolset OBP (Observer-based Prover). This paper shows how this combinatorial explosion could be reduced by specifying the environment of the system to be validated. 1. Introduction Software verification is an integral part of the software development lifecycle, the goal of which is to ensure that software fully satisfies all the expected requirements. Reactive systems are becoming extremely complex with the huge increase in high technologies. Despite technical improvements, the increasing size of the systems makes the introduction of a wide range of potential errors easier. Among reactive systems, the asynchronous systems communicating by exchanging messages via buffer queues are often characterized by a vast number of possible behaviors. To cope with this difficulty, manufacturers of industrial systems make significant efforts in testing and simulation to successfully pass the certification process. Nevertheless, revealing errors and bugs in this huge number of behaviors remains a very difficult activity. An alternative method is to adopt formal methods, and to use exhaustive and automatic verification tools such as model-checkers. Model checking algorithms can be used to verify requirements of a model formally and automatically. Several model checkers as [1–5] have been developed to help the verification of concurrent asynchronous systems. It is well known that an important issue that limits the application of model checking techniques in industrial software projects is the combinatorial explosion problem [6–8]. Because of the internal complexity of developed software, model checking of requirements over the system
References
[1]
G. J. Holzmann, “The model checker SPIN,” IEEE Transactions on Software Engineering, vol. 23, no. 5, pp. 279–295, 1997.
[2]
K. G. Larsen, P. Pettersson, and W. Yi, “UPPAAL in a nutshell,” International Journal on Software Tools For Technology Transfer, vol. 1, no. 1-2, pp. 134–152, 1997.
[3]
B. Berthomieu, P. O. Ribet, and F. Vernadat, “The tool TINA—construction of abstract state spaces for petri nets and time petri nets,” International Journal of Production Research, vol. 42, no. 14, pp. 2741–2756, 2004.
[4]
J. C. Fernandez, H. Garavel, A. Kerbrat, L. Mounier, R. Mateescu, and M. Sighireanu, “Cadp: a protocol validation and verification toolbox,” in Proceedings of the 8th International Conference on Computer Aided Verification( CAV '96), pp. 437–440, London, UK, 1996.
[5]
A. Cimatti, E. Clarke, F. Giunchiglia, and M. Roveri, “Nusmv: a new symbolic model checker,” The International Journal on Software Tools for Technology Transfer, vol. 2, no. 4, pp. 410–425, 2000.
[6]
E. M. Clarke, E. A. Emerson, and A. P. Sistla, “Automatic verification of finite-state concurrent systems using temporal logic specifications,” ACM Transactions on Programming Languages and Systems, vol. 8, no. 2, pp. 244–263, 1986.
[7]
G. J. Holzmann and D. Peled, “An improvement in formal verification,” in Proceedings of the Formal Description Techniques (FORTE '94), pp. 197–211, Chapman & Hall, Berne, Switzerland, October 1994.
[8]
S. Park and G. Kwon, “Avoidance of state explosion using dependency analysis in model checking control flow model,” in Proceedings of the 5th International Conference on Computational Science and Its Applications (ICCSA '06), vol. 3984 of Lecture Notes in Computer Science, pp. 905–911, 2006.
[9]
P. Godefroid, “The Ulg partial-order package for SPIN,” in Proceedings of the International Conference on Model Checking Software (SPIN '95), Montréal, Quebec, Canada, October 1995.
[10]
D. Bo？na？ki and G. J. Holzmann, “Improving Spin's partial-order reduction for breadth-first search,” in Proceedings of the 12th International SPIN Workshop on Model Checking Software (SPIN '05), pp. 91–105, August 2005.
[11]
D. Peled, “Combining partial-order reductions with on-the-fly model-checking,” in Proceedings of the 6th International Conference on Computer Aided Verifiation (CAV '94), pp. 377–390, Springer, London, UK, 1994.
[12]
A. Valmari, “Stubborn sets for reduced state space generation,” in Proceedings of the 10th International Conference on Applications and Theory of Petri Nets, pp. 491–515, Springer, London, UK, 1991.
[13]
J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. J. Hwang, “Symbolic model checking: 1020 states and beyond,” in Proceedings of the 5th Annual IEEE Symposium on Logic in Computer Science, pp. 428–439, June 1990.
[14]
E. M. Clarke, D. E. Long, and K. L. Mcmillan, Compositional Model Checking, MIT Press, 1999.
[15]
C. Flanagan and S. Qadeer, “Thread-modular model checking,” in Proceedings of the 10th International Conference on Model Checking Software (SPIN '03), vol. 2648 of Lecture Notes in Computer Science, pp. 213–224, 2003.
[16]
O. Tkachuk and M. B. Dwyer, “Automated environment generation for software model checking,” in Proceedings of the 18th International Conference on Automated Software Engineering, pp. 116–129, 2003.
[17]
L. De Alfaro and T. A. Henzinger, “Interface automata,” in Proceedings of the 8th Eiropean Engineering Conference and 9th ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE '01), pp. 109–120, ACM Press, September 2001.
[18]
J. Barnat, L. Brim, and J. St？íbrná, “Distributed ltl model-checking in spin,” in Proceedings of the 8th International SPIN Workshop on Model Checking of Software (SPIN '01), pp. 200–216, Springer, New York, NY, USA, 2001.
[19]
S. Edelkamp and S. Schroedl, Heuristic Search—Theory and Applications, Academic Press, 2012.
[20]
K. Havelund, A. Skou, K. G. Larsen, and K. Lund, “Formal modeling and analysis of an audio/video protocol: an industrial case study using UPPAAL,” in Proceedings of the 18th IEEE Real-Time Systems Symposium, pp. 2–13, December 1997.
[21]
F. Boniol, V. Wiels, and E. Ledinot, “Experiences using model checking to verify real time properties of a landing gear control system,” in Proceedings of the 5th European Congress ERTS Embedded Real Time Software (ERTS '06), Toulouse, France, 2006.
[22]
T. Bochot, P. Virelizier, H. Waeselynck, and V. Wiels, “Model checking flight control systems: the Airbus experience,” in Proceedings of the 31st International Conference on Software Engineering (ICSE '09), pp. 18–27, May 2009.
[23]
X. Dumas, P. Dhaussy, F. Boniol, and E. Bonnafous, “Application of partial-order methods for the verification of closed-loop SDL systems,” in Proceedings of the 26th Annual ACM Symposium on Applied Computing (SAC '11), W. C. Chu, W. Eric Wong, M. J. Palakal, and C. C. Hung, Eds., pp. 1666–1673, March 2011.
[24]
L. E. Moser, Y. S. Ramakrishna, G. Kutty, P. M. Melliar-Smith, and L. K. Dillon, “A graphical environment for the design of concurrent real-time systems,” ACM Transactions on Software Engineering and Methodology, vol. 6, no. 1, pp. 31–79, 1997.
[25]
Y. S. Ramakrishna, L.K. Dillon, L. E. Moser, P. M. Melliar-Smith, and G. Kutty, “Real-time interval logic and its decision procedure,” in Proceedings of the 13th Foundations of Software Technology and Theoretical Computer Science Conference (FSTTCS '93), vol. 761 of Lecture Notes in Computer Science, pp. 173–192, 1993.
[26]
M. B. Dwyer, G. S. Avrunin, and J. C. Corbett, “Patterns in property specifications for finite-state verification,” in Proceedings of the 21st International Conference on Software Engineering, pp. 411–420, IEEE Computer Society Press, May 1999.
[27]
R. L. Smith, G. S. Avrunin, L. A. Clarke, and L. J. Osterweil, “PROPEL: an approach supporting property elucidation,” in Proceedings of the 24th International Conference on Software Engineering (ICSE '02), pp. 11–21, St Louis, Mo, USA, May 2002.
[28]
S. Konrad and B. H. C. Cheng, “Real-time specification patterns,” in Proceedings of the 27th International Conference on Software Engineering (ICSE '05), pp. 372–381, St Louis, Mo, USA, May 2005.
[29]
N. De Francesco, A. Santone, and G. Vaglini, “A user-friendly interface to specify temporal properties of concurrent systems,” Information Sciences, vol. 177, no. 1, pp. 299–311, 2007.
[30]
P. Farail, P. Gaufillet, F. Peres et al., “FIACRE: an intermediate language for model verification in the TOPCASED environment,” in Proceedings of the European Congress on Embedded Real-Time Software (ERTS '08), Toulouse, France, Janvier 2008.
[31]
J. C. Roger, Exploitation de contextes et d'observateurs pour la validation formelle de modèles [Ph.D. thesis], ENSIETA, Université de Rennes I., December 2006.
[32]
P. Dhaussy, P. Y. Pillain, S. Creff, A. Raji, Y. Le Traon, and B. Baudry, “Evaluating context descriptions and property definition patterns for software formal validation,” in Proceedings of the 12th IEEE/ACM Conference Model Driven Engineering Languages and Systems (Models '09), vol. 5795 of Lecture Notes in Computer Science, pp. 438–452, Springer, 2009.
[33]
J. Whittle, “Specifying precise use cases with use case charts,” in Proceedings of the International Conference on Satellite Events at the MoDELS (MoDELS '06), vol. 3844 of Lecture Notes in Computer Science, pp. 290–301, 2006.
[34]
P. Dhaussy and J. C. Roger, “Cdl (context description language): syntax and semantics,” Tech. Rep., ENSTA, Bretagne, France, 2011.
[35]
P. Dhaussy, F. Boniol, and J.-C. Roger, “Reducing state explosion with context modeling for model-checking,” in Proceedings of the 13th IEEE International High Assurance Systems Engineering Symposium (Hase '11), Boca Raton, Fla, USA, 2011.
[36]
W. Janssen, R. Mateescu, S. Mauw, P. Fennema, and P. Van Der Stappen, “Model checking for managers,” in Proceedings of the International SPIN Workshop on Model Checking of Software, pp. 92–107, 1992.
[37]
N. Halbwachs, F. Lagnier, and P. Raymond, “Synchronous observers and the verification of reactive systems,” in Proceedings of the 3rd International Conference on Algebraic Methodology and Software Technology (AMAST '93), M. Nivat, C. Rattray, T. Rus, and G. Scollo, Eds., Workshops in Computing, Springer, Twente, The Netherlands, June 1993.
