Assume-guarantee verification of software components in SOFA 2 framework

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 such that composition of them forms a runnable program that can be model-checked. While 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. 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 provide an overview of our approach to the construction of an artificial environment for verification of SOFA 2 components implemented in Jav...

• Type: Journal
• Year: 2010
• Where: IEE
• Authors: Pavel Parizek, Frantisek Plasil
• Keywords: Artificial Environment, IEE 2010, Runnable Program, Software System