%0 Journal Article %1 Engels2003 %A Engels, Gregor %A Küster, Jochen Malte %A Heckel, Reiko %A Lohmann, Marc %D 2003 %J Electr. Notes Theor. Comput. Sci. %K CSP UML model-checker %N 7 %T Model-Based Verification and Validation of Properties %V 82 %X One of the key issues in software development, like in all engineering problems, is to ensure that the product delivered meets its specification. Verification and validation are well-established techniques for ensuring the quality of a product within the overall software development lifecycle. With models being expressed in the Unified Modeling Language, the application of verification and validation is complicated. Firstly, concerning verification, a UML model is typically not the input language of a verification tool. Secondly, with regards to validation, a UML model is also not directly executable. In this paper, we show how verification and validation can be achieved for UML models. Within our approach, graph transformation techniques are applied for automated translation of UML models into a language understood by a verification tool or directly into an implementation. By the use of such semantic-preserving transformations, both verification and validation can be lifted up to the model level, allowing for a seamless integration of verification and validation into a UML-based development process.

@article{Engels2003, abstract = {One of the key issues in software development, like in all engineering problems, is to ensure that the product delivered meets its specification. Verification and validation are well-established techniques for ensuring the quality of a product within the overall software development lifecycle. With models being expressed in the Unified Modeling Language, the application of verification and validation is complicated. Firstly, concerning verification, a UML model is typically not the input language of a verification tool. Secondly, with regards to validation, a UML model is also not directly executable. In this paper, we show how verification and validation can be achieved for UML models. Within our approach, graph transformation techniques are applied for automated translation of UML models into a language understood by a verification tool or directly into an implementation. By the use of such semantic-preserving transformations, both verification and validation can be lifted up to the model level, allowing for a seamless integration of verification and validation into a UML-based development process.}, added-at = {2008-06-24T15:09:12.000+0200}, author = {Engels, Gregor and K{\"u}ster, Jochen Malte and Heckel, Reiko and Lohmann, Marc}, bibsource = {DBLP, http://dblp.uni-trier.de}, biburl = {https://www.bibsonomy.org/bibtex/290d17b0922b85ab36d58af98621de252/ist_spl}, description = {DBLP Record 'journals/entcs/EngelsKHL03'}, ee = {http://www1.elsevier.com/gej-ng/31/29/23/133/48/show/Products/notes/index.htt\#011}, interhash = {83e7c0ab20fdb7e0da548524143cd2d2}, intrahash = {90d17b0922b85ab36d58af98621de252}, journal = {Electr. Notes Theor. Comput. Sci.}, keywords = {CSP UML model-checker}, note = {MR: UML-Modell (On the high level, our system model is composed of use case diagrams and sequence diagrams describing the interaction of the system with users of the system. On the low level, it is composed of class diagrams, statecharts and activity diagrams.) wird durch Grapftransformationen in eine formale Sprache (CSP) überführt und mit einem Model-Checker validiert und in ein Testmodell überführt.}, number = 7, timestamp = {2008-06-24T15:09:12.000+0200}, title = {Model-Based Verification and Validation of Properties}, volume = 82, year = 2003 }