SME Internal Representation for CSPm

FDR version 4 has demonstrated the ability to perform exhaustive verification of complex software in a timeframe that makes formal testing usable for real world scenarios. Since SME is built on the fundamental ideas behind CSP we believe it should be possible to translate SME programs into CSPm and then use FDR for verifying the solution. The project will require the student to get familiar with CSPm and FDR, and to specify additional information that must be provided by SME or the programmer, to produce a CSPM representation.

Area: Masters

Tags: SME:CSP:FDR

Contact: Brian Vinter, vinter@nbi.ku.dk

Activities: Analysis, design and implementation