Analysis of TLcharts for weapon systems software development

Abstract

The success of formal specifications and reactive systems is highly dependant on the formal specification language being used. To date, the most common approach to this problem involves two activities: (i) the specification activity, where correctness properties are specified, and (ii) verification activity, where the system under review is proven to satisfy those properties. Typically, some form of temporal logic or regular expression language is used to specify the correctness properties; properties that are specified for given states of the system under review. This means that specification is partial and is done after system design, prototyping, or coding. Temporal logics have been found to be unsuitable for early specification. This thesis investigates the suitability of TLCharts, a specification language that combines statecharts and temporal logic, for the early specification of the dynamic characteristics of a homing torpedo. In order to achieve the task, a fictitious homing torpedo example, called KTorp, is used. Using a systematic approach, we developed deterministic statecharts and non-deterministic TLCharts for the KTorp control software. Our case study shows that using TLCharts as the early specification language for weapon systems software provides efficient, visual and intuitive specifications.