Structured English for Model Checking Specification

Model checking has received wide acceptance as a valuable technique in the field of electronic design automation and is currently of growing interest in general systems design. Though its concepts and applications are well understood it often turns out that engineers have severe problems with the specification process and the underlying notation, i.e., formulation and understanding of specifications through means of temporal logic formulae. In this article, we present an approach for a natural language–oriented representation of temporal logic formulae by introducing patterns of structured English sentences for Clocked CTL (CCTL) specification. After outlining the basic patterns of the sentences we give their semantics by a translation to CCTL. A final example demonstrates their application.