runtime verification, trace expression, model checking