Tesis doctoral de Elena Planas Hortal
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 ¿foundational subset for executable uml models¿ (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 ¿action language for fuml¿ (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.
Datos académicos de la tesis doctoral «Lightweight and static verification of uml executable models«
- Título de la tesis: Lightweight and static verification of uml executable models
- Autor: Elena Planas Hortal
- Universidad: Politécnica de catalunya
- Fecha de lectura de la tesis: 21/03/2013
Dirección y tribunal
- Director de la tesis
- Cristina Gómez Seoane
- Tribunal
- Presidente del tribunal: antoni Olivé ramon
- Manuel Wimmer (vocal)
- robert Clariso viladrosa (vocal)
- vicente Pelechano ferrragud (vocal)