ON THE FORMAL SPECIFICATION AND VERIFICATION OF AUTOMATA-BASED PROGRAMS BY SPECIFICATION PATTERNS
Read the full article
Model checking is a well developed verification technique; still it is not widely adopted. One of the reasons is that defining formal specification as a set of temporal logic formulae is an error-prone and time-consuming task. This paper gives an overview of the research which focuses on expressing verifiable requirements in a controlled natural language in the framework of automata-based programming. Applicability of the specification patterns in scope of automata-based approach is investigated. Also a formal grammar is introduced to derivate the requirements.