The object-orienteddspecification language UML/OCL has seen a certain acceptance as a formal, object-oriented modeling language in the industrial practice, in particular in the context of model-driven engineering oriented software development processes. Still, the semantic foundation of the language (currently under control of the OMG) is a largely open issue, at least if the interaction of several parts of the language (class models for static data-modeling vs. state-charts allowing behavioral system descriptions) is concerned. This phd is concerned with the extension on existing formal semantics for UML, its translation into standard logics and the generation of tests for this particular setting.
Context
In prior work, Brucker and Wolff 1,2,3,4 provided a formal, system-checked theory for semantics of the static data modeling part of the language, formalizing OCL version 2.0. This semantics leaded to several high-ranked publications and to several interventions/proposals within the OMG standardization process. The implementation of a prototypical MDE-framework
su4sml was based on Isabelle/HOL 2005.
Objectives
The major task of this Phd is to extend prior work to a more comprehensive subset of UML/OCL comprising also behavioral aspects of UML models. On the basis of the semantic theory, a translation build upon derived rules should be provided, that allows for a semantically correct translation of 3-valued OCL into the 2-valued world of conventional automated theorem provers of the Test-Case Generation System HOL-TestGen 5,6. In particular, for the latter, „classic“ test-case generation methods like invariant unfolding and HCNF-normal-form-computation as well as constraint-solving shall be implemented and adopted to an onject-oriented setting. The major technical problem here is to extend test-case generation techniques geared towards free data-types with tree-like structures to co-algebraic data-strauctures with graph-like structure.
Work program
The tasks can be subsumed as follows:
- Integrating HOL-OCL (Isabelle 2005) into HOL-TestGen (Isabelle2009-1, involves theorem proving and advanced tactic programming in Isabelle/HOL)
- Extending HOL-OCL by semantically foundation of StateCharts for Behavioral Specs
Tactics to convert OCL2.0 or OCL 2.2 to two-valued HOL-Representations in HOL
setup for HOL-TestGen involving
— classical setup: invariant-unfolding + normalization
— behavioral setup: semantically conservative means of automatas exploration
medium-sized case studies.
Extra information
1.Achim D. Brucker, Matthias P. Krieger, Burkhart Wolff: Extending OCL with Null-References. MoDELS Workshops 2009: 261-27
2.Achim D. Brucker, Burkhart Wolff: Semantics, calculi, and analysis for object-oriented specifications. Acta Inf. 46(4): 255-284 (2009)
3.A. D. Brucker, Burkhart Wolff: An Extensible Encoding of Object-oriented Data Models in hol. J. Autom. Reasoning 41(3-4): 219-249 (2008)
4.A. D. Brucker, Burkhart Wolff: HOL-OCL: A Formal Proof Environment for UML/OCL. FASE 2008: 97-10
Prerequisite
- knowledge in functional languages, logics
- interest in interactive theorem proving
(Isabelle/HOL will be teached „on the job“)
Détails
Expected funding
Institutional funding
Status of funding
Expected
Candidates
Utilisateur
Créé
Lundi 07 juin 2010 17:10:55 CEST
dernière modif.
Lundi 07 juin 2010 17:46:13 CEST
Fichiers joints
filename
créé
hits
filesize
Aucun fichier joint à cette fiche
Connexion
Ecole Doctorale Informatique Paris-Sud
Directrice
Nicole Bidoit Assistante
Stéphanie Druetta Conseiller aux thèses
Dominique Gouyou-Beauchamps
ED 427 - Université Paris-Sud
UFR Sciences Orsay
Bat 650 - aile nord - 417
Tel : 01 69 15 63 19
Fax : 01 69 15 63 87
courriel: ed-info à lri.fr