%0 Journal Article
%T Improving Model Checking with Context Modelling
%A Philippe Dhaussy
%A Fr¨¦d¨¦ric Boniol
%A Jean-Charles Roger
%A Luka Leroux
%J Advances in Software Engineering
%D 2012
%I Hindawi Publishing Corporation
%R 10.1155/2012/547157
%X 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¨C5] 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¨C8]. Because of the internal complexity of developed software, model checking of requirements over the system
%U http://www.hindawi.com/journals/ase/2012/547157/