Output details
11 - Computer Science and Informatics
University of Oxford
Assumption-commitment support for CSP model checking
<07>
This paper brings support for the Assumption-Commitment paradigm to the realm of CSP model checking. Techniques developed here have been implemented in a modelling tool (ModelWorks, which provides a front-end to CSP/FDR) in the commercial sector by QinetiQ (Corroboration for this and D-RisQ: see case study 7). The support of these techniques within ModelWorks was instrumental in the winning of follow-on research projects that both applied and extended ModelWorks, and have recently led to its commercial release and a spin-out company, D-RisQ.
This 34-page journal paper expands on the 16-page conference paper presented at AVoCS’06, adding full proofs and experimental validation. None of this work was submitted to RAE2008.