Online monitoring of a distributed building automation system to verify large sequences of bus messages by causal Petri net models.