Extending a system with verified components

Abstract

The verification of component-based systems can be extremely complicated because it is usually not possible for system developers to pre-check the compatibility of the individual parts before the actual integration takes place. A system cannot be considered correct if its components do not work properly. Unfortunately, all the information on the correctness of the individual components become irrelevant and out-of-date from the moment they are used anywhere but the original environment. The solution to this problem can be based on the idea of building correct programs in which reliability is built-in. In this paper open incremental model checking - addressing the changes to a system rather than re-checking the entire system model including the new extensions - is discussed and compared to traditional modular model checking methods. In our paper we study the practical aspects and the efficiency of using Open Incremental Model Checking by working out a sample system consisting of verified components.