TimeLine Depiction: an approach to graphical notation for supporting temporal property specification

The finite-state verification techniques such as model checking allow for automated checking whether system model described with automata satisfy temporal properties, or not. The temporal properties should be typically specified in temporal logic formulae, which is a difficult task for programmers who aren’t verification experts. Therefore, there is a few of research to propose description languages with which non-experts can accurately express temporal requirements on system’s behaviors and the methods transforming them automatically into temporal property specification of particular model checker. We analyzed various researches aimed at the construction of property specifications, that is, machine translation from natural language to temporal logical formula, property specification pattern and graphical scenarios for specifying property, and so on. Based on the analysis, in this paper, we present a visual language called TimeLineDepic, which is a user-friendly graphical notation for temporal property description and whose expressive power is same as other languages. And we propose a method to transform TimeLineDepic to buchi automata (never claim) and insert it in promela-based model for model checker SPIN.