Formal Requirements Modeling with Executable Use Cases and Coloured Petri Nets Artigo Académico