=Paper=
{{Paper
|id=None
|storemode=property
|title=Symbolic Execution of Satellite Control Procedures in Graph-Transformation-Based EMF
Ecosystems
|pdfUrl=https://ceur-ws.org/Vol-1069/09-paper.pdf
|volume=Vol-1069
|dblpUrl=https://dblp.org/rec/conf/models/NachtigallBE13
}}
==Symbolic Execution of Satellite Control Procedures in Graph-Transformation-Based EMF
Ecosystems==
https://ceur-ws.org/Vol-1069/09-paper.pdf
Symbolic Execution of Satellite Control
Procedures in Graph-Transformation-Based
EMF Ecosystems
Nico Nachtigall, Benjamin Braatz, and Thomas Engel
Université du Luxembourg, Luxembourg
firstname.lastname@uni.lu
Abstract. Symbolic execution is a well-studied technique for analysing
the behaviour of software components with applications to test case gen-
eration. We propose a framework for symbolically executing satellite con-
trol procedures and generating test cases based on graph transformation
techniques. A graph-based operational symbolic execution semantics is
defined and the executed procedure models are used for generating test
cases by performing model transformations. The approach is discussed
based on a prototype implementation using the Eclipse Modelling Frame-
work (EMF), Henshin and ECLiPSe-CLP tool ecosystem.
Keywords: symbolic execution, graph transformation, test case gener-
ation, triple graph grammars, EMF henshin
1 Introduction
Symbolic execution [4] is a well-studied technique for analysing the behaviour of
software components with applications to test case generation. The main idea is
to abstract from possibly infinite or unspecified behaviour. Uninitialised input
variables or external function calls are represented by symbolic variables with the
sets of possible concrete input values as value domains. Consequently, symbolic
program execution is rather based on symbols than on concrete values leading to
symbolic expressions which may restrict the value domains of the symbols. For
each execution path, a path constraint (PC) is defined by a dedicated boolean
symbolic expression. Solving the expression, i.e., finding a valuation for all con-
tained symbolic variables so that the expression is evaluated to true, provides
concrete input values under which the corresponding path is traversable. An
execution path is traversable as long as its path constraint is solvable.
In this paper, we propose a framework for symbolically executing satellite
control procedures (SCPs) and generating test cases based on graph transfor-
mation techniques [6]. We successfully apply graph transformation techniques
in an industrial project with the satellite operator SES (Société Européenne des
Satellites) for an automatic translation of SCPs from proprietary programming
languages to SPELL (Satellite Procedure Execution Language & Library) [8].
The safety-critical nature of SCPs implies that extensive testing is required after
Proceedings of MoDeVVa 2013 61
Symbolic Execution of Satellite Control Procedures in Graph-Transformation-Based EMF Ecosystems
translation. The presented approach allows us to generate tests without leaving
this graph-transformation-based ecosystem. We define a graph-based operational
semantics for symbolically executing SCPs for a subset of the SPELL language.
The executed procedure models are used for generating test cases by performing
model transformations. We discuss our approach based on a prototype imple-
mentation using the EMF Henshin [7] and ECLiPSe-CLP [9] tools.
Sec. 2 introduces the symbolic execution framework. In Sec. 3, the graph-
based operational symbolic execution semantics is defined. Sec. 4 presents model
transformation rules for test case generation and a prototype implementation for
the approach. Sec. 5 concludes the paper and compares with related work.
2 Models & Symbolic Execution Framework
The symbolic execution framework in Fig. 1 uses the abstract syntax tree (AST)
of a procedure, which defines a typed attributed graph [6]. The AST can be con-
structed by parsing the source code with appropriate tools (see Sec. 4). The AST
graph is symbolically executed using two graph transformation systems (GTSs).
A GTS is a set of graph transformation rules where each rule may create or delete
nodes and edges or update attribute values. In phase one, the GTS GTS F low
is used to annotate AST with execution flow information leading to graph
AF = AST + FLOW . In phase two (symbolic execution), the GTS GTS Sym
is exhaustively applied to AF leading to graphs State i = AF + SYM i , i = 1..n
representing the status of the execution.
Fig. 2 shows the running example in a small subset of the SPELL language
[8]. SCP “Charge Batteries” retrieves the state of charge (SC) of both batteries
of a satellite, defines a minimal threshold min of 50%, and switches to the battery
with higher SC if it exceeds min. Otherwise, an alert is issued. Meta-model SCP
specifies the general syntax of ASTs for such procedures. A procedure Proc con-
sists of a list of statements Stmnt (assignments Asg, function calls FnCall, defini-
tions FnDef or branching If structures) with explicit next pointers. Function calls
contain a list of arguments (arg) and function definitions contain a list of param-
eters (pm). An assignment contains a variable (var) and an assigned expression
(ex). Expressions (Expr) are either numbers (Number), variables (Var) or Boolean
expressions (Bool) with operator (<, <=, >, >=, and, or) and operands (left (le)
and right (ri)). Complex statements (If,FnDef) contain a block (B) that references
a list of statements. Furthermore, If statements have a boolean condition cond
and may have else and ElIf structures (edge el). The AST for the procedure is a
graph typed over meta-model SCP. Graph FLOW represents the flow annotation
of AST . Places P are assigned (dotted edges asg) to nodes in AST that should
Annotate Stepwise Model checking
Graph based E-Flow Symbolic invariant properties
SCP Model
AF Detection of unreachable
Information Execution
AST (apply GTS Flow ) AST P
ASTP00 (apply GTS Sym ) („dead“) model fragments
State 1.. n Test case generation
Fig. 1. Steps of Symbolic Model Execution
Proceedings of MoDeVVa 2013 62
Symbolic Execution of Satellite Control Procedures in Graph-Transformation-Based EMF Ecosystems
cond
Bool Number Var Stmnt next Proc
FnDef f
Op op Int i Id v FnCall
Pm Arg arg Id fn first
Id fn B bl,else If
var pm arg
le,ri pm body el
Expr ex Asg
first :Proc asg :P on
pc=…and(S0>S1,…)…
1 DEF switch & charge (x ,
2 y, :FnDef :P
3 min ): fn=switch&charge
:Token
4 IF x > y AND pm f
body :Pm
eval=true
5 x > min : :P n
... pm v=‘x‘ l ...
sym=2
6 Send ( ’ S W I T C H _ B 1 &
:B :P n
lines 1-11
7 C H A R G E _ B 2 ’) ... l ...
8 el
f :If f,l :P
9 ELIF y > min : ... l ...
cond bl
10 Send ( ’ S W I T C H _ B 2 & f hi lo
:Bool :P
11 C H A R G E _ B 1 ’) next le op=AND ri c c
f l
12 ...
13 s0 = GetTM ( ’ SC1 ’) :Bool :P n ...
le op=> ri f
14 s1 = GetTM ( ’ SC2 ’) l
...
15 min =50 :Var ...
term=S0
:P n
:Symb
16 v=‘x‘ lst
n :P f
l.13
17 switch & charge ( s0 , next :Asg ex
... var ... f,l ... c
18 s1 , :FnCall ... ...
19 min ) next n :P l nxt
fn=swi... f
lines 14-23
20 arg n
:Arg
term=S1
21 IF s0 <= min AND next n :P ...
:Symb
n
22 s1 <= min : ... arg v=‘s0‘ ... c
23 Alert () :If :P l
AST FLOW SYMn
Fig. 2. SCP meta-model (top), SCP “Charge Batteries” (left), SCP model (AST), flow
annotation (FLOW) and symbolic execution elements (SYMn )
be executed. P nodes can be connected by f,l or n edges in order to indicate which
other nodes need to be executed at first, next or last before finishing the execu-
tion of a node, e.g., in order to execute the procedure (node Proc), the assignment
in line 13 (node Asg) needs to be executed first. For each execution path, a Token
representing the current execution point with path constraint is created (in total
six Tokens for the example). In graph SYM n , the Token node on place P that
is assigned to node Proc indicates that the procedure was evaluated (eval=true)
with path constraint pc=and(and(S0 >S1 ,S0 >50),not(and(S0 <=50,S1 <=50))) and
symbolic variables S0 , S1 (Symb) for GetTM(’SC1’) and GetTM(’SC2’) by enter-
ing line 6 but not line 23. The resulting graphs State 1..n can be used for model
checking invariants, detection of dead model fragments or test generation.
3 Operational Execution Semantics
The execution semantics is divided into the execution flow of the AST graph
and the token semantics for traversing all flow paths. Fig. 3 shows the rules of
GTS F low and GTS Sym in short-hand notation, i.e., nodes and edges marked
with <+> are created, those marked with <-> are deleted and attribute values of
the form [x=>y] are updated from x to y when applying the rule. Nodes marked
with have a “hidden” translation attribute that is updated [false=>true]
during rule application so that the rule is only applied once. A more formal
definition of graph transformation in general is given in [6].
Proceedings of MoDeVVa 2013 63
Symbolic Execution of Satellite Control Procedures in Graph-Transformation-Based EMF Ecosystems
Rule Init1 specifies that the first statement of a procedure needs to be exe-
cuted first. An initial token is put on the first place with path constraint true
and eval=false. Rule Stmnt1 defines that successive statements need to be exe-
cuted successively. Note that the first statement in Fig. 2 is a FnDef. Therefore,
another rule defines that the succeeding statement needs to be executed first
until there is no more FnDef. Rule Asg1 defines that the expression of an assign-
ment needs to be evaluated first before assigning the resulting value. The rule
for blocks is defined analogously. Rule Bool1 defines that the left operand has to
be evaluated before the right operand. Rule If 1 , branches the flow - the condition
is evaluated before executing the block (hi - positive condition) or an “empty”
place (lo - negative condition). Rule ElIf 1 links the “empty” place of rule If 1 to
the alternative If. Rule Else1 is defined analogously.
Rule TFst2 moves the token to the first child place (edge f) as long as possible.
Rule TNxt2 moves the token of an evaluated place to the next place (edge n) and
changes attribute eval to false. The rules implement a left-most inner-most evalu-
ation strategy. Rule GetTM2 evaluates each GetTM-FnCall to a path-wide unique
symbolic variable (Symb) Si (uniqueness is given by token attribute sym which is
increased by one). Note that Symbs are ordered in their occurence of evaluation
which is important for a later test generation. Rule GetTM2 requires that a last
Symb already exists. An analogue rule creates a last Symb if not existent. Rule
Asg2 assigns the term of the evaluated expression to the variable Var and sets the
assignment as evaluated by moving token edge on. Rule BoolAnd2 concatenates
Init1 Stmnt1 Asg1 Bool1 If1 ElIf1
<+> l :P hi lo
:Token<+> :P :P <+> :P <+>
n :P <+> :P lo<+> :P
eval=false <+> <+> <+> <+>
:P
pc=true l <-> f,l :P :P f
<+>
sym=0 on <+> f l <+> f <+>
:P n :P <+> :P <+> :P l
<+>
<+>
<+> <+> <+> <+> l :P l
<+> <+>
<+>
<+>
:P f,l :P <+> <+>
<+> <+> :Asg :Bool bl cond
le ri :If :If
<+> first <+> next ex el
:Proc :Stmnt :Stmnt :Stmnt :Expr :Expr :Expr :B :Bool :If
TFst2 TNxt2 GetTM2 :FnCall Asg2
:P f :P :P n :P :P fn='GetTM' :P l :P :Asg :Var
<-> <+> <+> c :Symb<+> <+> var Id v
<-> <+> on on nxt :Symb :Term
c
on on <+> c term=Si term=t on<+>
on lst<+> on
:Token :Token c :Var<+>
eval=[true <->
:Token eval=[false=>true] :Token name=v
eval=false =>false] sym=[i=>i+1] <-> eval=true in<+> val=t
lst
BoolAnd2 Branch2 :P hi :P lo :P :Var<+> Check2
:P f :P l :P :Bool :Term name=v
eval=[check=>false]
c op=‘and‘ on term=t c on on val=vt
<+> c <+> c <-> <+>
sat(pc)=true
c :Token :Token<+>
:Token
:Term :Term<+> :Term :Var eval=[true=>check] eval=check in
term=t1 term=and(t1,t2) term=t2 name=v pc=[pc=>and(pc,t)] pc=[pc=> <+>
<+> c on on val=vt
<+> <-> sym=i and(pc,
pc=pc
c not(t))]
c :Token c <+> sym=i
eval=true in :Symb c
Fig. 3. Rules for annotation (top, GTS Flow ) and symbolic execution (bottom, GTS Sym )
Proceedings of MoDeVVa 2013 64
Symbolic Execution of Satellite Control Procedures in Graph-Transformation-Based EMF Ecosystems
both evaluated operands with and. Analogue rules for boolean expressions with
other operators (or,<,>,etc.) are defined. Amalgamated rule Branch2 duplicates
the token with all connected variables and symbols, negates the condition (not(t))
for the lo path and concatenates the condition with the path constraint. Rule
Check2 checks, if the path constraints of duplicated tokens are still satisfiable af-
ter a branch (attribute condition sat(pc)=true). If the path constraint of a token
becomes unsatisfiable, the token status eval remains check and the token can not
be moved any more. After simulating the example in Fig. 2, three tokens from
six possible paths are assigned to node Proc with eval=true while the other three
tokens remain at the last If statement with unsolvable path constraints. Only
tokens that are assigned to node Proc with eval=true are considered during test
case generation (they represent execution paths with solvable path constraints).
Additional rules are defined for annotating and traversing function calls and def-
initions. A function is traversed every time it is called so that global side effects
in execution can be respected, e.g., operations on call by reference arguments.
4 Implementation & Test Case Generation
A procedure is parsed with Xtext [5] to an EMF AST graph first. Then, the EMF
Henshin tool [7] is used in combination with the ECLiPSe constraint solver [9] to
execute the AST graph by automatic rule applications and satisfiability checking
/ solving constraints. The AST graph is completely preserved during execution.
Correspondences between symbolic variables of path constraints (nodes of type
Symb) and AST graph structures are used for test generation by applying the
forward model transformation (FT) rules in Fig. 4. An FT rule [8] consists of
a source graph GS , correspondence graph GC and target graph GT . While GS
is parsed, nodes and edges in GC , GT are created. Applying the rules yields a
graph that is serialised to test case files with Xtext. Rule Proc2Test creates a Test
suite for a procedure. Rule Token2Case creates a test case for each execution path
with solvable path constraint. Rule LstSymb2KeyElem adds a key tm for each last
(edge lst) evaluated GetTM(tm) function call of an execution path to the test
case with a list containing a test input valuation for symbolic variable s as first
(edge fst) element so that path constraint pc is satisfied (solve(s,pc)). A second
rule handles all previous symbolic variables. Symbolic variables are ordered in
order to reflect the sequential execution order of the represented GetTM function
calls which is needed for proper test generation with test inputs in correct order.
Proc2Test Token2Case LstSymb2KeyElem
GS GC GT GS GC GT GS GC GT
val=solve(s,pc)
:Proc :C :Test :Proc :C :Test :Token
:ListElem<+>
<+> :C :Case
pc=pc
<+>
<+>
<+> :FnCall <+>
lst :P
<+>
:P case <+> k
fn=‘GetTM‘
<+>
on c fst
<+>
<+>
:Token :Case :Symb
:Arg :Key<+>
:C term=s val=tm
<+> arg name=tm
Fig. 4. Rules for test case generation
Proceedings of MoDeVVa 2013 65
Symbolic Execution of Satellite Control Procedures in Graph-Transformation-Based EMF Ecosystems
5 Conclusion & Related Work
We have presented a framework for symbolically executing simple satellite proce-
dures. The approach preserves the correspondences between symbolic variables
and the AST, so that the result graph can be used for test case generation by
performing model transformations afterwards. A prototype implementation for
the symbolic execution and test case generation framework has been presented.
In contrast to interpreter based symbolic execution engines [1,3] of program-
ming languages, our graph-transformation-based approach allows symbolic exe-
cution on a more abstract level enabling its formal analysis and application to
other languages and behavioural diagrams in future work. In [2], an abstract
symbolic execution framework based on term rewriting is proposed. In contrast
to our approach, the correspondences between symbolic variables and the pro-
gram term are not preserved. Research on how to transfer and enhance results
from term to graph rewriting approaches for symbolic execution is topic of future
work. In [10], the execution of UML state machines is presented but diagram–
path-constraint correspondences are not specified explicitly.
In future work, we plan to extend the symbolic execution semantics for ap-
plicability to industrial SPELL SCPs [8] and analyse its correctness w.r.t. a
formal SPELL semantics that needs to be defined first. We will investigate im-
portant properties of symbolically executed models that should be preserved
during model refactorings and how to ensure their preservation. Moreover, we
will assess the scalability of our approach.
References
1. Anand, S., Pasareanu, C.S., Visser, W.: JPF-SE: A symbolic execution extension
to java pathfinder. In: TACAS. pp. 134–138 (2007)
2. Arusoaie, A., Lucanu, D., Rusu, V.: A Generic Approach to Symbolic Execution.
Tech. Rep. RR-8189, INRIA (Dec 2012)
3. Cadar, C., Dunbar, D., Engler, D.: Klee: unassisted and automatic generation
of high-coverage tests for complex systems programs. In: Proceedings of the 8th
USENIX conference on Operating systems design and implementation. pp. 209–
224. OSDI’08, USENIX Association, Berkeley, CA, USA (2008)
4. Cadar, C., Sen, K.: Symbolic execution for software testing: three decades later.
Commun. ACM 56(2), 82–90 (Feb 2013)
5. The Eclipse Foundation: Xtext (2013), http://www.eclipse.org/Xtext/
6. Ehrig, H., Ehrig, K., Prange, U., Taentzer, G.: Fundamentals of Algebraic
Graph Transformation, vol. EATCS Monographs in Theoretical Computer Science.
Springer (2006)
7. EMF Henshin (2013), http://www.eclipse.org/modeling/emft/henshin/
8. Hermann, F., Gottmann, S., Nachtigall, N., Braatz, B., Morelli, G., Pierre, A., En-
gel, T.: On an Automated Translation of Satellite Procedures Using Triple Graph
Grammars. In: Proc. ICMT’13, LNCS, vol. 7909, pp. 50–51. Springer (2013)
9. Schimpf, J., Shen, K.: Eclipse - from lp to clp. Theory and Practice of Logic
Programming 12, 127–156 (2012)
10. Zurowska, K., Dingel, J.: Symbolic execution of UML-RT State Machines. In: Proc.
of SAC ’12. pp. 1292–1299. SAC ’12, ACM (2012)
Proceedings of MoDeVVa 2013 66