Formal models & verification [Session 1]

This session of three papers addresses the various forms of consistency checking in model based engineering. Within model based engineering, systems are modelled from different views. A different formalism is often used for each perspective, and those models then need to be internally consistent in order for a correct and effectively realizable design. The first paper covers the incremental refinement of a system´s functionality using class diagrams, whereas the second paper then checks the consistency of a system´s behavioral view and its structural definition. The third paper then derives a complete interface specification from a partial one in order to support the modeler needs. A common theme between the three papers is also the use of Satisfiability Modulo Theories (SMT) checkers to assist in the practical verification of the methods.