Bergeron, M. (2004). Model-checking UML designs using a temporal extension of the object constraint language. (Masters thesis, École Polytechnique de Montréal).