Assessing situation models with a lightweight formal method

In order to leverage the benefits of the notion of situation at design time, proper support is required at the modeling level. In the past, this need has led to the development of a situation type specification language called SML. Although SML facilitates the definition of situation types by providing a graphical notation, designers could profit from additional support in order to assess the quality of the situation type models they produce. Since situations consist of combinations of context elements and may also be combined into complex situations, composition may lead to inconsistent, redundant and/or unintended situation type definitions. In order to address this challenge, in this paper we present a formal validation method for situation modeling based on the automatic transformation of SML models into a lightweight formal method.