C. Dubois, P. Masci, D. Mé y (Eds.): F-IDE 2016
EPTCS 240, 2017, pp. 38–52, doi:10.4204/EPTCS.240.3
© G. Le Gue nic, B. Combemale & J.A. Galindo
This wo k is licensed unde he
C ea i e Commons A ibu ion License.
Indus ial Expe ience Repo on he Fo mal Speci ica ion o a
Packe Fil e ing Language Using he K F amewo k
Gu an LEGUERNIC
DGA Maî ise de l’In o ma ion
35998 Rennes Cedex 9, F ance
Benoi COMBEMALE José A. GALINDO
INRIA RENNES – BRETAGNE ATLANTIQUE
Campus uni e si ai e de Beaulieu
35042 Rennes Cedex, F ance
Many p ojec -speci ic languages, including in pa icula il e ing languages, a e de ined using non-
o mal speci ica ions w i en in na u al languages. This leads o ambigui ies and e o s in he speci-
ica ion o hose languages. This pape epo s on an indus ial expe imen on using a ool-suppo ed
language speci ica ion amewo k (K) o he o mal speci ica ion o he syn ax and seman ics o a
il e ing language ha ing a complexi y simila o hose o eal-li e p ojec s. This expe imen a ion
aims a es ima ing, in a speci ic indus ial se ing, he di icul y and bene i s o o mally speci ying a
packe il e ing language using a ool-suppo ed o mal app oach.
1 In oduc ion
Packe il e ing (accep ing, ejec ing, modi ying o gene a ing packe s, i.e. s ings o bi s, belonging
o a sequence) is a ecu ing p oblema ic in he domain o in o ma ion sys ems secu i y. Such il e s
can se e, among o he uses, o educe he a ack su ace by limi ing he capaci ies o a communica ion
link o he legi ima e needs o he sys em i belongs o. This ype o il e ing can be applied o ne wo k
links (which is he mos common use), p oduc in e aces, o e en on he communica ion buses o a
p oduc . I he il e ing policy needs o be adap ed du ing he deploymen o ope a ional phases o he
sys em o p oduc , i is o en equi ed o design a speci ic language L(syn ax and seman ics) o exp ess
new il e ing policies du ing he li e ime o he sys em o p oduc . This language is he basis o he
il e s ha a e applied o he sys em o p oduc . Hence, i plays an impo an ole in he secu i y o
his sys em o p oduc . I is he e o e impo an o ha e s ong gua an ees ega ding he exp essi i y,
p ecision, and co ec ness o he language L(meaning ha e e y hing ha need o be exp essed can,
and ha e e y hing ha can be exp essed has he mos ob ious seman ics). Those gua an ees can be
pa ly p o ided by a o mal design (and de elopmen ) p ocess.
Among di e se du ies, he DGA (Di ec ion Géné ale de l’A memen , a ench p ocu emen agency)
is in ol ed in he supe ision o he design and de elopmen o il e ing componen s o p oduc s. Those
il e s come in a ying shapes and oles. Some o hem a e ne wo k appa a uses il e ing s anda d In-
e ne p o ocol packe s (such as i ewalls); while o he s a e small pa s o in eg a ed ci cui s il e ing
speci ic p op ie a y packe s ansi ing on compu e buses. Thei common de ini ion is: “a ool si ing
on a communica ion channel, analyzing he sequence o packe s (s ings o bi s wi h a beginning and an
end) ansi ing on ha channel, and po en ially d opping, modi ying o adding packe s in ha sequence”.
Whene e he il e ing algo i hm applied is ixed o he li e ime o he componen o p oduc , his algo-
i hm is o en “ha d coded” in o he componen o p oduc wi h he po en ial addi ion o a con igu a ion
ile allowing o sligh ly al e he beha io o he il e . Howe e , some imes he il e ing algo i hm o
apply may depend on he deploymen con ex , and may ha e o e ol e du ing he li e ime o he compo-
nen o p oduc o adap o new uses o a acke s. In his case, i is o en necessa y o be able o easily
G. Le Gue nic, B. Combemale & J.A. Galindo 39
w i e new il e ing algo i hms o he speci ic p oduc and con ex . Those algo i hms a e hen o en de-
sc ibed using a Domain Speci ic Language (DSL) ha is designed o he exp ession o a speci ic ype o
il e s o a speci ic p oduc . The de ini ion o he syn ax and seman ics o his DSL is an impo an ask.
This DSL is he link be ween he il e ing objec i es and he p ocess ha is eally applied on he packe
sequences. O en, language speci ica ions (when he e is one) a e p o ided using na u al language. In
he majo i y o cases, his leads o ambigui ies o e o s in he speci ica ion which p opaga e o imple-
men a ions and inal use code. This is o example he case o common languages such as C/C++ o
Ja a™ [12].
“Un o una ely, he cu en speci ica ion has been ound o be ha d o unde s and and has
sub le, o en unin ended, implica ions. Ce ain synch oniza ion idioms some imes ecom-
mended in books and a icles a e in alid acco ding o he exis ing speci ica ion. Sub le,
unin ended implica ions o he exis ing speci ica ion p ohibi common compile op imiza-
ions done by many exis ing Ja a i ual machine implemen a ions. [...] Se e al impo an
issues, [...] simply a en’ discussed in he exis ing speci ica ion.”
JSR-133 expe g oup [12]
Some o hose ambigui ies, as he memo y model o mul i- h eaded Ja a™ p og ams [12], equi ed a
o mal speci ica ion in o de o be sol ed.
This pape is an indus ial expe ience epo on he use o a ool-suppo ed language speci ica ion
amewo k ( he K amewo k) o he o mal speci ica ion o he syn ax and seman ics o a il e ing
language ha ing a complexi y simila o hose o eal-li e p ojec s. The ool used o o mally speci y
he DSL is in oduced in Sec . 2. Fo con iden iali y easons, in o de o be allowed by he DGA o
communica e on his expe imen a ion, he language speci ied o his expe imen is no linked o any
pa icula p oduc o componen . I is a gene ic packe il e ing language ha ies o co e he majo i y
o ea u es equi ed by packe il e ing languages. This language is in oduced in Sec . 3 while i s o mal
speci ica ion is desc ibed in Sec . 4. This language is es ed in Sec . 5 by implemen ing and simula ing
a il e ing policy en o cing a sequen ial in e ac ion o a made-up p o ocol simila o DHCP. Be o e
concluding in Sec . 7, his pape discusses he esul s o he expe imen a ion in Sec . 6.
2 In oduc ion o he KF amewo k
Su p isingly, e en i i is a niche o ools, he e exis s qui e a numbe o ools speci ically dedica ed o
he o mal speci ica ion o languages (ou ocus in his wo k is on speci ying a he han implemen ing
DSLs). Those ools include among o he s: PLT Redex [6, 13], O [23], Lem [19], Maude MSOS
Tool [3], and he K amewo k [20, 26]. All hose ools ocus on he (clea o mal) speci ica ion o
languages a he han hei (e icien ) implemen a ion, which is mo e he ocus o ools and languages
such as Rascal [16, 2, 15] o i s ances o The Me a-En i onmen [14, 25], Ke me a [9, 10], and o he s.
PLT Redex is based on educ ion ela ions. PLT Redex is an ex ension (in e nal DSL) o he Racke
p og amming language [7]. O and Lem a e mo e o ien ed owa ds heo em p o e s. O and Lem allow
o gene a e o mal de ini ions o he language speci ied o Coq, HOL, and Isabelle. In addi ion, Lem
can gene a e execu able OCaml code. O is mo e p og amming language syn ax o ien ed, while Lem is
a mo e gene al pu pose seman ics speci ica ion ool. O and Lem can be used oge he in some con ex s.
The Maude MSOS Tool, whose de elopmen has s opped in 2011, is based on an encoding o modula
s uc u al ope a ional seman ics (MSOS) ules in o Maude. Simila ly o he Maude MSOS Tool, he K
amewo k is based on ew i ing and was also o iginally implemen ed on op o Maude.
40 Fo mal Speci ica ion o a Packe Fil e ing Language Using he K F amewo k
The goal se o he expe imen epo ed in his pape is o es ima e he di icul y and bene i s o
an a e age enginee (i.e. an enginee wi h educa ion and expe ience in compu e science bu no speci ic
knowledge in o mal language seman ics) o use an “app op ia e” ool o he o mal speci ica ion o a
packe il e ing language. The “app op ia e” ool needs o: be easy o use; be able o p oduce (o ake
as inpu ) “human eadable” language speci ica ions; p o ide some le el o co ec ness gua an ees o
he language speci ied; and be execu able (simula able) in o de o es (e alua e) he language speci ied.
The K amewo k seems o mee hose equi emen s and has been chosen o be he “app op ia e” ool
a e a sho e iew o a ailable ools. As he e has been no in dep h compa ison o he di e en ools
a ailable, he e is no claim in his pape ha he K amewo k is be e han he o he ools, e en in ou
speci ic se ing.
This sec ion in oduces he K amewo k [21] by elying on he example o a language allowing
o compu e addi ions o e numbe s using Peano’s encoding [8]. The Ksou ce code o his language
speci ica ion is p o ided below.
1module PEANO - SYNTAX
syn ax Nb ::= " Ze o" |"Succ" Nb
3syn ax Exp ::= Nb | Id | Exp "+" Exp [s ic ,le ]
syn ax S m ::= Id ":=" Exp ";" [s ic (2) ]
5syn ax P g ::= S m | S m P g
endmodule
7
module PEANO impo s PEANO - SYNTAX
9syn ax KResul ::= Nb
11 con igu a ion
<en colo ="g een"> .Map </en >
13 <k colo =" cyan"> $PGM :K </k>
15 ule N:Nb + Ze o => N
ule N1:Nb + Succ N2:Nb => ( Succ N1 ) + N2
17
ule
19 <en > ... Va :Id |-> Val:Nb ... </en >
<k> ( Va :Id => Val :Nb ) ... </k>
21
ule
23 <en > Rho:Map (. Map => Va |-> Val ) </en >
<k> Va :Id := Val:Nb ; => . ... </k>
25 when no Bool ( Va in keys (Rho))
27 ule
<en > ... Va |-> ( _ => Val ) ... </en >
29 <k> Va :Id := Val:Nb ; => . ... </k>
31 ule S:S m P:P g => S ~> P [ s uc u al]
endmodule
G. Le Gue nic, B. Combemale & J.A. Galindo 41
AKde ini ion is di ided in o h ee pa s: he syn ax de ini ion, he con igu a ion de ini ion, and he
seman ics ( ew i ing ules) de ini ion. The de ini ion o he language syn ax is gi en in a module whose
name is su ixed wi h “-SYNTAX”. I uses a BNF-like no a ion [1, 17]. E e y non- e minal is in oduced
by a syn ax ule. Fo example, he de ini ion o he no a ion o numbe s (Nb) in his language, p o ided
on line 2, is equi alen o he de ini ion gi en by he egula exp ession “(Succ)*Ze o”.
•
Map
en
$PGM:K
k
Figu e 1: Peano’s Kcon igu a ion
The con igu a ion de ini ion pa is in oduced by he keywo d
con igu a ion and de ines a se o (po en ially nes ed) cells de-
sc ibed in an XML-like syn ax. This con igu a ion desc ibes he
“abs ac machine” used o de ining he seman ics o he language.
The ini ial s a e (o con igu a ion) o he abs ac machine is he one
desc ibed in his con igu a ion pa . The pa sed p og am (using he
syn ax de ini ion o he p e ious pa ) is pu in he cell con aining he $PGM a iable (o ype K). Fo he
Peano language, he en cell is used o s o e a iable alues in a map ini ially emp y (.Map is he emp y
map). F om his de ini ion, he K amewo k can p oduce a g aphical ep esen a ion o he con igu a ion,
p o ided in Fig. 1
The seman ics de ini ion pa is composed o a se o ew i ing ules, each one o hem in oduced
by he keywo d ule. In he Ksou ce ile, ules a e oughly deno ed as “CCF => NCF” whe e CCF
and NCF a e con igu a ion agmen s. The meaning o “CCF => NCF” can be summa ized as: i CCF
is a agmen o he cu en abs ac machine s a e (o con igu a ion) hen he ule may apply and he
agmen ma ching CCF in he cu en con igu a ion would hen be eplaced by he new con igu a ion
agmen NCF. In o de o inc ease he exp essi i y o ules, CCF may con ain ee a iables ha a e
eused in exp essions in NCF. I a speci ic alua ion o he ee a iables Vin CCF allows a agmen o
he cu en con igu a ion o ma ch CCF, hen his agmen may be eplaced by NCF whe e he a iables
Va e eplaced by hei ma ching alua ion.
The ules o addi ion o e numbe s (Nb and no Exp), on lines 15 and 16, ollows closely his
ep esen a ion. Fo hose ules, CCF is a p og am agmen ha can be ma ched in any cell o he con ig-
u a ion. Fo hose wo ules, he K amewo k can hen p oduce he ollowing g aphical ep esen a ions:
RULE
N:Nb + Ze o
N
RULE
N1:Nb + Succ N2:Nb
(Succ N1)+N2
Fo o he ules, he con igu a ion agmen ma ching is mo e complex and in ol es p ecise con-
igu a ion cells ha a e explici ly iden i ied. In o de o comp ess he ep esen a ion, CCF and NCF
a e no s a ed sepa a ely anymo e. The common pa s a e s a ed only once, and he pa s di e ing a e
again deno ed “CCFi=> NCFi”, whe e CCFiis a sub- agmen in CCF and NCFiis he co esponding
sub- agmen in NCF. Cells ha ha e no impac on a ule Rand a e no impac ed by Rdo no appea
explici ly in he ule. Cells heads and ails (po en ially emp y) ha a e no modi ied by a ule can be
deno ed “...”, ins ead o using a ee a iable ha would no be eused.
Fo example, he ule which s a s on line 18is he ule used o e alua e a iables. The cu en
con igu a ion needs o con ain a mapping om a a iable Va o a alue Val (“X |-> V” deno es a
mapping om X o V) somewhe e in he map con ained in he en cell. I also needs o con ain he a iable
Va a he beginning o cell k. This ule has he e ec o eplacing he ins ance o Va a he beginning
o cell kby he alue Val. Fo his ule, he K amewo k gene a es he g aphical ep esen a ion gi en in
Fig. 2.
The las ule on line 31 in ol es o he in e nal aspec s o he K amewo k. I oughly s a es ha ,
in o de o e alua e a s a emen S ollowed by he es Po he p og am, Smus i s be e alua ed o a
42 Fo mal Speci ica ion o a Packe Fil e ing Language Using he K F amewo k
KResul (de ined on line 9) and hen Pis e alua ed.
3 GPFL Con ex
RULE
Va :Id 7→ Val:Nb
en
Va :Id
Val:Nb
k
Figu e 2: Peano’s K ule o a iables
The language speci ied in he expe imen epo ed in his
pape , named GPFL, is a gene ic packe il e ing language.
Fo con iden iali y easons, GPFL is no a language ac ually
used in any speci ic eal p oduc . GPFL has been made-up
in o de o be able o communica e on he expe imen a ion
on ool suppo ed o mal speci ica ion o il e ing languages
epo ed in his pape . Howe e , GPFL co e s he majo i y
o ea u es needed in packe il e ing languages deal wi h
by he DGA. GPFL can be seen as he “mo he ” o he ma-
jo i y o packe il e ing languages.
GPFL aims a exp essing a wide a ie y o il e s. Those il e s can be placed a he le el o ne -
wo k, in e aces, o e en communica ion buses be ween elec onic componen s. They can be applied on
s anda d p o ocols such as IP, TCP, UDP, . . . o on p op ie a y p o ocols, which a e mo e common o
componen communica ion p o ocols. Howe e , all hose il e s a e assumed o be placed on a commu-
nica ion link. Messages (packe s) ha ge h ough he il e can only ge h ough in wo ways, ei he
“going in” o “going ou ”; he e is no swi ching aking place in GPFL il e s. Those di e en use cases
a e illus a ed in Fig. 3.
in
ou
GPFL il e
(a) Ne wo k il e ing
in
ou
GPFL il e
in
ou
GPFL il e
(b) In e ace il e ing
in
ou
GPFL il e
in
ou
GPFL il e
(c) Bus il e ing
Figu e 3: Use cases o GPFL-based il e s
GPFL ocuses on he in e nal logic o he il e . Decoding and encoding o packe s is assumed o be
handled ou side o GPFL p og ams ( il e s), po en ially using echnologies such as ASN.1 [11, 5]. Fo
GPFL p og ams, a packe is a eco d (a se o alued ields). A GPFL p og am (dynamically) inpu s a
sequence o eco ds and ou pu s a sequence o eco ds. Figu e 4 desc ibes he a chi ec u e o GPFL-
based il e s. An incoming packe (on ei he side) is i s pa sed (decoded) be o e being handed o e o

G. Le Gue nic, B. Combemale & J.A. Galindo 43
he GPFL p og am. I he packe can no be pa sed, depending on he ype o il e (whi e lis o black
lis ), he packe is ei he d opped o passed o he o he side wi hou going h ough he GPFL p og am.
Any packe ( eco d) ou pu by he GPFL p og am (on ei he side) is encoded be o e being sen ou . In
addi ion, he GPFL p og am can gene a e ala ms due o packe s no complying wi h he encoded il e ing
policy.
GPFL
Fil e
Ala m
Decode Encode
Decode Encode
bin
bin
P
o
P
o
whi e
lis black lis
whi e
lis
black lis
Figu e 4: A chi ec u e o GPFL-based il e s
The GPFL language mus allow o: d op, modi y o accep he cu en packe being il e ed; gene a e
new packe s; and gene a e ala ms. GPFL mus allow o base he decision o ake any o hose ac ions on
in o ma ion pieces conce ning he cu en packe being il e ed and p e iously il e ed packe s. Those in-
o ma ion pieces mus include: some iming in o ma ion, cu en o p e ious packe s di ec ions h ough
he il e (“in” o “ou ”), and cha ac e is ics o cu en o p e ious packe s including ield alues and
compu ed p ope ies such as, o example, a packe “ ype” o o al leng h. The compu a ion o hose
p ope ies and decoding o packe ields is ou side o he scope o GPFL; i is le o he decode s.
In o de o g adually build a decision, GPFL mus allow o in e ac wi h a iables ( eading, w i -
ing, and compu ing exp essions) and au oma a ( igge ing a ansi ion in an au oma on and que ying i s
cu en s a e). The in en o au oma a is o be used o ack he cu en s ep o sessions o complex p o-
ocols. GPFL mus allow o combine il e ing s a emen s using: sequen ial con ol s a emen s (execu ing
wo s a emen s in sequence); condi ional con ol s a emen s (execu ing a s a emen only i a condi ion is
ue); i e a ing con ol s a emen s ( epea edly execu ing a s a emen o a ixed numbe o epe i ions).
The e is no equi emen o a loop (o while) s a emen whose exi condi ion is con olled by an exp es-
sion ecompu ed a e e e y i e a ion. Fo he expe imen epo ed in his pape (on o mal speci ica ion
o a il e ing language), he i e a ing s a emen is conside ed su icien o he in ended use o GPFL and
close enough o a loop s a emen om a seman ics poin o iew, while exhibi ing in e es ing p ope ies
o u u e analyses ( o example, any GPFL p og am e mina es).
4 GPFL’s Speci ica ion
Due o lack o space, GPFL’s speci ica ion and es ing is only summa ized in his pape . Howe e , a ull
speci ica ion o GPFL and a es ing sec ion can be ound in he companion echnical epo [18].
44 Fo mal Speci ica ion o a Packe Fil e ing Language Using he K F amewo k
Syn ax. To he excep ion o exp essions and exp ession agmen s, GPFL’s syn ax is o mally de ined
by he Ksou ce agmen p o ided below.
18 syn ax Cmd ::= " nop" |"accep " |" d op" |" send (" Po "," Fields ")"
|" ala m (" Exp ")" [s ic (1)]
20 |"se (" Id "," Exp ")" [s ic (2)]
|"newAu oma on(" S ing "," Au oma onId ")"
22 |"s ep (" Au oma onId "," Exp "," S m ")" [s ic (2)]
syn ax S m ::= Cmd
24 |"cond (" Exp "," S m ")" [s ic (1)]
|"i e (" Exp "," S m ")" [s ic (1)]
26 |"newIn e up (" In "," Bool "," S m ")"
| S m S m [ igh ]
28 |"{" S m "}" [b acke ]
30 syn ax Au oma aDe ::= " AUTOMATA " S ing Au oma aDe Tail
syn ax Au oma aDe Tail ::= " ini " "=" AS a eId AT ansi ions | AT ansi ions
32 syn ax AT ansi ions ::= Lis {AT ansi ion ,""}
syn ax AT ansi ion ::= AS a eId "-" AE Id " ->" AS a eId
34 syn ax AS a eId ::= S ing
syn ax AE Id ::= S ing
36 syn ax Ini Seq ::= "INIT " S m
syn ax P ologEl ::= Au oma aDe | Ini Seq
38 syn ax P ologues ::= P ologEl | P ologEl P ologues
40 syn ax P og am ::= " PROLOGUE " P ologues "FILTER" S m
A GPFL p og am is composed o a p ologue, execu ed only once in o de o ini ialize he execu ion
en i onmen , and a il e s a emen , execu ed once o e e y incoming packe . A p ologue is composed
o au oma on kind de ini ions and ini ializa ion sequences. An au oma on kind de ini ion speci ies an
iden i ie K, an ini ial s a e o au oma a o kind Kand a se o ansi ions o au oma a o kind K. A
ansi ion de ini ion is composed o : wo au oma on s a es Fand T, and an au oma on e en ha igge s
he ansi ion om F o T.
A GPFL s a emen is composed o GPFL commands o s a emen s combined sequen ially. Some
s a emen s can be gua ded by an exp ession and execu ed only i ha exp ession e alua es o ue (cond).
Some s a emen s (i e ), associa ed wi h an exp ession e, a e exec ued imes, whe e is he alue o
ebe o e he i s i e a ion. Finally, newIn e up s a emen s egis e a s a emen o be execu ed in he
u u e, po en ially pe iodically.
GPFL commands a e he basic uni s ha ing an e ec on he execu ion en i onmen . The nop com-
mand has no e ec and se es mainly as a place holde . The accep , esp. d op, command s a es o
accep , esp. d op, he cu en packe and s op he il e ing p ocess o his packe . The send command
sends a packe on one o he po s. The ala m command gene a es a message on he ala m channel. The
se command se s he alue o a a iable. The newAu oma on command ini ializes an au oma on o he
p o ided kind, and assigns his newly c ea ed au oma on o he p o ided iden i ie . The s ep command
ies o igge an au oma on ansi ion by sending an e en e o an au oma on a. I he e is no ansi ion
om he cu en s a e o a igge ed by he e en e, hen he associa ed s a emen is execu ed.
Seman ics The ull o mal speci ica ion o GPFL’s seman ics can be ound in he companion echnical
epo [18]. GPFL’s seman ics ules a e de ined on he con igu a ion p esen ed g aphically in Fig. 5.
The p g cell con ains he GPFL p og am. A e ini ializa ion o he p og am, au oma on kind de ini ions
a e s o ed in he au oma onKindDe s cell and he il e cell con ains he il e (GPFL s a emen )
G. Le Gue nic, B. Combemale & J.A. Galindo 45
$PGM:K
p g
•
K
au oma aKind
•
K
ini ialS a e
•
Map
ansi ions
au oma aKindDe *
au oma aKindDe s
•
K
il e
•
Lis
nex In e up s
•
K
in Time
•
K
in Code
•
K
pe iod
in e up *
in e up s
•
K
k
0
clock
•
K
inHead
•
Lis
inTail
in
•
Lis
ala m
•
Lis
ou
s eams
•
K
ime
•
K
po
•
Map
ields
inpu
•
Map
kinds
•
Map
s a es
au oma a
•
Map
a s
en
Figu e 5: Kcon igu a ion o GPFL
ha is o be execu ed o e e y packe . The in e up s cell con ains a se o in e up de ini ions
(in e up *). An in e up is a iple composed o : he ime when he in e up is o be igge ed,
he code (s a emen ) o be execu ed, and a “Time” alue equal o he in e up ion pe iod o a pe iodic
in e up ion (o no hing o a non-pe iodic in e up ion). In addi ion, he in e up s cell con ains an
o de ed lis o he nex “ imes” when an in e up is o be execu ed. The clock cell egis e s he cu en
“ ime”. The con igu a ion also con ains a kcell ha holds he GPFL s a emen unde execu ion. Each
ime a new packe is inpu , he con en o he kcell is eplaced by he con en o he il e cell, and he
newly a i ed packe is s o ed in he inpu cell wi h i s a i al ime and po .
Packe s a e inpu om he s eams cell which con ains: he packe inpu s eam di ided in o he
nex packe o a i e (inHead) and he es o he s eam (inTail); he packe ou pu s eam; and he
ala m ou pu s eam. In he inpu s eam, esp. ou pu s eam, packe s a i ing, esp. lea ing, on bo h
46 Fo mal Speci ica ion o a Packe Fil e ing Language Using he K F amewo k
po s a e mixed oge he , bu con ains in o ma ion on he po o en y, esp. exi . Some choices made o
ep esen hose s eams a e no an in insic pa o GPFL’s o mal speci ica ion. The di ision o he inpu
s eam in o a head and a ail is such a choice. Those choices a e made in o de o be able o execu e he
speci ica ion. I is hen equi ed o implemen , in he K amewo k, a mechanism o e ie e and pa se
s ings desc ibing packe sequences sen o he il e . In o de o help dis inguish be ween he o mal
speci ica ion o GPFL and he mechanisms pu in place o execu e i , whene e possible, implemen a ion
choices, such as he o ma o s ings desc ibing packe s, a e de ined in ano he ile which is loaded in
he main speci ica ion ile wi h he equi e ins uc ion.
Finally, he en cell is he main dynamic pa o he execu ion en i onmen . I co esponds o a
“ eco d” o maps ha associa e: au oma on kind and cu en s a e o au oma on iden i ie s (au oma a
cell); and alues o a iables.
5 Tes ing GPFL’s Speci ica ion
GPFL’s speci ica ion, in oduced abo e and con ained in he companion echnical epo [18], is no
necessa ily pe ec . By a ma e o ac , impe ec ions o GPFL’s speci ica ion a e o in e es o he
expe imen a ion epo ed in his pape . Indeed, he goal o he expe imen a ion is o see how a ool such
as he K amewo k can help o spo and co ec impe ec ions in il e ing language speci ica ions. One
way o do so is by “ es ing” he new language speci ied, which is possible i he amewo k used o
speci y he language suppo s he execu ion o simula ion o language speci ica ions, which is he case
o he K amewo k.
The es scena io used assumes a ne wo k o clien s and se e s. The clien s eques esou ces o
se e s using a made-up p o ocol, called “DHCP che y”, summa ized in Fig. 6. The es scena io as-
Se e
Se e 1
Clien
Clien
Se e
Se e 2
Disc Disc
O (R1) O (R2)
Req(R1) Rej(R2)
locks R1 Ack
Ack
msc Nominal acqui e sequence
Se e
Se e 1
Clien
Clien
Rel(R1)
unlocks R1
Ack
msc Nominal elease sequence
Figu e 6: Nominal packe sequences o DHCP che y p o ocol
sumes ha se e s beha e poo ly when in e ac ing concu en ly wi h di e en clien s. The objec i e o
he es scena io is hen o il e communica ions in on o se e s in o de o p e en any concu en
clien -se e in e ac ions wi h any gi en se e . This es scena io is ob iously made-up o his expe -
imen a ion, which is a equi emen due o con iden iali y issues. Howe e , i is s ill co e ing he mos
equen ly used ea u es o il e ing languages simila o GPFL, while emaining simple enough o a
i s expe imen a ion.