U-MarMo

U-MarMo (UML to Markov Models) consists of a model-to-model transformation step followed by model checking to formally verify
non-functional requirements on UML diagrams. Currently U-MarMo supports SDs decorated with quantitative annotations and generates Markov models. DTMCs and CTMCs are used to verify reliability and performance properties. A variant of DTMCs is used to verify cost properties, such as energy consumption.