Behaviour Analysis and Safety Conditions: a Case Study in CML

Abstract

We describe a case study where novel program analysis technology has been used to pinpoint a subtle bug in a formally developed control program for an embedded system. The main technology amounts to first defining a process algebra (called behaviours) suited to the programming language used (in our case CML) and secondly to devise an annotated type and effect system for extracting behaviours from programs in a such a manner that an automatic inference algorithm can be developed. The case study is a control program developed for the "Karlsruhe Production Cell" and our analysis of the behaviours shows that one of the safety conditions fails to hold.