Industrial Strength CSP: Opportunities and Challenges in Model-Checking

Abstract

The Systems Assurance Group within QinetiQ Trusted Information Management is concerned with the development of high integrity systems. Historically these have been military safety or security critical applications, more recently our focus includes customers with dependability concerns from the civil and commercial sectors. CSP has become a core capability of the group, and is widely applied throughout our work. Central to our use of CSP is the ability to verify automatically refinements using the FDR model checker. This talk will present an overview of our application of model-checking to industrial systems assurance, the technical challenges we face, the methods we employ to overcome them, the future technology landscape that we will be facing and the associated opportunities and challanges for application of CSP.