On the Verification of SCOOP Programs
This work addresses verification challenges in concurrent programming, specifically for SCOOP models used in robotics, but it is incremental as it builds on existing formalizations and tools.
The paper tackles the verification of SCOOP concurrency programs by integrating an alias analyzer and a deadlock detector within a Rewriting Logic framework, enabling the use of Maude's model-checker for analysis, with solutions provided for state explosion and an extended alias calculus for unbounded executions.
In this paper we focus on the development of a toolbox for the verification of programs in the context of SCOOP -- an elegant concurrency model, recently formalized based on Rewriting Logic (RL) and Maude. SCOOP is implemented in Eiffel and its applicability is demonstrated also from a practical perspective, in the area of robotics programming. Our contribution consists in devising and integrating an alias analyzer and a Coffman deadlock detector under the roof of the same RL-based semantic framework of SCOOP. This enables using the Maude rewriting engine and its LTL model-checker "for free", in order to perform the analyses of interest. We discuss the limitations of our approach for model-checking deadlocks and provide solutions to the state explosion problem. The latter is mainly caused by the size of the SCOOP formalization which incorporates all the aspects of a real concurrency model. On the aliasing side, we propose an extension of a previously introduced alias calculus based on program expressions, to the setting of unbounded program executions such as infinite loops and recursive calls. Moreover, we devise a corresponding executable specification easily implementable on top of the SCOOP formalization. An important property of our extension is that, in non-concurrent settings, the corresponding alias expressions can be over-approximated in terms of a notion of regular expressions. This further enables us to derive an algorithm that always stops and provides a sound over-approximation of the "may aliasing" information, where soundness stands for the lack of false negatives.