Loading...
 
[Show/Hide Left Column]

Sujets Help

Print View Items
No Tabs
ViewCommentsAttachments (0)

View Item

Domain Programming-Testing-Proving
Domain - extra Testing Object-oriented System Models
Year 2010
Starting 1.10.2010
Status Open
Subject Black-box Testing UML/OCL Specifications
Thesis advisor WOLFF Burkhart
Co-advisors Frederic Voisin (LRI), OCL
Makarius Wenzel (Postdoc LRI; Isabelle development)
Laboratory LRI VALS
Collaborations
Abstract 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“)
Details
Expected funding Institutional funding
Status of funding Expected
Candidates
user
Created Monday 07 of June, 2010 17:10:55 CEST
LastModif Monday 07 of June, 2010 17:46:13 CEST


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 at lri.fr