Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
6874211 | Information Processing Letters | 2018 | 5 Pages |
Abstract
The success of component-based techniques for software construction relies on trust in the emergent behaviour of the compositions. Here, we propose an efficient correct-by-construction technique for building livelock-free CSP models. Its verification conditions are based on a local analysis of the shortest event sequences (traces) that represent a recursive behaviour in the CSP model. This affords significant gains in performance in model checking. We evaluate our strategy based on models of the Milner's scheduler and the dining philosophers.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
Authors
M.S. Conserva Filho, M.V.M. Oliveira, A. Sampaio, Ana Cavalcanti,