Automatic Simulation of Network Problems in UDP-Based Java Programs Temporal Logic and Natural Language Conditioned Transitions
Santa Fe, New Mexico
Apr. 26, 2004 to Apr. 30, 2004
Doron Drusinsky , Time-Rover, Inc.
This paper describes TLCharts, a visual specification language that combines the visual and intuitive appeal of non-deterministic 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 will also be 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.
Doron Drusinsky, "Automatic Simulation of Network Problems in UDP-Based Java Programs Temporal Logic and Natural Language Conditioned Transitions", IPDPS, 2004, Parallel and Distributed Processing Symposium, International, Parallel and Distributed Processing Symposium, International 2004, pp. 268a, doi:10.1109/IPDPS.2004.1303343