Open Source Software for Model Driven Engineering 2014
On Open Source Tools for
Behavioral Modeling and Analysis
with fUML and Alf
Zoltán Micskei, Raimund-Andreas Konnerth,
Benedek Horváth, Oszkár Semeráth,
András Vörös, and Dániel Varró
This work was partially supported by
Budapest University of Technology and Economics
Department of Measurement and Information Systems
Model Based Analysis of Distributed Systems
System design
Mathematical analysis
Model
generation
High-level
System Model
Fix problem
Receive request
Mathematical
model
Calculate Rating
Yes
Accept?
No
Send offer
Send rejection
Receive answer
Receive
update request
No
Send reply
Update?
List of
inconsistencies
Yes
Analysis
(e.g. model checker)
Overview of the Approach
OMG standard
UML
fUML
Alf
Formal Methods
State Machine
Activity Diagram
Alf Model
Timed Automata
1. What open source tools are available for fUML and Alf?
2. What level of support do they provide?
3. What are their maturity level?
4. What techniques are available for model generation?
3
Open Source Tooling Overview
UML
fUML
Alf
Formal Methods
State Machine
Activity Diagram
Alf Model
Timed Automata
Alf Editor
Model Checker
UML Editor
fUML Reference Impl.
AlfRef. Impl.
Papyrus
Alf Editor
Moka
Moliz
4
UPPAAL
Running Example: Fibonacci Calculation
ALF
UML State Machine
let tmp: Integer = 0;
if (input == 1) {
return 1;
} else if (input ==2) {
return 1;
}
let i: Integer = 3;
while (i <= input) {
tmp = var1 + var2;
var1 = var2;
var2 = tmp;
i++;
}
return tmp;
5
UPPAAL
Lesson Learned
No list of tools: Even collecting the tools was considerable effort
o Promote tools on OMG website
Few examples: Few example fUML models or Alf code available.
o Version and tool incompatibility hinders
Reference implementations:
o Help understand the specifications,
o Good starting point
Alf grammar: Complex structures to ensure unambiguity
o Good for evaluation of expressions
o Not good for semantic information to help verification
Transformation: Mapping of state machines?
6
Technologies for M2M
Java over EMF API
Concrete Syntax
while (i <= input){
i++;
}
Abstract Syntax
:Guard
block
:WhileStatement
exp="!(i<=input)"
condition
:Block
:ConditionTest
:Increment
:Relation
:VariableRef
name = "i"
op="<="
:VarRef
name = "i"
:VarRef
name = "input"
8
:Edge
trg
:Edge
src
:Location
trg
:Edge
src
:Edge
src
trg
:Location
:Update
:Guard
exp="i++"
exp="!(i<=input)"
Java over EMF API
Concrete Syntax
Defined by Java code
while (i <= input){
i++;
}
1. Traversal by code
2. Manual model building
3. No traceability
Abstract Syntax
for(state:block)
- High Maintenance
- Low Reusability
+ Easy to start
1
instanceof
A,B,CState
block
:WhileStatement
Factory.create
condition
:Block
:ConditionTest
:Increment
:Relation
:VariableRef
name = "i"
op="<="
:VarRef
name = "i"
:VarRef
name = "input"
2
:Guard
exp="!(i<=input)"
:Edge
trg
setTarget()
:Edge
src
:Location
trg
:Edge
src
:Edge
src
trg
:Location
:Update
:Guard
exp="i++"
exp="!(i<=input)"
Transformation code
Location transform(WhileStatement w) {
for(Statement s: w.block.statements) {
/* map the inner states */}
for(Location l : locations) {
/* Link the locations to a circle */}
// Map the condition
// Set the guards of the outgoing edges
}
w.block.increment.variableRef.name
1
l = factory.createLocation();
2
3
e.setSource(locationMap.get(
edgeMap.get(w.condition)));
9
M2M Languages
• Example: ATL
• Alternatives:
o
o
o
o
Epsilon
QVT
Xtend
…
Concrete Syntax
while (i <= input){
i++;
}
Abstract Syntax
:Guard
block
:WhileStatement
exp="!(i<=input)"
condition
:Block
:ConditionTest
:Increment
:Relation
:VariableRef
name = "i"
op="<="
:VarRef
name = "i"
:VarRef
name = "input"
:Edge
trg
:Edge
src
:Location
trg
:Edge
src
:Edge
src
trg
:Location
:Update
:Guard
exp="i++"
exp="!(i<=input)"
ATL Code
module Alf2UPPAAL; create OUT : Machine from IN : Block {
rule State2Location {
rule Condition2Guard {
from s: Alf!State
from s: Alf!Condition
to
l: UPPAAL!Location}
to
positiveGuard: UPPAAL!Guard(
rule Transition2Edge {
from s1: Alf!State,
negativeGuard: UPPAAL!Guard(
s2: Alf!State ( /* next state */ )
to
e: UPPAAL!Edge( src <- /*...*/
trg <- /*...*/ )}
10
location <- /*...*/
expression <- /*...*/)
location <- /*...*/
expression <- /*...*/)}}
Declarative Queries + MT languages
Concrete Syntax
Defined by Queries +
Templates
1. Traversal Queries
2. Building by Templates
3. (Match, Result) traces
while (i <= input){
i++;
}
Abstract Syntax
While
match block
:Guard
:WhileStatement
exp="!(i<=input)"
condition
:Block
:ConditionTest
:Increment
:Relation
:VariableRef
name = "i"
Relation
match
http://eclipse.org/incquery
Queries
op="<="
:Edge
trg
While
trg
template
:VarRef
name = "i"
:VarRef
name = "input"
Templates
:Edge
src
:Location
src
:Edge
:Edge
src
trg
:Location
:Update
:Guard
exp="i++"
exp="!(i<=input)"
Relation
template
pattern While(W,Condition,States){
WhileStatement.condition(W,Condition);
WhileStatement.block(W,Block);}
def dispatch transform(WhileStatement w) {
val innerStates=WhilePattern.getStates(w).map[createState]
val condition=WhilePattern.getCondition(w)
/* link the edges */ }
pattern Relation(R,Op1,Op2){
Relation.left(R,Op1);
Relation.right(R,Op1);
Relation.op(R,"<=");}
def dispatch transform(Relation condition) {
val m=RelationPattern.getMatch(condition)
createGuard()=>[exp='''«m.op1.name» <= «m.op2.name»''']}
11
Query-based Features
Declarative build by Queries
1. Queries
2. Declarative model build
Concrete Syntax
while (i <= input){
i++;
}
Abstract Syntax
Object, References, Attributes
3. Implicit, referrable traces
"Guard Image of while"
:Guard
block
:WhileStatement
exp="!(i<=input)"
condition
:Block
:ConditionTest
:Increment
:Relation
:VariableRef
name = "i"
op="<="
:VarRef
name = "i"
:VarRef
name = "input"
http://eclipse.org/incquery
:Edge
trg
:Edge
src
:Location
trg
:Edge
src
:Edge
src
trg
:Location
:Update
:Guard
exp="i++"
exp="!(i<=input)"
Query Based Features
@QueryBasedObject(Location)
pattern Statement(S)
@QueryBasedObject(Guard)
@QueryBasedFeature(exp, "($Expression$)")
@TraceLookup(Incoming, Edge) @QueryBasedFeature(guard, Edge, Guard)
pattern PositiveWhileCondition(Incoming, Condition, Expression)
@QueryBasedObject(Edge)
@QueryBasedFeature(src, Edge, From)
@QueryBasedFeature(trg, Edge, To)
pattern nextState(From,To)
@QueryBasedObject(Guard)
@QueryBasedFeature(exp, "! ($Expression$)")
@TraceLookup(Outgoing, Edge) @QueryBasedFeature(guard, Edge, Guard)
pattern NegativeWhileCondition(Outgoing, Condition, Expression)
12
Technologies for M2T
Native Java over EMF API
Defined by Java code
1. Traversal by code
2. Manual text building
3. No traceability
Concrete Syntax
while (i <= input){
i++;
}
Abstract Syntax
:Guard
block
- High Maintenance
- Low Reusability
+ Easy to start
:WhileStatement
exp="!(i<=input)"
condition
:Block
:ConditionTest
:Increment
:Relation
:VariableRef
name = "i"
op="<="
:VarRef
name = "i"
:VarRef
name = "input"
:Edge
trg
:Edge
src
:Location
trg
:Edge
src
:Edge
src
trg
:Location
:Update
:Guard
exp="i++"
exp="!(i<=input)"
Transformation code
Location transform(WhileStatement w) {
for(Statement s: w.block.statements) {
/* map the inner states */}
for(Location l : locations) {
/* Link the locations to a circle */}
// Map the condition
// Set the guards of the outgoing edges
}
"<location name=\"Location_"+ i +"\"/>"
14
2
„M2T”: Queries + AST generation
Model Template Code
Model Template Model
Grammar Code
Direct code generation
AST generation
Simple structure
Low complexity
Fast development
Linear output generation
(single pass)
⁻ Problematic formatting
⁻ Problematic M2C
synchronization
Represents the program
structure (PSM)
⁻ Can be very complex
⁻ Slower development
⁻ Distributed generation process
Support for M2C
synchronization
Incremental code generation
”pretty formatting”
E.g., Eclipse JDT
15
Chaining Transformations along
Views
Outlook: An Avionics Project
Avionics R&D project
o Model-driven toolchain
o Allocate SWs onto HWs
o Platform: ARINC 653
Component
database
Functional
Architecture
Platform
description
Allocation
Integrated
System
Model
Outlook: An Avionics Project
Avionics R&D project
o Model-driven toolchain
o Allocate SWs onto platform
Simplified Example
PilotControl
Simulink
tag: func
SubS1
FAM_PilotControl
: Function
SubS2
Navigation
tag: func
Id
Other SubSystem without tag
Port Blocks
InPort/OutPort
consumer
FAM_Navigation
: Function
tag: func
provider
nav2ems
:InformationLink
View
tag: func
Function SubSystem with "func" tag)
FAM_EMS
: Function
subFunctions
EMS
FMS
Id
FAM
consumer
FAM_FMS
: Function
id:Function
provider
id:InformationLink
EMS: Engine Management System
FMS: Flight Management System
18
nav2fms
:InformationLink
Maintanence
Maintenance:
• Incrementally
• Immediately
Summary of Behavior Modeling Tools
Alf
fUML
Tool
Version
Modified
Platform
Goal
fUML Ref. Impl.
1.1.0
2013-06
Java / console
Interpreter
Moka
1.0.0
2014-06
Eclipse
Execution engine
Moliz
1.0
2014-06
Eclipse
Execution engine
0.4.0
2014-05
Java / console
Interpreter
-
2014-07
Eclipse
Editor
4.0
2010-09
Application
Model Checker
Alf Ref. Impl.
Papyrus Alf Editor
UPPAAL
Maturity
• Proven: Eclipse platform, UPPAAL
• Early prototype: fUML engines (Moka, Moliz)
• Alpha: Alf editor in Papyrus is still in active development
19
Transformation
Summary of Transformation Tools
Tool
Version
Modified
Platform
Goal
EMF
2.10.0
2013-05
Eclipse
Metamodelling tool
ATL
3.5
2013-13
Eclipse
M2M transformation
XTend
2.7
2014-09
Eclipse
Template Language
IncQuery
0.8
2014-07
Eclipse
Query engine
Eclipse
M2M transformation
Query Based Feat.
Maturity
• Proven: Eclipse platform and core services (e.g. EMF, Xtend), ATL
• Stable: EMF-IncQuery (note: local developer support)
20
© Copyright 2024 ExpyDoc
