Local livelock analysis of component-based models
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...
Na minha lista:
| Autor principal: | |
|---|---|
| Outros Autores: | |
| Formato: | doctoralThesis |
| Idioma: | por |
| Publicado em: |
Brasil
|
| Assuntos: | |
| Endereço do item: | https://repositorio.ufrn.br/jspui/handle/123456789/22209 |
| Tags: |
Adicionar Tag
Sem tags, seja o primeiro a adicionar uma tag!
|
| Resumo: | 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. |
|---|