Motives Reiko

Foundations of Model Transformation: 

ARTIST2 - MOTIVES Trento - Italy, February 19-23, 2007 Model Transformation and UML Reiko Heckel University of Leicester, UK Foundations of Model Transformation

Motivation: Model-driven Engineering: 

Motivation: Model-driven Engineering Focus and primary artifacts are models instead of programs Core activities include maintaining consistency evolution translation execution of models These are examples of model transformations A math. foundation is needed for studying expressiveness and complexity execution and optimisation well-definedness preservation of semantics of transformations Graph transformations can be one such foundation

Outline: 

Outline Graph Transformation why it is fun how it works Semantics-preserving Model Transformation

Why it is fun: Programming By Example: 

Why it is fun: Programming By Example StageCast (www.stagecast.com): a visual programming environment for kids (from 8 years on), based on behavioral rules associated to graphical objects visual pattern matching simple control structures (priorities, sequence, choice, ...) external keyboard control intuitive rule-based behavior modelling Next: abstract from concrete visual presentation

States of the PacMan Game:Graph-Based Presentation : 

States of the PacMan Game: Graph-Based Presentation :Ghost :Field :Field :Field :Field :Field :Field :PacMan marbles=3 :Marble

Rules of the PacMan Game:Graph-Based Presentation, PacMan : 

Rules of the PacMan Game: Graph-Based Presentation, PacMan f1:Field f2:Field pm:PacMan f1:Field f2:Field pm:PacMan movePM pm:PacMan marbles=m f1:Field f2:Field :Marble f1:Field f2:Field pm:PacMan marbles=m+1 collect

Rules of the PacMan Game:Graph-Based Presentation, Ghost: 

Rules of the PacMan Game: Graph-Based Presentation, Ghost f1:Field f2:Field g:Ghost f1:Field f2:Field g:Ghost moveGhost g:Ghost f1:Field f2:Field :PacMan f1:Field f2:Field g:Ghost kill

Graph Transformation: 

Graph Transformation :Ghost :Field :Field :Field :Field :Field :Field :PacMan marbles=3 :PacMan marbles=4 typing collect ; kill Field PacMan marbles:int Ghost Marble 1 1 1 * * *

Outline: 

Outline Graph Transformation why it is fun how it works Semantics-preserving Model Transformation

A Basic Formalism: Typed Graphs: 

A Basic Formalism: Typed Graphs Directed graphs multiple parallel edges undirected edges as pairs of directed ones Graph homomorphism as mappings preserving source and target Typed graphs given by fixed type graph TG instance graphs G typed over TG by homomorphism g g:Ghost :Field :Field :Field :Field :Field f:Field g Field PacMan marbles:int Ghost Marble G TG

Rules : 

Rules p: L  R with L  R well-defined, in different presentations like above (cf. PacMan example) with L  R explicit [DPO]: L  K  R f1:Field f2:Field pm:PacMan movePM: f1:Field f2:Field pm:PacMan

Rules : 

Rules p: L  R with L  R well-defined, in different presentations like above (cf. PacMan example) with L  R explicit [DPO]: L K  R with L, R integrated [UML, Fujaba]: L  R and marking L - R as destroyed R - L as new f1:Field f2:Field pm:PacMan movePM: {destroyed} {new}

Transformation Step: 

Transformation Step select rule p: L  R ; occurrence oL: L  G remove from G the occurrence of L\ R add to result a copy of R \ L f1:Field f2:Field pm:PacMan marbles=3 m2:Marble G f3:Field m1:Marble

Semantic Questions: Dangling Edges: 

Semantic Questions: Dangling Edges conservative solution: application is forbidden invertible transformations, no side-effects radical solution: delete dangling edges more complex behavior, requires explicit control ?

A bit of History …: 

A bit of History … Chomsky Grammars Term Rewriting Petri Nets Graph Transformation and Graph Grammars Diagram Languages Behaviour Modelling and Visual Programming Models of Computation

Outline: 

Outline Graph Transformation why it is fun how it works Semantics-preserving Model Transformation operational denotational transformation

Example: Executable Business Process: 

Example: Executable Business Process refactoring of business processes, replacing centralised by distributed execution How to demonstrate preservation of behaviour? specify operational semantics of processes define transformations show that transformations preserve semantics Receive order Undo order Shipment Warehouse Office

Operational Semantics: Idea: 

Operational Semantics: Idea diagram syntax plus runtime state GT rules to model state transitions Abstract Syntax operational semantics

Operational Semantics: Formally: 

Operational Semantics: Formally GTS = (TG, P) with start graph G0 defines transition system LTS(GTS, G0) = (S, L, ) taking as states S all graphs reachable from G0 observations on rules as labels transformations as transitions

Type Graph: Metamodel: 

Edge Node Basic op: String Structured Orch name: String Msg op: String id: String Switch Invoke src tar current to from partner request Reply response Elem corresponds responsible Type Graph: Metamodel … … with runtime state Abstract Syntax

Rules: Invoke another Service: 

Rules: Invoke another Service e:Edge tar i:Invoke o1:Orch o2:Orch current partner e:Edge tar i:Invoke o1:Orch o2:Orch current partner m:Msg id=new() op=i.op from to req(i.id, m.id) request Abstract Syntax operational semantics

Rules: Answer the Invocation: 

Rules: Answer the Invocation e:Edge tar r:Reply o1:Orch o2:Orch current m1:Msg op=r.op from to e:Edge tar r:Reply o1:Orch o2:Orch current m1:Msg op=r.op from to m2:Msg id=new() op=r.op from to reply(r.id, m1.id, m2.id) response src e:Edge src e:Edge Abstract Syntax operational semantics

Rules: Receive the Response: 

Rules: Receive the Response i:Invoke o1:Orch o2:Orch current src m1:Msg to from m2:Msg to from e:Edge partner i:Invoke o1:Orch o2:Orch current src e:Edge partner resp(i.id, m2.id) request response Abstract Syntax operational semantics

Simulation: 

Simulation :Edge tar i:Invoke o1:Orch o2:Orch current partner :Edge src :Edge tar r:Reply :Edge src current Observations: req(i.id, m1.id); reply(r.id, m1.id, m2.id); resp(i.id, m2.id)

Refactoring Executable Processes: 

Refactoring Executable Processes replace local control flow by message passing … Orch 1 Orch 2 … … Orch1 Orch 2 <<invoke>> Orch2.op <<receive>> op <<reply>> op … … … … … delegate

Semantic Compatibility: 

Semantic Compatibility Processes P1 and P2 are semantically compatible if they are weakly bisimilar after hiding labels not in alph(P1) ⋂ alph(P2) Show for trafo P1  P2 that P2 simulates P1, i.e. P1obs Q1 implies P2 obs Q2 Q2 simulates Q1 and vice versa. Approach: mixed (local) confluence critical pair analysis P1 Q1 P2 Q2 obs obs

Critical Pairs and Local Confluence: 

Critical Pairs and Local Confluence a pair of rules (p1, p2) in a minimal conflict situation constructed by overlapping their left-hand sides so that they intersect in items to be deleted system is locally confluent if all critical pairs are G H * G2 G1 * p1 p2

Critical Pair Analysis in AGGdelegate vs operational rules: 

Critical Pair Analysis in AGG delegate vs operational rules

Critical Pair: 

Critical Pair LHS of invoke vs delegate delete-use-conflict

Outline: 

Outline Graph Transformation why it is fun how it works Semantics-preserving Model Transformation operational denotational transformation

Process Improvement: 

Process Improvement Motivation: transform process to increase flexibility, performance, ... preserve behaviour! Aim: rule-level verification

Rule-level Verification: 

Rule-level Verification r r/o s(L) s(R) G H s(G) s(H) Approach: check for each rule r if s(L) R s(R) make sure that s(L) R s(R) implies s(G) R s(H) semantic domain

Works if …: 

Works if … we select semantic domain SD where relation R is compositional trace or failures equivalence or refinement in CSP is closed under context we can show that semantic mapping s: AS  SD is compositional maps union of graphs to composition of CSP processes  use GT to define mapping s

Context-Free Graph Grammar: 

Context-Free Graph Grammar Productions in EBNF-like notation: Concrete syntax of well-structured activity diagrams Abstract Syntax

Analysis: 

Analysis check availability receive order notify client calculate prize send receipt [product not available] [product available] 0 1 2 3 4 5 6 7 8

Pair Grammar: 

Pair Grammar do something out in ::= A:Act [c] [not c] if [c] then Proc(A1) else Proc(A2) do something Source: well-structured activity diagrams Abstract Syntax Semantic Domain denotational semantics

Synthesis: 

Synthesis Proc(A0) Proc(A1) ; Proc(A2) … Proc(A3) ; Proc (A4) ; if [product available] then Proc(A5) else Proc(A8) … receive order ; check availability ; if [product available] then calculate prize ; send receipt else notify client check availability receive order notify client calculate prize send receipt [product not available] [product available]

Good Enough … ?: 

Good Enough … ? Visual abstract syntax or concrete syntax templates Bi-directional swap source and target grammars Declarative Expressive ? context-free graph languages only Traceable ? through naming conventions Efficient ? NP complete parsing problem …  Triple Graph Grammars (see Andy’s lecture) Challenge: verify compositionality for more complex mappings

Relevant Theory: 

Relevant Theory Chomsky Grammars Term Rewriting Petri Nets Graph Transformation and Graph Grammars Formal language theory of graphs; Diagram compiler generators Concurrency theory Causality and conflict Processes, unfoldings Event-structures Stochastic concepts Verification, … Well-definedness Termination Confluence Semantics of process calculi