Sander de Putter: Evaluation of compositional model checking

Event Details

Although model checking is one of the most successful approaches for the analysis and verification of the behaviour of concurrent systems, it is plagued with the so-called state space explosion problem; the state space of a concurrent system tends to increase exponentially as the number of parallel processes increases linearly. To combat state space explosion several compositional verification approaches have been proposed such as compositional aggregation and assume-guarantee reasoning. In their evaluation of assume guarantee reasoning Cobleigh, Avrunin, and Clarke[1] rais doubts about the effectiveness of assume-guarantee reasoning. Inspired by this work, my current work investigates the effectiveness of compositional aggregation. In contrast to [1], we also aim to characterize situations when compositional aggregation is or is not effective. In this talk I will briefly discuss [1] and present our methodology and preliminary results of our evaluation of compositional aggregation.

[1] Cobleigh, J.M., Avrunin, G.S., Clarke, L.A.: Breaking up is hard to do: An evaluation of automated assume-guarantee reasoning. ACM Trans. Softw. Eng. Methodol. 17(2), 7:1-7:52(May 2008)