U-MarMo

A promising approach to achieving non-functional requirements relies on software models that capture the relevant aspects of the system being designed. Models can be analyzed to predict whether the future system satisfies the requirements prior to implementing system. By following a model-driven approach and by applying verification at the model level, software engineers can anticipate detection of possible flaws that would otherwise become part of the implementation. 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.

Go to the U-MarMo homepage