Publication at Faculty of Mathematics and Physics |
2010
Abstract
A key problem in compositional model checking of software systems is that typical model checkers 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.
For practical purposes it is sufficient to capture in the environment just the use of the component in a particular software system – this idea is expressed by the paradigm of assume-guarantee reasoning. In this paper, we present our approach to assume-guarantee-based verification of software systems in the context of the SOFA 2 component framework.
We show the benefits of our approach on results of experiments with a non-trivial software system.