Local livelock analysis of component-based models

Abstract

The use of increasingly complex applications is demanding a greater investment of resources in software development to ensure that applications are safe. For mastering this complexity, compositional approaches can be used in the development of software by integrating and reusing existing reliable components. The correct application of such strategies, however, relies on the trust in the behaviour of the components and in the emergent behaviour of the composed components because failures may arise if the composition does not preserve essential properties. Problems may be introduced when two or more error-free components are integrated for the first time. This concern is even more relevant when a group of components is put together in order to perform certain tasks, especially in safety-critical applications, during which classical problems can arise, such as livelock. In this thesis, we present a local strategy that guarantees, by construction, the absence of livelock in synchronous systems as modelled using the standard CSP notation. Our method is based solely on the local analysis of the minimum sequences that lead the CSP model back to its initial state. Locality provides an alternative to circumvent the state explosion generated by the interaction of components and allows us to identify livelock before composition. The verification of these conditions use metadata that allow us to record partial results of verification, decreasing the overall analysis effort. In addition, our work can also be applied to check livelock freedom in models that perform asynchronous communications. In this case, we carry out livelock analysis in the context of a component model, BR IC, whose behaviour of the components is described as a CSP process. Finally, we introduce three case studies to evaluate our livelock analysis technique in practice: the Milner’s scheduler and two variations of the dining philosophers, a livelock-free version and a version in which we have deliberately included livelock. For each case study, we also present a comparative analysis of the performance of our strategy with two other techniques for livelock freedom verification, the traditional global analysis of FDR and the static livelock analysis of SLAP. This comparative study demonstrates that our strategy can be used in practice and that it might be a useful alternative for establishing livelock freedom in large systems.