A key problem in compositional model checking of software systems is that typical modelcheckers accept only closed systems (runnable programs) and therefore a component cannot be model-checked directly. A typical sol...
详细信息
A key problem in compositional model checking of software systems is that typical modelcheckers accept only closed systems (runnable programs) and therefore a component cannot be model-checked directly. A typical solution is to create an artificial environment for the component such that its composition forms a runnable program that can be model-checked. Although it is possible to create a universal environment that performs all possible sequences and interleavings of calls of the component's methods, for practical purposes it is sufficient to capture in this way just the use of the component in a particular software system-this idea is expressed by the paradigm of assume-guarantee reasoning. The authors present an approach to assume-guarantee-based veri. cation of software systems in the context of the SOFA 2 component framework. They provide an overview of the approach to the construction of an artificial environment for the veri. cation of SOFA 2 components implemented in java with the java pathfinder model checker. They also show the benefits of their approach on results of experiments with a non-trivial software system and discuss its advantages over other approaches with similar goals.
暂无评论