Formulating Model Verification Tasks Prover-Independently as UML Diagrams
Sprache des Vortragstitels:
Englisch
Original Tagungtitel:
European Conference on Modelling Foundations and Applications
Sprache des Tagungstitel:
Englisch
Original Kurzfassung:
The success of Model-Driven Engineering (MDE) relies on
the quality of the employed models. Thus, quality assurance through
validation and verification has a tradition within MDE. But model verification
is typically done in the context of specialized approaches and
provers. Therefore, verification tasks are expressed from the viewpoint
of the chosen prover and approach requiring particular expertise and
background knowledge. This contribution suggests to take a new view
on verification tasks that is independent from the employed approach
and prover. We propose to formulate verifications tasks in terms of the
used modeling language itself, e.g. with UML and OCL. As prototypical
example tasks we show how (a) questions concerning model consistency
can be expressed with UML object diagrams and (b) issues regarding
state reachability can be defined with UML sequence diagrams.