Software components and formal methods from a computational viewpoint

Software components and the methodology of component-based development offer a promising approach to master the design complexity of huge software products because they separate the concerns of software architecture from individual component behavior and allow for reusability of components. In combination with formal methods, the specification of a formal component model of the later software product or system allows for establishing and verifying important system properties in an automatic and convenient way, which positively contributes to the overall correctness of the system. Here, we study such a combined approach. As similar approaches, we also face the so-called state space explosion problem which makes property verification computationally hard. In order to cope with this problem, we derive techniques that are guaranteed to work in polynomial time in the size of the specification of the system under analysis, i.e., we put an emphasis on the computational viewpoint of verification. As a consequence, we consider interesting subclasses of component-based systems that are amenable to such analysis. We are particularly interested in ideas that exploit the compositionality of the component model and refrain from understanding a system as a monolithic block. The assumptions that accompany the set of systems that are verifiable with our techniques can be interpreted as general design rules that forbid to build systems at will in order to gain efficient verification techniques. The compositional nature of software components thereby offers development strategies that lead to systems that are correct by construction. Moreover, this nature also facilitates compositional reduction techniques that allow to reduce a given model to the core that is relevant for verification. We consider properties specified in Computation Tree Logic and put an emphasis on the property of deadlock-freedom. We use the framework of interaction systems as the formal component model, but our results carry over to other formal models for component-based development. We include several examples and evaluate some ideas with respect to experiments with a prototype implementation