Behavioral and Temporal Rule Checking for Gaussian Random Process – a Kalman Filter Example

This paper describes a behavioral and temporal pattern detection technique for state-space systems whose state is a random variable such as the state estimated using a Kalman filter. Our novel behavioral and temporal pattern detection technique uses diagrammatic, intuitive, yet formal specifications based on a dialect of the UML of the kind used to monitor or formally verify the correctness of deterministic systems. Combining these formal specifications with a special code generator, extends the deterministic pattern detection technique to the domain of stochastic processes.We demonstrate the technique using a Ballistic trajectory Kalman filter tracking example in which a pattern-rule of interest is not flagged when observing the sequence of mean track position values but is flagged with a reasonable probability using the proposed technique.