Visual formal specification using (N)TLCharts: statechart automata with temporal logic and natural language conditioned transitions

Summary form only given. This paper describes TLCharts, a visual specification language that combines the visual and intuitive appeal of nondeterministic Harel statecharts with formal specifications written in linear-time (metric) temporal logic (LTL and MTL). The formalism is described using a practical infusion pump requirement example. The infusion pump TLChart specification is then compared with two competing representations: temporal logic and deterministic Harel statecharts. The infusion pump example is also used to point out the strength of each constituent TLCharts component. We provide an informal semantics for TLCharts using nondeterministic automata with negation and overlapping states. Finally, we show how natural language snippets are used instead of TLChart temporal logic conditions thereby inducing a formalism we call NTLCharts.