{"id":113990,"date":"2018-03-11T10:41:48","date_gmt":"2018-03-11T10:41:48","guid":{"rendered":"https:\/\/www.deberes.net\/tesis\/sin-categoria\/lightweight-and-static-verification-of-uml-executable-models\/"},"modified":"2018-03-11T10:41:48","modified_gmt":"2018-03-11T10:41:48","slug":"lightweight-and-static-verification-of-uml-executable-models","status":"publish","type":"post","link":"https:\/\/www.deberes.net\/tesis\/diseno-y-componentes-de-sistemas-de-informacion\/lightweight-and-static-verification-of-uml-executable-models\/","title":{"rendered":"Lightweight and static verification of uml executable models"},"content":{"rendered":"<h2>Tesis doctoral de <strong> Elena Planas Hortal <\/strong><\/h2>\n<p>Executable models play a key role in many development methods (such as mdd and mda) by facilitating the immediate simulation\/implementation of the software system under development. This is possible because executable models include a ?Ne-grained speci?Cation of the system behaviour using an action language. Executable models are not a new concept but are now experiencing a comeback. As a relevant example, the omg has recently published the ?Rst version of the \u00c2\u00bffoundational subset for executable uml models\u00c2\u00bf (fuml) standard, an executable subset of the uml that can be used to de?Ne, in an operational style, the structural and behavioural semantics of systems. The omg has also published a beta version of the \u00c2\u00bfaction language for fuml\u00c2\u00bf (alf) standard, a concrete syntax conforming to the fuml abstract syntax, that provides the constructs and textual notation to specify the ?Ne-grained behaviour of systems. The omg support to executable models is substantially raising the interest of software companies for this topic.  given the increasing importance of executable models and the impact of their correctness on the ?Nal quality of software systems derived from them, the existence of methods to verify the correctness of executable models is becoming crucial. Otherwise, the quality of the executable models (and in turn the quality of the ?Nal system generated from them) will be compromised.  despite the number of research works targetting the veri?Cation of software models, their computational cost and poor feedback makes them di?Cult to integrate in current software development processes. Therefore, there is the need for efficient and useful methods to check the correctness of executable models and tools integrated to the modelling tools used by designers.  in this thesis we propose a veri?Cation framework to help the designers to improve the quality of their executable models. Our framework is composed of a set of lightweight static methods, i.E. Methods that do not require to execute the model in order to check the desired property. These methods are able to check several properties over the behavioural part of an executable model (for instance, over the set of operations that compose a behavioural executable model) such as syntactic correctness (i.E. All the operations in the behavioural model conform to the syntax of the language in which it is described), non-redundancy (i.E. There is no another operation with exactly the same behaviour), executability (i.E. After the execution of an operation, the reached system state is -in case of strong executability- or may be -in case of weak executability- consistent with the structural model and its integrity constraints) and completeness (i.E. All possible changes on the system state can be performed through the execution of the operations de?Ned in the executable model). For incorrect models, the methods that compose our veri?Cation framework return a meaningful feedback that helps repairing the detected inconsistencies.<\/p>\n<p>&nbsp;<\/p>\n<h3>Datos acad\u00e9micos de la tesis doctoral \u00ab<strong>Lightweight and static verification of uml executable models<\/strong>\u00ab<\/h3>\n<ul>\n<li><strong>T\u00edtulo de la tesis:<\/strong>\u00a0 Lightweight and static verification of uml executable models <\/li>\n<li><strong>Autor:<\/strong>\u00a0 Elena Planas Hortal <\/li>\n<li><strong>Universidad:<\/strong>\u00a0 Polit\u00e9cnica de catalunya<\/li>\n<li><strong>Fecha de lectura de la tesis:<\/strong>\u00a0 21\/03\/2013<\/li>\n<\/ul>\n<p>&nbsp;<\/p>\n<h3>Direcci\u00f3n y tribunal<\/h3>\n<ul>\n<li><strong>Director de la tesis<\/strong>\n<ul>\n<li>Cristina G\u00f3mez   Seoane<\/li>\n<\/ul>\n<\/li>\n<li><strong>Tribunal<\/strong>\n<ul>\n<li>Presidente del tribunal: antoni Oliv\u00e9 ramon <\/li>\n<li>Manuel Wimmer (vocal)<\/li>\n<li>robert Clariso viladrosa (vocal)<\/li>\n<li>vicente Pelechano ferrragud (vocal)<\/li>\n<\/ul>\n<\/li>\n<\/ul>\n<p>&nbsp;<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Tesis doctoral de Elena Planas Hortal Executable models play a key role in many development methods (such as mdd and [&hellip;]<\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"site-sidebar-layout":"default","site-content-layout":"","ast-site-content-layout":"","site-content-style":"default","site-sidebar-style":"default","ast-global-header-display":"","ast-banner-title-visibility":"","ast-main-header-display":"","ast-hfb-above-header-display":"","ast-hfb-below-header-display":"","ast-hfb-mobile-header-display":"","site-post-title":"","ast-breadcrumbs-content":"","ast-featured-img":"","footer-sml-layout":"","theme-transparent-header-meta":"","adv-header-id-meta":"","stick-header-meta":"","header-above-stick-meta":"","header-main-stick-meta":"","header-below-stick-meta":"","astra-migrate-meta-layouts":"default","ast-page-background-enabled":"default","ast-page-background-meta":{"desktop":{"background-color":"var(--ast-global-color-4)","background-image":"","background-repeat":"repeat","background-position":"center center","background-size":"auto","background-attachment":"scroll","background-type":"","background-media":"","overlay-type":"","overlay-color":"","overlay-gradient":""},"tablet":{"background-color":"","background-image":"","background-repeat":"repeat","background-position":"center center","background-size":"auto","background-attachment":"scroll","background-type":"","background-media":"","overlay-type":"","overlay-color":"","overlay-gradient":""},"mobile":{"background-color":"","background-image":"","background-repeat":"repeat","background-position":"center center","background-size":"auto","background-attachment":"scroll","background-type":"","background-media":"","overlay-type":"","overlay-color":"","overlay-gradient":""}},"ast-content-background-meta":{"desktop":{"background-color":"var(--ast-global-color-5)","background-image":"","background-repeat":"repeat","background-position":"center center","background-size":"auto","background-attachment":"scroll","background-type":"","background-media":"","overlay-type":"","overlay-color":"","overlay-gradient":""},"tablet":{"background-color":"var(--ast-global-color-5)","background-image":"","background-repeat":"repeat","background-position":"center center","background-size":"auto","background-attachment":"scroll","background-type":"","background-media":"","overlay-type":"","overlay-color":"","overlay-gradient":""},"mobile":{"background-color":"var(--ast-global-color-5)","background-image":"","background-repeat":"repeat","background-position":"center center","background-size":"auto","background-attachment":"scroll","background-type":"","background-media":"","overlay-type":"","overlay-color":"","overlay-gradient":""}},"footnotes":""},"categories":[4149,13880,15596],"tags":[13034,226143,226142,226144,164536,47125],"class_list":["post-113990","post","type-post","status-publish","format-standard","hentry","category-diseno-y-componentes-de-sistemas-de-informacion","category-informatica","category-politecnica-de-catalunya","tag-antoni-olive-ramon","tag-cristina-gomez-seoane","tag-elena-planas-hortal","tag-manuel-wimmer","tag-robert-clariso-viladrosa","tag-vicente-pelechano-ferrragud"],"_links":{"self":[{"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/posts\/113990","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/comments?post=113990"}],"version-history":[{"count":0,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/posts\/113990\/revisions"}],"wp:attachment":[{"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/media?parent=113990"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/categories?post=113990"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/tags?post=113990"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}