On Open Source Tools for Behavioral Modeling and Analysis with fUML and Alf

Abstract. Executable and well-defined models are a cornerstone of model driven engineering. We are currently working on a transformation chain from UML models to formal verification tools. In the context of the UML language, the fUML and Alf specifications offer a standardized way for the semantics of the basic model elements and a textual specification lan-guage. Open source modeling tools started to adapt these specifications. However, their support is of varying degree. This paper summarizes our experiences with the open source tools regarding fUML and Alf support, and different model transformation technologies in order to analyse them with formal verification tools