View of Workshop on Modelling of Objects, Components, and Agents, Aarhus, Denmark, August 27-28, 2001

(1)

ISSN 0105-8517

Workshop on Modelling of Objects, Components, and Agents

Aarhus, Denmark, August 27-28, 2001

Daniel Moldt (Ed.)

DAIMI PB – 553 August 2001

DATALOGISK INSTITUT

AARHUS UNIVERSITET

(2)

(3)

This booklet contains the proceedings of the workshop Modelling of Objects, Com-

ponents, and Agents (MOCA'01), August 27-28, 2001. The workshop is organi-

zed by the

"

Coloured Petri Net\ Group at the University of Aarhus, Denmark and

the

"

Theoretical Foundations of Computer Science\ Group at the University of Ham-

burg, Germany. The papers are also available in electronic form via the web pages:

http://www.daimi.au.dk/CPnets/workshop01/

Objects,components,andagentsarefundamentalconceptsoftenfoundinthemodellingof

systems. Even thoughthey areused intensivelyinsoftware engineering,therelationsand

potentialof mutual enhancements between Petri-net modelling and the three paradigms

havenotbeennallycovered. Theintentionofthisworkshopistobringtogetherresearch

and application to have a lively mutual exchange of ideas, view points, knowledge, and

experience.

The submitted papers were evaluatedby a programme committee consisting of:

Wilvander Aalst (The Netherlands)

RemiBastide (France)

Jonathan Billington (Australia)

DidierBuchs (Switzerland)

HenrikBrbak Christensen (Denmark)

Jose-ManuelColom (Spain)

Jorg Desel (Germany)

Susanna Donatelli (Italy)

NisseHusberg (Finland)

EkkartKindler (Germany)

GabrielaKotsis (Austria)

FabriceKordon (France)

CharlesLakos (Australia)

RainerMackenthun (Germany)

DanielMoldt (Chair) (Germany)

KjeldHoyer Mortensen (Denmark)

DanSimpson (United Kingdom)

RudigerValk (Germany)

Tomas Vojnar (Czech Republic)

The programme committee has accepted 8 papers for presentation. They tackle the

concepts of objects, components, and agents from dierent perspectives. Formal as well

as application aspects demonstrate how wide the range can be within which Petri nets

canbeusedand illustrateatthe sametime thatthere isatendency touse more abstract

concepts for the analysis and design of Petri-net-based models.

DanielMoldt

(4)

!"$#%&' )(*

+-,/.021 35460278359:<;=0>?9A@B1C02D 9E.,21 FHG,21I5JK9LMNGPOQMN7=RS02753TU02VWMN3=0>?MW75RSX;=7?>?MWD 9ZY\[],^V`_

[KMW7=RbaA,2D J=VN9EcedSMN4 L1 9E>?9E_/9E[]97?>fIgOK4h>?9D 4jiiiiiiiiikiiiiiiiiiiiiiiiiiiiiiiiiiikiii l

mnEoqp rts\quv*t*g&xwS]sy

z 9{>t1 M|759E>t4U027=3}L,2D JK,27597?>t46~9{c<>t9753=MW75R)>t59)dU8]0^J=J=1 ,^02L=iiiiiiiiiikiiii l

m?\B!r&hB r"A{oq k

878J=J=VNMWL0>tMN,27,2G027Y\cKJ=1 94 4 M[]9 aA,2VN,2;=1C93 z 9E>t1CM9E>t4,!359VNMW7=R9E>?=,!35,2VW,^RO

>t, 0 Z;=4CMW7=94 4v>t, Z;=4CMW7=94 4Y7?[KMN1 ,27=D 97t>iiiiikiiiiiiiiiiiiiiiiiiiiiiiiiikiiiiii 2

so b#%E r

8R297?> _1CMW97t>?93,!3=9VWVNMN7=R$,2GdSMN4h>?1 MN=;g>?93IgOK4h>?9D 4.)M>t">?=9q!E9LE>aA,!,21C3=MN7=0_

>tMN,27}9{>q8J=J=1C,202Liiiiiiiiiiiiiiiiiikiiiiiiiiiiiiikiiiiiiiiiiiiiiiiiiiiiiiiii 2

m<^syUQsybqpEE S ZQ ¡

87Y|cKJB91CMWD 97?>.)M>taA,!,^1 3=MN7=0>?938VWR^9=1C02MWL z 9{>t1 Mx9E>t4024U@B,^1 D 02VNMW4CD¢G,21£,_

3=9VNMN7=R",2=MNVW98R^97?>t4}ikiiiiiiiiiiiiikiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiikiii 2

¤E ¡Btsw ¡Bsy bq *Hn sn *

+-,/.021 354¥0§¦7=MN¨=93©8J=J=1 ,^02L©G,21,3=9VWMN7=R§027=3ªTU91 MN¨=L0k>tMN,27©,2GS;=V>tM8R297?>

IgOK4h>?9D 4}iiiiiiiiiiiiiiiiiiiiiiiiiiiiikiiiiiiiiiiiiiiiiiiiiiiiiiikiiiiiiiiiiiii «2

¬ ^&#SQ®t&'&yE&%)r¯#S

,3=9VNMW75R"Ig>?0>t9{_dS9JK97=3=97?>H!E9L{>t4U;=4 MN7=RbaA,2VN,21 93

z

9{>t1CM|9E>?4jiiiiiiiiiikiiiii

lk°2

&hsEq(]E±¤ª²Qtk¡Bt ±q$m<E³´AP(P®B±¯ µ¶Q

8·aA02VNL;=VN;=4U,2G z 9E>t1CM|9{>qaA,^DbJB,27=97?>t4ªiiiiiiiiiiiiikiiiiiiiiiiiiiiiiiiiiiiiiii

l l

E *f(]¸g¬ *}#S eµot

Ig>t9J=4£+-,/.021 354@¹,21CDb0^V!TU91CMW¨=L0>tMN,27,2G-8R297?>C_=024C93Y\_Z;=4CMW7594 48J=J5VWMNL0>?MW,^7=4¯i

l 2

#%!Eeµg&º¸

8J=J5VWMNL0>?MW,^7,2G

z

9{>t1CM9E>?4UMN7,!359VNVWMN7=RbdSMW4»>t1 MN=;g>?93I=,2GP>¼.021 9)IgOK4h>?9D 4´iiiiiiki

lk½

(5)

Runtime Evolving Complex Discrete-event Systems

Nasreddine Aoumeur Gunter Saake

InstitutfurTechnischeInformationssysteme

Otto-von-Guericke-UniversitatMagdeburg

Postfach4120,D{39016Magdeburg

E-mail: faoumeur|Saakeg@iti.cs.uni-ma gdeb urg. de

Tel.: ++49-391-67-18659 Fax: ++49-391-67-12020

Abstract

Althoughformalspecication/validationisnowadaysdenitelyacceptedasanecessarystepin

developing reliable complexdiscrete-event systems,most ofexisting formalisms are facing chal-

lenging problems dueto the multi-dimensionalrequirements to be met by suchsystems. As a

resultofthisunsatisfactorystateofaair,dierentsystem'sfacetsareoftenseparatelyapproached

bydierentformalismswhichavoidany coherent descriptionof thewholesystem. Besides that,

most of formal proposals are lacking conceptual means for dynamically updating the (initial)

system's specication as unavoidable consequences of technological change, user's requirement

modication,etc.

Asacontributiontowardsasatisfactoryframework,wepresentinthispaperamulti-paradigm

formalism that we argue allows coping in a coherent way with most requirementsin complex

(discrete-event)systems. Thisformalism,referredtoasevolvingCo-nets,soundlyintegrates: (1)

Conceptsfromobject-orientationandmodularityprinciplesforcopingwiththecomplexstructure

and behaviour of such systems; (2)Timed high level Petri-nets for intrinsically mastering the

concurrent and timedependingnature ofsuchsystems;(3)A true-concurrencyrewriting logic-

based semanticsfor capturinginasimpleway runtimebehaviourmodicationinthisproposed

object-basedPetrinets,forderivingrapid-prototypesusingrewritingtechniques,andlastbutnot

leastfor controllingthe behaviour usingstrategies|possible duetothe reective natureofthis

logic. Allkeyfeaturesofthisframeworkareillustratedusinganon-trivialversionoftheEuropean

traincontrol systems(ETCS).

1 Introduction

Rigorousspecicationandvalidation,beforeanyeÆcientanduser-friendlyimplementation,represents

nowadaysmore than everthe mostcrucial phase inany complexsoftware development. Moreover,

suchaprecisedescriptionoffuturesoftwarefacetswithvalidationandvericationoftheirimportant

properties becomesunavoidable for software dedicated to criticalsystems, where any misconception

resultsindisastrousconsequences.

Unfortunately,despitetheexistingofseveralformalapproacheswearefarfromanywidelyaccepted

formalism which intrinsically copeswith all dimensionscharacterizing present-day criticalsystems.

Indeedwithmostofexistingapproaches,system'sfacetsareoftenseparatelyapproachedbydierent

formalismsavoidinganycoherentdescriptionandanalysisofthewholesystem.

Asacontributiontothisvividandcomplexareaofresearch,wepresentinthispaperanewproposal

that weargueallowsto copecoherentlywiththefollowingrequirementsincomplexcriticalsystems:

complexdata andknowledge, concurrentand and distributed behaviour,real-time constraints, and

theirevolutioninanon-previousway.

The model we are proposing is referred to as ECo-nets (an acronym for evolving concurrent

(6)

Object orientation with modularity: For coping with the rst dimension, we take prot of

allobject-orientedabstractionmechanisms(i.e. object,classication, dierentformsof inheritance,

object-compositionandobjectinteraction). Moreover,toallowanincrementaldescriptionforsuchsys-

tems,weregardeachclassratherasamodulewithanexplicitinterfaceincludingobservedattributes

and imported /exported messages. Thisnotion of moduleis naturallyextended to the notionof a

componentashierarchyofmodules usingdierentformsofinheritanceandobjectcomposition.

Timed high-level Petri nets: For adequately dealing with timing constraints with a full exhi-

bitionofintra-and inter-objectconcurrencywith dierentformsofcommunication,weintegrateall

mentioned object-oriented structuring mechanisms into an appropriate variant of timing algebraic

Petrinets. Thisintegrationhasbeenrstlyintroducedin[2].

Meta-reasoning on object Petri nets: Forcoping the dynamic evolution in complex discrete-

eventsystems,weproposeanaturalextensionofthisobjectPetrinetsvariant. Themainideasrstly

forwardedin[1] consistsin: (1) introducingmeta-placesthose tokensareacompletetransition'sbe-

haviour;associatethree(meta-)transitionsforupdating,deletingorcreatinganybehaviourastokens;

(3)relatethismeta-levelwiththeobjectlevelthroughappropriateread-arcs.

Rewriting logic-based semantics: Forrapid-prototyping purposes and for a clean true concur-

rency semantics,we interpretthe behaviour ofdierenttransitionsinrewritinglogic[12]. Also, for

capturingtheruntimebehaviourweproposeatwo-stepvaluatedinferenceruleinthislogic.Theother

crucialadvantagesofthislogicisitsintrinsicreectivenature[6]. Wetakeadvantagesofthisproperty

forcomposingdierenttransitionsbehaviourinaruntime way, leadingtodierentstrategieswhich

maymanifestsuchsystems.

Theproposedapproach,namelyECo-netsisincrementallyintroducedusinganontrivialversion

oftheEuropeantraincontrolsystems(shortlyETCS).Thiscasestudyhasbeenestablishedasoneof

twoapplicationsina(DFG)project 1

. Thiscomplexcasestudymanifestsallthementionedcrucialfea-

turesofcriticalsystems. Indeed,rst,itiscomposedofseveralsynchronouslyand/orasynchronously

communicatingcomponents including: trains, gates, sensors, control-lightand software controllers.

Secondly,eachcomponentincludescomplexmulti-layereddataandconcurrentbehaviour,andshows

onlypartofthemtoothercomponents. Thirdly,allcomponentsworkunder verypreciseandcritical

timingconstraints. Fourthly,the technologyused ineach componentis rapidlychangingtowards a

moreandmoresophisticatedones.

Therestof this paperis organizedasfollows. Inthesecond section weinformallyintroducethe

ETCScasestudywedealwithinthispaper. Thethirdsectionpresentshowdierentcomponentsare

formallyconceivedusingtheCo-nets approach. Inthenextsectionweconcentrateontheruntime

behaviourmodicationinCo-netsusingthisrunningapplication,leadingtotheintroductionECo-

nets. In thefth section, using the reective level of rewritinglogic,weshowhowstrategies over

rewrite rules gouverningECo-nets behaviour maybeexpressed. The last section summarizesthe

achievedwork,andoutlinesourfuturework. Wepointouthoweverthat duetospacelimitationour

presentationismostlyintuitive;correspondingrigorousdenitionsofallconceptsmaybefoundin[3].

1

"IntegrationofSoftwareSpecicationsforEngineeringApplications"supportedbytheGermanResearchCommu-

nity(DFG).

(7)

2.1 ETCS problem : technical presentation

Initstechnicalabstractversion[15]asageneralizationoftherailroadcrossingsystems[8],theETCS

problemcanbeexpressedasfollows. Arailroadcrossingwithseveraltraintracksandcommongates

canberepresentedasdepictedinFigure2.1. Sensorsalongeverytrackdetectoncominganddeparting

trains. Basedonsignalsfromthesesensors,anautomaticcontrollersignalsthegatetoopenorclose,

andalsomanageslight-controlinconsequence. Afterreceivingasignalformasensor,thetrainenters

inwhatiscalledtheregionofinterest(shortly,R );afterwardsdependingonthestateofthegatethe

trainhasto stoportocrosstheroad(I).

I egion R

,

nCrossing

Sensors Sensors

1

2

dw

up

Figure 1: Anabstractschemaofarailroadcrossing.

Thetechnicaltimingrequirementmaybeexpressedasfollows.

1 (resp. 2)representsthelower(resp. thehigher)timestamp forthe trainto reach theroad

after beingdetected byasensor (orto bedetected byasensor after leavingtheroad). These

twolimitsdependamongotheronthecurrentspeedofthetrain.

I R ;g(t)2[0;90];withg(t)=0correspondingtogatedown.

f

i

g of occupancy intervals : one or more trains are in I. ith occupancy is represented as

i

=[

i

;

i ].

i

isthetimeoftheithentryofatrainintothecrossingwhennoothertrainisin

thecrossing.

i

isthersttimesince

i

thatnotrainisinthecrossing.

Giventwoconstants

1

>0and

2

>0(with

dw +

1

<

1

<

dw +

2 and

dw +

1

<

2

<

up +

2

), the problem is to develop a system to operate the crossing gate that satises the

followingtwoproperties:

SafetyProperty: t2[

i

)g(t)=0(the gateisdownduringalloccupancyintervals.)

Liveness Property: t62[

i [

i

1

;

i +

2

])g(t)=90. (the gateisup whenno trainis in

thecrossing)

2.2 ETCS : an informal OO description

In this versionof ETCS we consider vecomponents|as classes with encapsulated behaviour and

explicitinterfaces. Fourcomponentsbelongtotheenvironment,namelyTraindescribingtrainstrav-

elingoncontrolledtracks,Gateasoperatingroad-crossinggates,Sensorsforautomaticallydetecting

(8)

ingOOnotationsadoptedfrom[16]andslightlyadaptedforemphasizingthedistinctionbetweenany

component'slocaland observedfeatures andtheinter-componentinteraction,wedepictedinFigure

2adiagrammaticOOdescriptionofthis ETCSsystem.

G2R R2G

Raise

The European Train Control System

Position : .. Track: .. StateG: ..

RepairG Lower DefcG

The Gate component

StateL : ..

EnterI

The Train Component

The Light component

DefcctS

StateS : ..

The Sensor component

Dt-in

Dt-out TrainlNo : ..

EnterR

Stop

Exit Position : ..

AddCar

ChgSp LmtSp

CarNb: ..

SchedTr : ..

StateT : ..

SeatNb : ..

The Control component

Spd: ..

SoonAr : ..

NoSoonAr : ..

onG : R onT : G

Addschd Remvschd Soon-Arv

NoSoon-Arv

Figure2: InformaldescriptionofdierentETCScomponents

Insomedetails,attributesandmethod-invocationsormessagesofeachcomponentareasfollows:

Train component: Besides the self-explained (local) attributes |TrainNo, SeatNb, CarNb|,

thereisthepositionposwhichisanobservedone. Thisattributemayhavethreevalues: E(lsewhere)

(\not in the section of interest"), R (\in the region of interest"), or I (\in the railroad crossing").

Also, the current speed is represented by Spd. Finally, by StateT we refer to the state of train

which maybe on (i.e. traveling) oro expressing that the trainis stopped due to gate failurefor

instance. Theoperationsacting onthis (train-)stateare thefollowing. EnterRallowsforchanging

theattribute positionfromE to R,and at thesame timeinforms theController componentof this

arrival. EnterI(resp. Exit) correspondsto theentry(resp. leavingof)intherailroad. Besidesthat,

wehaveincludedanoperationAddCarthatallowsforaddingnewcar(withacorrespondingnumber

ofsites) 2

. Also,whenthetrainreceived(fromothercomponents)astopmessageitsstatebecomeso.

Gate component: Thiscomponentismainlycharacterizedbythepositionofthegatethatmaybe

Up,Down(shortly,Dw),andbythestateofeachtrack(i.e. occupiedorfree,shortlyOc,fr). Thatis,

inthisversionweallowagatewithseveraltracks. TheassociatedmessagesonthisstateareLower,

RaisewhichhavetobesentbytheControllercomponent,andalsoasystematicappearanceofadefect

messageincase ofabreaking-downof the gate. Insuch casethis messageisrst communicatedto

thecontrollercomponentand then broadcasted to all trains,scheduled forthis gate, to be stopped

untilthegateisbeingrepaired;thuswehavealsoanothermessagedenotedrepair.

2

Thisoperationisirrelevantforthesystem,butitallowsustomakeexplicittheintra-objectconcurrencyexhibition.

(9)

(with corresponding crossing times and associated gate and track) allowed to cross the gate, an

(boolean) attribute SoonArrival indicating that atrain willsoon arrive(in lessthan Gamma units

of time), and another boolean attribute NoSoonArrival indicating that no train is scheduled for a

suÆcienttime(i.e. morethanGamma)inwhichcasethegateshouldbeUp. Twomessagesaretobe

consideredinthiscomponent. Firsttheschedulingof agiventrain(i.e. itsaddition tothe SchedTr

list). Each schedule is atuple composed of: trainidentity, corresponding gate, associated track in

such gate, and thetime to passthis gate. Secondthe removalof ascheduledtrain after passing a

correspondinggate. Afterpassingasensor,werequirethatthespeedofthetrainshouldbelessthan

someconstantSp

1

;whenasensorisdisplayingadefectstatesuchspeedshouldbelessthanSp

2 (with

Sp

2

<Sp

1 )

Sensorcomponent:Thiscomponentismainlycharacterizedbythestateofthesensorthatmaybe

Okordefect(shortly,Dfc). Theassociatedmessagesonthisstatearedetectanddefect;where detect

returnsthetimeandthecorrespondingtrain,whereasdefectindicatesthatthecorrespondingsensor

isnotworking.

Light-controlcomponent: Thiscomponentismainlycharacterizedbythestateofthelightsystem

(i.e. asforsensorOk,Dft),thecoloroflightindirectionofthegateaswellastheoneindirectionof

thetracks(shortly,onG, onT.Themethodsthatmayexhibitthiscomponentarethechangebetween

dierentcolors(i.e. Red-Yellow-Green).

3 Co-nets for components specication and validation

Thepurposeofthissectionistoreviewandapply,inanincrementalway, 3

tothisETCScasestudythe

mainCo-netsconceptsforderivingaformalcomponent-basedspecicationwhichcaninadditionbe

directlyvalidated. First,thenotionofcomponentsignatureispresentedandappliedtoderiveaformal

specication of dierent ETCS component signatures. Second, we highlight how the (concurrent)

behaviourof dierentcomponentsis thenderived. Third, wepresenthowrewrite rules gouverning

suchbehaviourareobtained. Fourth,thegeneralpatternforinteractingdierentcomponentsthrough

theirobservedpartissketchedandappliedtotheETCSproblem. Wenotehoweverthatduetospace

limitationinheritanceisnotaddressed,andonlysomecomponentsarethoroughlyspecied.

3.1 Co-nets component signature

Thecomponentsignaturedenesthestructureofobjectstatesandoperationstobeacceptedbysuch

states. TheOOsignaturethatweproposecanbeinformally[]describedasfollows:

Objectstatesare(algebraic)termsastuples oftheform: hIdjatr

1 :val

1

;::;atr k:val

k

;at bs

1 :

val 0

1

;::;atbs

k 0

:val 0

s

i; where Id is anobservedobjectidentity; atr

1

;::;atr

k

are localattribute

identiershavingascurrentvaluesrespectivelyval

1

;::;val

k

. Attributesobservedbyothercom-

ponentsareidentiedbyat bs

1

;:::;atbs

s

withval 0

1

;::;val 0

k

asrespectivecurrentvalues.

Thisobjectstateisallowedtobesplit(resp. recombined)ataneed. This'splitting/recombi-

nation'isregardedasanaxiom,whichmaytaketheform

hIdjattrs

1

;attrs

2

i=hIdjattrs

1

ihIdjattrs

2 i

with attr

i

asan abbreviationof atr

i1 :val

i1

;:::;atr

ik :val

ik

. Themultisetoperator willbe

explainedlater.

Messagesare just operationsbut withat least oneargumentofobjectstatesort, that is,they

shouldbesentorreceivedbyobjects. Wealsomakeacleardistinctionbetweenlocalmessages

and external ones, as imported or exported messages. Local messages trigger object states

changeinagivencomponent,whereasexternalones allowforinteractingdierentcomponents.

(10)

algebraiclanguagenotation-like.

3.1.1 Signaturesof dierentETCS components

For theETCS problemveCo-nets component signatureshave tobespecied. Butrst we have

tospecifythecommon(algebraic)datalevelfor dierentobjectvaluesand messageparameters. We

notethat justthetraincomponentsignatureisdescribedbelow;theothersignaturesaresketchedin

theappendix.

Inthedatalevelspeciedbelow,there areparticularlytheOId sortwhichstandsfor theobject

identitysort,theTimethatweassumeisspeciedelsewhere,andthedierentstatesofthegate(i.e.

GUpforgoingup,Up,etc). Finally,wehavealsothescheduledsetoftrainsasalistoftuplesoftuples

oftheform[OIdof train;[OIdof gate1;tracks number1;crossingtime1]j[OIdof gate2;tracks

number2;crossingtime12]j:::]:::. That is foreach trainwegrouptogether allroad-crossings(infor-

mation)itisgoingtopassthrough. Thisfacilitate,for instance,anyremovalaswellasrescheduling

duetogatefailure.

obj ETCSSturcture is

protecting OId Time Bool Nat Real .

sorts Gate PositionT PositionG .

subsorts OId-Gate OId-Train < OId .

subsort Track-Nb < Nat .

sorts SchedSet Elt Color.

subsorts T-roadElt < T-roadList.

subsort nil < SchedSet .

subsort Sched-Elt < SchedSet .

op : GUp, Up, GDw, Dw: ! PositionG .

op Gr, Red : ! Color .

op : Gamma : ! Time .

op : [,,]: OId-Gate Track-Nb Time ! T-roadElt .

op : | : T-roadElt T-roadList ! T-roadList . [assoc. comm.]

op : [,] : OId-Train T-roadList ! Sched-Elt .

op : . : SchedSet SchedSet

! SchedSet [assoc. comm.] .

op : in: Elt SchedSet ! Bool .

var S : SchedSet .

vars E, E' : Elt .

vars Now, t : Time .

eq E in nil = false .

eq E in E'.S =

if E == E' then true else E in S fi.

endo.

Train component signature: From theabove OO informaldescription of theETCS, the formal

traincomponentsignaturemaybedirectlyderivedasfollows.

obj Train is

protecting ETCSStructure .

subsort Id.Train < OId .

subsort LocalTrain ExternalTrain < Train .

subsort EnterI AddCar < Local TrainMes .

subsort EnterR Exit < ExportedTrainMes .

(* localattributes *)

op hjSpd: ;NbSeat: ;NbCar: i :

Id.Train Real NAT NAT ! LocalTrain.

(* observedattributes *)

op hjPos: ;StateT: i : Id.Train POSITION ! External Train .

(* localmessages *)

op AddCar: Id.Train Nat ! LocalTrain Mes .

op ChgSp: Id.Train Real !Local TrainMes . (*forspeedchange*)

(* Exportedmessages *)

(11)

op Exit: Id.Train OId ! ExportedTrain Mes

op EnterI: Id.Train ! ExportedTrain Mes .

op LmtSp: Id.Train Real ! ExportedTrain Mes (*forspeedlimitation*).

vars T : Id.Train .(*tobeusedinthenet*).

vars P, P1 : REAL.

endo.

3.2 Co-nets component specication

On the basisof a given componentsignature, wedene thenotion of componentspecicationas a

Co-netinthefollowingstraightforwardway.

Co-netsplacesarepreciselydenedbyassociatingwitheachmessagegeneratorone(message)

place, that is, such messages places contain associated message instances sent or received by

objectsbut notyet performed(i.e. by ringtheir correspondingtransitions). Also, witheach

objectsorta(object) placeisassociated,that is,anobjectplacecontainscurrentobjectstates

with respectivevalues. Wenote that places correspondingto externalmessageswillbe drawn

withboldcircles.

Co-netstransitionsreecttheeectofmessagesonobjectstatestowhichtheyareaddressed.

Conditions maybe associated to them restricting theirapplication. Moreover,wedistinguish

betweenlocalandexternaltransitions. Localtransitionsreectobjectstateschangeinagiven

component, whereas externalones capture theinteraction betweendierentcomponents. For

bothweproposeinnextsectionappropriategeneralpatterns.

Wedealwiththereal-timeconstraintsinourapproachbyattachingtimestampsortimeinternals

totransitionsandtotime-dependentmessages. Anappropriatesemantics,suchtime-dependent

transitionswillbeinterpretedintimedrewritinglogic[10].

3.2.1 ETCS component specication in Co-nets

AsfortheETCScomponentsignatures,wecommentherewithsomedetailsontheTraincomponent

whereastheothercomponentspecicationsaresketchedintheappendix.

The Train Co-net component: This netasdepictedinFigure 3is composed of anobjectplace

denoted by TRAIN containing current (object) states of dierent trains, three places corresponding

to dierentlocalmessages, and four places associated with observed messages(depicted inthe left

hand sidewithboldlines). Theeect ofeachmessageiscaptured byanappropriatetransition. For

instance,theeect ofthe messageEnterR(T)iscaptured by thetransitionENTER-Rwhich takesas

inputthepositionof thetrainwhich shouldbeE(lsewhere). After theringof thistransition,there

is a sending of EnterI(T) message and change of the position to R(in the region of interest) (i.e.

hTjPos: R i) 4

). It isalso worthwhilenoting that transitionslabeled byEnterI,Enter-R and Exit

aretime-dependenttransitionsasrequiredintheinformal(technical)description.

3.3 Co-nets Component semantics

After highlighting how Co-nets components are constructed, we focus herein on the behavioural

aspects, that is, how object states' components have to change in a coherent and true concurrent

way. Bycoherentwespecicallyunderstand therespect ofobjectuniquenessand theencapsulation

property. Forthis aim, we rstpropose ageneral pattern that has to be respected inconstructing

transitions in such components (i.e. local transitions). Second, a rewrite rule is derived for each

transitiononthebasisofthis generalintra-componenttransitionpattern.

4

Remarkthat dueto the splitting axiom only the position whichis the justconcerned attribute in this eect is

selected.

(12)

The Train Component as a Co-net

. . . . .

<T | Pos: R, StateT : off, Spd : 0>

Exit(T1)

<T1 | StateT : on, Pos : E, NbCar : N, Nbseat : Ns, Spd: s1>

Exit(I)

<T | Pos : R, StateT:on>

EnterI(T,t1)

AdCar(T, Ns)

EnterR(T1,.)

EnterI(T,t)

ChgSp(t1,s1) <T | StateT:on, Spd:S1>

ChgSp(T,S)

<T| StateT:on,Spd:S>

LmSp(T1,s1) Rest(T1)

LmSp(T, S)

<T | Pos : I>

AdCar(T.Nc)

<T | StateT: on, Pos : E>

<T | Spd : 0, NbCar: Nc, Nbseat: S>

TRAIN

<T | Pos: R, StateT : on, Spd : S>

<T | Pos : I, StateT : on>

<T | StateT:off, Spd:0>

<T | StateT:on, Spd:min>

<T | Pos : R, StateT : on>

Stop(T)

<T | Pos : E>

EnterI(T,t1)

EnterR(T,t)

Stop(T1)

ChgSp(T,S)

<T | Spd : 0, NbC : Nc+1, Nbseat : S + Ns>

True Restart

. . ..

RESTART

ENTERI

EXIT LMSP

True . . ..

. . ..

ENTER True

True

EnterR LmtSp

True

ADDC

. . ..

Exit

Stop . . ..

. . ..

CHGSP True

True

True CHGSP

. . ..

Stop

[

1

;

2 ]

Figure3: TheTrainComponentasaCo-net.

ThisgeneraltransitionpatternisdepictedinFigure4,anditcanbeintuitivelyexplainedasfollows:

The contact of just the relevant parts of some object states in a given component Cp, |namely

hI

1 jattrs

1 i

5

;..; hI

k jattrs

k

i| with some messages ms

i1

;::;ms

ip

declared in this component results

inthe followingeects: (1) the messagesms

i1

;::;ms

ip

disappear; (2) some(parts of) object states

participating in the communication change, namely hI

s

1 jattrs

s

1 i;:::;hI

s

t jattrs

s

t

i; (3) some objects

may be explicitly deletedby sending them delete messages; and (4) new messages maybe sent to

objectsofCp,namely ms 0

h1

;::;ms 0

hr .

Conditions on attributes values and messages parameters

. .

t obj

. . .

hId

i jatr

i

1 :v al

i

1

;:::i

k

i=1 hId

i jattrs

i i

s

t

i=s1 hId

i jattrs

0

i i

i

r

i=i1 hId

i jattrs

i i

Mes

i1

Mes

ip

Mes

h1

Mes

hr ms

i

1 ms

ip

ms

h

1

ms

hr

Figure4: Ageneralintra-componentor localtransitionpattern

Wenoteinthispatternthatmarkingsindierentplacesisasusualregardedasamultisetoftokens.

Such(marking)multisetisconstructedusingaunionoperatorwedenoteby.

3.3.1 Rewritetheoryfor Co-nets semantics

AswementionedinorderassigntoCo-netsbehaviouratrue-concurrencysemanticswithfullexhibi-

tionofintra-andinter-objectconcurrencyinsteadofaninterleavingorevenastep-basedsemanticslike

5

Withattrsi asasimpliednotationofatri1:vali1;::;atr

ik :val

ik .

(13)

inrewritelogic[12]. Themainideas(adaptedfromthealgebraicnetin[4])consistin: (1)associate

witheachmarkingmtitscorrespondingplacepasapair(p;mt);(2)tocapturethecurrentstateofa

Co-netsas multisetoverdierentpairs(p

i

;mt

i

)weintroduceanewmultisetgenerated byaunion

operator we denoteby , that is, aCo-nets stateis hencedescribed as(p

1

;mt

1 )(p

1

;mt

2 ):::;

(3)inordertoexhibitamaximalofconcurrencywerequirethedistributivityofover,thatis,if

mt

1

andmt

2

are twomarkingmultisetsthen we alwayshave: (p;mt

1

mt

2

)=(p;mt

1

)(p;mt

2 ).

Finally,intra-objectconcurrencyistobeensuredbythesplitting/recombiningaxiom.

Onthebasisof thesemoreorlessintuitiveideas,thegeneralrewriterulegouverningthegeneral

transitionpatterndepictedinFigure4takethefollowingform:

t: (obj;

k

i=1

hIdijattrsii) p

k =1 (Mes

ik

;ms

ik

))(obj;

t

k =1 hIds

k jattrs

0

s

k i

r

k =1 hIdi

k jattrsi

k i)

r

k =1 (Mesh

k

;msh

k

)ifCondition.

3.3.2 Applicationfor deriving Train transitionsrewrite rules

Byapplyingthisgeneralformofrule,itisnotdiÆculttogeneratetherulesgoverningETCScompo-

nents'behaviour. Forinstance,therewriterulesassociatedwiththetraincomponentareasfollows:

ADDC: (Train;hTjSpd:0;NbCar:Nc;Nbseat:Si)(AddC ;AddCar(T;Ns)

)(Train;hTjSpd:0;NbCar:Nc+1;Nbseat:S+Nsi)

ENTER: (Train;hTjPos:E;StateT:oni)

(EnterR ;EnterR (T;C)) [1;2]

) (Train;hTjPos:R ;StateT :oni)

(EnterI;EnterI(T))

ENTERI: (Train;hTjPos:R ;StateT :oni)(EnterI;EnterI(T))

)(Train;hTjPos:I;StateT:oni)(Exit;Exit(T;C))

EXIT: (Train;hTjPos:I;StateT :oni)(Exit;Exit(T;C))

)(Train;hTjPos:E;StateT :oni)(Exit;Exit(T;C))

STOP: (Train;hTjPos:R ;StateT:on;Spd:Si)(Stop;Stop(T))

)(Train;hTjPos:R ;StateT:off;Spd:0i)

LMSP: (LmtSp;LmtSp(T;S))(CHGSP;ChgSp(T;S)

CHGSP: (CHGSP;ChgSp(T;S)(Train;hTjStateT :on;Spd:S1i)

)(Train;hTjStateT :on;Spd:Si)

It isworthobservingthat a timestamp() and time-interval([

1

;

2

]) label thetwotime-dependent

transitions, namely ENTER and ENTER I. Such timed-rewrite rules are interpreted in Timed

rewritelogic[17]asastraightforwardextensionofrewritelogic[12]. Usingthefourinferencerulesof

thislogicandparticularlytheconcurrentreplacementones(withthestatesplitting/mergingaxiom

and the distributivity of over ) any reachable state can be computed in true concurrent way

startingfromaninitialmarkingfordierentplaces. Moreover,bysimultaneouslyaccompanyingsuch

computationwithgraphicalsimulationmostofmisconception,errorsandmissingcanbedetectedand

thencorrected.

3.4 Co-nets components interaction

Takingintoaccountthatobjectstatechangeineachcomponentisensuredbythealreadydescribed

intra-componentpattern,theinter-componentinteractionmaybemadeexplicitasfollows: Thecon-

tactofsomeexternalpartsofsomeobjectstates,namelyhI

1

jattrsob

1 i;:::;hI

k

jattrs ob

k

i,whichmay

belongtodierentcomponentsnamelyCp

1

;:::;Cp

m

withsomeexternalmessagesms

i1

;::;ms

ip results

inthefollowing:(1)themessagesms

i1

;::;ms

ip

disappear;(2)someexternalpartsofobjectstatespar-

ticipatinginthecommunicationchange;(3)newexternalmessages(thatmayinvolvedeletion/creation

ones)aresenttoobjectsindierentcomponents,namelyms 0

h1

;::;ms 0

hr

. Thisinter-componentinter-

actionorexternaltransitiongeneralpatternisdepictedinFigure5.

(14)

. . . . . . . .

. . Conditions on attributes values

and messages parameters

. .

t

hId

k jatrbs

k

1 :v al

k

1

;:::i

hId

l jatrbs

l

1 :v al

l

1

;:::i Bs(obj1)

Bs(obj

p )

Meso

i

1

Meso

i

p

Meso

h

1

Meso

h

r ms

i

1 ms

ip

ms

h

1 ms

h

r i

1

i 1

i

j hIdp

j

jattrsbsp

j i

i hId

1

i jattrs

0

bs

1

i i

j hId

p

j jattrs

0

bs

p

j i

Figure5: TheInter-componentinteractionpattern

3.4.1 Interacting dierent ETCS components

Toachievethe desired behaviour intheETCS problem, thevecomponentshave to interact, with

respect to this inter-component pattern, using their imported / exported messages and observed

attributes. This interactionis depicted inFigure 6. In this interaction,for instance,the transition

Dt-Itakesasinputs: (1)the detectionby sensorsofagiventrainT approachingagateGonatrack

K(i.easinputmessageDt-in(T,G,K,t));(2)andtheeectiveschedulingofsuchtrainatthistimet

(usingtheexportedmessage(Sn(T,G,K,t)). Theresultingoutputmessagesofthistransitionare: (1)

asendingtothetraincomponentofthemessageEnterR(T,G,K,now)(i.e. enteringintotheregionof

interest'R');(2)asendingofamessageforlimitingtrainspeedtoSp

1

;and(3)asendingofmessage

to thelightcomponentfor changingitslightcolorfromgreento red. Theremainingtransitionsare

alsoconstructedfollowingthesamereasonning.

Therewritingrulesgoverningthisinteractioncanbecapturedinasimilarway,asdonefortheinternal

behaviour,fromtheeectofeachtransition.

4 Runtime Evolution in Co-nets

The purpose of this subsection is, rst, to review the main ideas and corresponding constructions

for handlingruntimemodicationthat we rstproposedin[1]. Then, weproposea moreadequate

inferencerulefor propagatingagivenbehaviourfromthemeta-levelto theobjectlevel. Finally,we

showhowsuchmeta-levelallowsforanETCSevolvingspecication.

4.1 Meta-places and non-instantiated transitions constructions

For handlingruntime modicationof Co-nets componentspecications, theconstructions we pro-

posedin[1]maybesummarizedasfollows:

1. InordertofreesomeCo-netstransitions 6

fromtheirrigidity,weproposetoreplaceeachoftheir

three components| namely inputtokens inscribingtheir inputarcs, output tokens inscribing

their output arcs and their conditions| by appropriate variables those sorts are exactly the

sorts of associated input or output places. We refer to such transitions with only variables

as inscriptions as non-instantiated transitions. Their general form is sketched in the lower

righthand-side ofFigure 7. In this generalpattern for non-instantiated transitions,all(arc-)

inscriptions,namelyIC

obj

;IC

i1

;::;IC

ip

forinputarcs,CT

obj

;CT

h1

;::;CT

hr

foroutputarcsand

TC fortheconditionaretobeconsideredasappropriatevariables.

2. Second, for each becoming non-instantiated transition we gather its initial (i.e. before their

replacement by variables) condition and arc inscriptionswith their respective input /output

places into a a single tuple of the form: htransitionid: version j (input-)multiset,

6

Inthesamespiritasin [14 ],weassumethatsomebehaviour,i.e. transitions,is xedforeverreecting minimal

propertiesofthespeciedapplication.

(15)

Light

<L1 | Gate : G, aTgt : gr, aTtr: red, state : ok>

Dfct-Sc

Sensor

Exported Features of the Sensor Component

Controller

Remove

Exported Features of the Train Component

Soon

. . . . Dtc(k1, T1, t1)

. . . .

Train

. . . . . . . .

. . . . Sn(t1,g1,k1,t1) . . . .

Lower-G

LwG(g1, k1)

LW

. . . .

Dt-in

Dt-out

Rmv(Trk,G,T, t1)

Sn(T, G, Trk, t)

<Tr1 | StateT: ok>

LmSp(T,sp2)

. . . .

Exported Features of the Controller Component

. . . . . . . .

Gate

True

True True Tf

Tr . . . .

RepG

RepG(g1)

DefG

DefG(g1)

. . . .

Rmv(t1,g1,k1,t1)

RestL StopL

RestL(T1.T2..)

RepG(G) DefG(G)

StopL(T.Lt)

StopL(Lt)

RestL(T.Lt)

StpT(T) ResT(T)

RestL(Lt)

. . . .

StpT StpT(T1) ResT(T1) . . . . ResT

G2R(l1,g1) . . . .

G2R

Exported Features of the Light Component R2G

R2G(li,gi) . . . .

R2G(G)

G2R(G)

Td-out(k1)

<S1 | StatS: ok> . . . . (Now - t) < True

DfS(s1,g1)

Enter-R(T, G, K, now) Enter-R(T, G, K, now)

Ex(T1,K1,..) . . . .

Exit Limit-Sp

Enter-R(T, G, K, now)

LmSp(T1,Sp1) EntR(T1,K1,.)

LmSp(T,sp1)

Dt-out(T,G,K, t) Dt-in(T,G,K, t)

True

Exit(T,Tk, G, Tm)

Lower(G, K, now) Enter-R(T, K, G, t)

True <G1 | StatG:ok>

. . . .

Exported Features of the Gate Component

True

< G | StatG : Ok>

Exit(T,K, G, Tm)

Raise-G

Rep-G(g1) . . . .

Rep-G Dfc-G(g1) . . . . Dfc-G

Dfc-G(G) RaisG(G, K, now)

RAIS Rep-G(G)

. . . .

RaisG(gj, kj)

StopL(T1.T2..t)

. . . .

DT-O

DTF

Sn(T, G, K, t)

DfS(S,G)

<C1 | Gate:G1, Schd:[t1, k1, tm1]...].., StateC : ok>

Enter-R

DT-I

<T | StateT: Ok>

Figure6: TheTrain-Gate-Controller-Sensor-LightInteractingusing observedfeatures

(output-)multiset, condition i. In this tuple transition id refers to the label of the

transition,whereasversionisjustanaturalnumberindicatingthatthistuplecanberegarded

as a particularversionof a behaviour associated with this transition; this willbe moreclear

in thefollowing. In particular,theprecise formof such a tuple withrespectto the transition

(general-pattern)T inFigure4takesthefollowingform;wheretheindexirepresentsaparticular

versionofsuchtransition.

hT :ij(obj;IC

obj )

i

p

k =i

1 (Mes

k

;IC

k

);(obj;CT

obj )

h

q

k =h

1 (Mes

k

;CT

k

);Conditioni

3. Third, weconsider such `behaviour' tuples astokens w.r.t. a new place, namely meta-place

inFigure 7. Thisplace constitutes therst elementofthe proposed meta-level. On thebasis

of this behaviourastokens,it becomesquitepossibleto delete someof them, modifysomeof

them or introduce new ones: This correspondsrespectively to thetransitionsDEL, MODIFand

(16)

transition 7

.

4. Finally,usinganappropriateread-arcwerelatethetwolevels,i.e. themeta-placeinthemeta-

levelwitheachnon-instantiatedtransitionintheobjectlevel.

. . . . Chg-Bh(T,..)

General Pattern of Run-time Modified Internal Transitions

. . . . . . . .

Add-Bh(T,..) . . . . Del-Bh(T,..)

. . . .

The Meta-object Level Gouverning the Modified Behaviour

obj

General Pattern of rigid Internal Transitions True

Meta-Place

. .

Add-Bh

. .

T True DEL

T(i)

TC

True

True Del-Bh

ADD2 ADD1

MODIF

. .

Chg-Bh

Conditions on attribute values and message parameters

hId

i jatr

i

1 :v al

i

1

;:::i k

i=1

hIdijattrsii

st

i=s

1 hId

i jattrs

0

i i

ir

i=i

1 hId

i jattrs

i i

Mes

i

1 Mes

i

1

Mes

i

p Mes

i

p

Mes

h

1 Mes

h

1

Mes

hr Mes

hr ms

i

1 ms

i

p

ms

h

1

ms

hr

IC

i

1 IC

ip

CT

h

1

CT

hr IC

obj

CT

obj AddBh(T;

i (P

i

;IC

i );

j (Q

j

;CT

j );TC) hT

k :n

1 j(obj;

s hId

1 jattr s

is i)

r (Mes

ir

;mes

ir );(obj;

h hId

0

1 jattr s

0

i

h i)

l (Mes

h

l

;mes

h

l ); TC1i

hT:k jIC;CT;TCi

hT:k+1j

i (P

i

;IC

i );

j (Q

j

;CT

j );TC

j )i hT:1j

i (P

i

;IC

i );

j (Q

j

;CT

j );TC

j )i D elBh(T;i)

hT:ij; ; i

ChgBh(T;i;

j (P

0

j

;IC 0

j );

h (Q

0

h

;CT 0

h );TC

0

)

hT:ij

i (P

i

;IC

i );

r

(Qr;CTr);TCi

hT:ij

j (P

0

j

;IC 0

j );

h (Q

0

h

;CT 0

h );TC

0

i

hT:ij(obj;IC

obj )

ip

i=i

1 (Mes

i

;IC

i );(obj;CT

obj )

h

r

j=h

1 (Mes

j

;CT

j );TCi

Figure 7: ThegeneralpatternforhandlingdynamicbehaviourinCo-nets

Remark: Todealwithruntimebehaviourmodicationalsofortime-dependenttransitionitsuÆces

just to addanother componentto thetuple constructionintheaboveconceptualization. Morepre-

cisely,under theassumptionthat thetransitionT (general-pattern)inFigure 7takestmas unitof

timesortimeintervalthen, thecorrespondingbehaviourastupleis:

ht:ij(obj;IC

obj )

i

p

k =i1 (Mes

k

;IC

k

);(obj;CT

obj )

j

q

k =j1 (Mes

k

;CT

k

);Condition;Tmi

.

4.1.1 Semantical part: the meta-inferencerule

For theoretical underpinningof these constructions, we propose with respect to the sameCo-nets

rewritelogicsemantic-basedanadequateinferencerulethatcanberegardedasamoreexibleformu-

lationoftheoneproposedin[1]. Themainideasunder thisreformulationas describedbelowarethe

following. Foreachnon-instantiatedtransitionwegeneratearewriteruleinthesamewayaswedone

forusualCo-netstransitionsexceptthatweintroduceanewbinaryoperatordenotedk

r

separating

theread-arcinscriptionfromotherpairsofplace-tokens. Thisoperatorisnecessarybecauseweshould

expressthefactthattokensselectedusingaread-arcarenotfromtheobjectlevel(i.e. theCo-nets

7

Theoperator

capturethe notionofinhibitorarc,inthe sensethattheinscriptionshouldnotbeinthecurrent

marking.

(17)

inFigure 7thisrulelabeledbyt nins

isderivedasfollows.

t nins

:(Pmeta;ht:ij(obj;ICobj) i

p

i=i

1

(Mesi;ICi);(obj;CTobj) j

q

j=j

1

(Mesj;CTj);TCikr(obj;ICobj) i

p

i=i

1

(Mesi;ICi)

)(obj;CTobj) j

q

j=j

1

(Mesj;CTj) if TC

However,due to theitsinferencebetweenthetwo-level(i.e. themeta-levelthroughtheread-arc

and theobjectlevel), this rewrite rulecannot bedirectlyapplied, and wetherefore haveto gener-

ate fromit ausual rewrite rule or an instantiated rule we denote by t ins

(i). This process consists

in selectingthrough dierentsubstitutions (

i

) a particularbehaviourfrom the meta-place, and it

canbecapturedthroughthefollowinginferencerulewhereM(P

. . . .

ChgSp(T,S)

<T | Pos: R, StateT : off, Spd : 0>

The Meta-object Level Gouverning the Modified Behaviour of the Train Component

AdCar(T,N)

Exit(I)

<T | Pos : R, StateT:on>

AdCar(T, Ns)

EnterR(T1,.)

LmSp(T, S)

<T | Pos : I>

ChgSp(t1,s1)

<T | Spd : 0, NbCar: Nc, Nbseat: S>

TRAIN

<T | Pos: R, StateT : on, Spd : S>

EnterI(T,t)

<T | StateT:off, Spd:0>

<T | StateT:on, Spd:min>

<T | Pos : I, StateT : on>

The Train Component as a Co-net

EnterI(T,t) . . . . .

Stop(T1) Exit(T1)

<T | Spd : 0, NbC : Nc+1, Nbseat : S + Ns>

Stop(T) LmSp(T1,s1)

Rest(T1)

<T | Pos : E>

<T1 | StateT : on, Pos : E, NbCar : N, Nbseat : Ns, Spd: s1>

True

CHGSP

ENTERI ENTER

Meta-Place

RESTART

. . ..

EXIT Restart

LmtSp

. . ..

EnterR Exit

. . ..

beta True . . ..

ADDC

CHGSP True

LMSP

Stop

. . ..

True

Stop

ICe

1

ICe

2

TCe

CT

e

1

CTe

2 Tm

ICc

1

IC

c

2

TCc

CT

c

hENTER:1j(EnterR;EnterR(T;t;))(TRAIN;hTjStateT:on;Pos:Ei);

(EnterI;EnterI(t1))(TRAIN;hTjStateT:on;Pos:Ri);True;[1;2]i

hCHGSP:1j(CHGSP;ChgSp(T;S))(TRAIN;hTjStateT:on;Spd:S1i);(TRAIN;hTjStateT:on;Spd:Si);Truei

hENTER:2j(EnterR;EnterR(T;t))(TRAIN;hTjStateT:on;Pos:E;Spd:Si);

(EnterI;EnterI(t1))(TRAIN;hTjStateT:on;Pos:R;Spd:S 20i);S<40;[(S 20)Cs1;SCs1]i

hCHGSP:2j(CHGSP;ChgSp(T;S))(TRAIN;hTjStateT:on;Spd:S1;Pos:Pi);

(TRAIN;hTjStateT:on;Spd:Si);((P=E)^(S<160))_(P6=E)^(S<40))i

hENTER:ij(EnterR;IC

e

1

)(TRAIN;IC

e

2

);(EnterI;CT

e

1

)(TRAIN;CT

e

2 );TC

e

;T

m i

hCHGSP:ij(CHGSP;ICc

1

)(TRAIN;ICc

2

);(TRAIN;CTc;TCci

Figure8: A runtinemodiableCo-netstraincomponent

(19)

Besidesitstrueconcurrencynatureanditsoperationalityallowinggenerationofrapid-prototypes,the

keyfeatureofrewritinglogicisalsoitsintrinsicreectioncapabilities. For ourCo-netsframework,

thecrucialadvantageofthis\second"meta-levelisthepossibilityofintroducingappropriatestrategies

for controlling the way in which dierent transitions should be red. This is of great benet for

reectingacurrentfunctioningofagivensystem,withoutresortingtoxforeveraparticularwayof

functioning. Moreover,thisallowstofreeasmuchaspossiblethenetfromsuchcontrolwhichledtoa

verysimpleand exiblenetspecication. Inthefollowing,wegivemoredetailaboutthislevel,then

weshowhowtoapply ittotheETCScasestudy.

5.1 Strategies using reection in rewrite logic

Rewritinglogicisreective[11],thatis,thereisanitelypresentedrewritetheoryU thatisuniversal

inthesense thatwecanrepresentinU anynitelypresentedrewritetheoryR(includingU itself)as

atermR ,anytermst,t 0

inRastermst,t 0

,andanypair(R;t)asaterm(R ;t),insuchawaythat

wehavethefollowingequivalence

(y)R`t !t 0

()U`hR;ti !hR;t 0

i

Forasystemofrewriterulesgouverningtransitionsbehaviourasinourcase,itisnowquitepossibleto

representitas(apairof)datatypes,andtherewritingofanyCo-netsstaterepresentingthecurrent

marking can be now completely controlled. In this sense, an expressive language for composing

dierentrewriteruleshasbeendevelopedfortheMaudelanguage[13,5];that weadopt here.

Firstakernelisdenedstatinghowrewritingintheobjectlevelisaccomplishedatthemeta-level.

Inparticular,Maudesupportsastrategylanguagekernelwhichdenestheoperation:

op meta-apply : Term Label Nat >Term.

Atermmeta-apply(t,l,n)isevaluatedbyconvertingthemeta-termttothetermitrepresents 8

and

matchingtheresultingtermagainstallruleswiththegivenlabell. Therstnsuccessfulmatchesare

discarded,and ifthere isan(n+1)th successfulmatch itsruleis applied,and theresultingtermis

convertedtoameta-termandreturned;otherwise,errorisreturned.

ThestrategylanguageSTRATdenedin[5]extendsthekernelwithoperationstocomposestrate-

gies,and also with operationsto create and manipulatea solutiontree obtainedbythe application

of a strategy. It denes sorts Strategy and StrategyExp for strategies, and sorts SolTree and

SolTreeExpforthesolutiontree. Themainoperationsdenedonstrategiesare:

operationsdeningbasicstrategies:

opidle: >Strategy. //*idleisanemptystrategy *//

opapply: Label >Strategy//applicationofagivenrule //.

oprew =>with : TermSolTreeExpStrategy >StrategyExp.

failure: >StrategyExp.

operationsdeningsolutiontrees:

op? : >SolTreeExp.

opapply: Label >Strategy.

oprew =>with : TermSolTreeExpStrategy >StrategyExp.

failure: >StrategyExp.

operationsthat composestrategies:

op ; : Strategy Strategy >Strategy//applicationoftwostrategies insequence //.

(20)

op iterate: Strategy > Strategy // repetitive applicationof a given strategy untilit isno-more

applied//.

Foramoredetailaboutthesemanticsofthese operations,thereadermayparticularlyconsult[5].

5.2 Application to the ETCS system

As wepointed outthe meta-levelwe propose for dynamicallyevolving Co-nets specicationis in

itselfnotsuÆcientforexpressingparticularlyhowdierentsystemtransitionsareperformed. Indeed,

rst recallingthat usuallyinPetri netsa transitionmaybered as soonas itbecome rable, and

thereisnowayforcontrollingtheorderinwhichtransitionshavetobered. ThesediÆcultiesinduce

that the designer of the systemshould decided whether (s)he let irrelevant such order oropt for a

defaultorderandintegrateitdirectlyinthemodel|leadinginmostofreal-casetoverycomplexPetri

netwhich worksonlyforthisdefaultstrategy.

ObviouslyinspecifyingtheETCSproblemwehavedecidedfortherstsolution,thatis,nocontrol

atallof dierentsystemelementarybehaviourortransitions. Infact,wedidnotstate,forinstance,

whenshouldthespeedbeeectivelylimitedinthetraincomponent,orwhenshouldthetrainenterthe

regionofinterest,etc. Butimaginethatwehavedecidedforaparticularxedstrategy;forinstance,

rstlimitthespeedthenenterintotheregionofinterest,enterthecrossingroadandthenexitit;and

onlythen performchangeof car numbers,orrestartstopped trains,etc. It isveryhard toimagine

how complexand articialwould be theresulting netfor such adefault strategy. Forinstance,for

ringthetransitionENTERwehavetobesurethatthetransitionsLMSPandCHGSPhavealreadybeen

redinthisorder. ThismeansthatwehavetoaddanarticialoutputplacetotheCHGSPtransition

forindicatingitsring,andrelatethisplacethroughanarticialtransitionto theEnterRasoutput

place.

Fortunatelyduetotothisrewritelogicmeta-reection,theETCSspecicationofdierentcompo-

nentsas wellasinteractionremainsunchangedwhilewecanformulateanystrategywewouldliketo

have. Forinstance,takinginto accountaslabelthenameofdierenttransitions,theabove'default'

strategywewouldliketohavemaybesimplyexpressedbythefollowing:

iterate(LMSP;CHGSP;ENTER ;ENTER I;EXIT)

)

The meta-levelof rewritinglogicwould respects this strategy. Moreover, we canassociate complex

conditionsonapplyingsuchstrategies.

6 Conclusions

Wepresentedinthispaperageneral-purposeframework,referredto asCo-nets,particularlysuited

forspecifying/ validatingcomplexdistributedobject-basedcriticaldiscrete-eventsystems,but also

fordynamicallymanipulatingtheirbehaviour. Methodologicallythisframeworkmayberegardedas

three layer-basedone. The rstlayeris asoundintegrationobjectorientedabstractionmechanisms

with modularityconstructsinto anappropriate varietyof algebraic Petri nets. The second layeris

meta-level one, and it allows for dynamically creating, modifying and/or deleting any elementary

behaviourwhilethesystemremainstillrunning. Thethirdlayertakesprotofthereectioncapabili-

tiesofrewritelogic|assemanticsforCo-netsbehaviour|fordynamicallydescribingasappropriate

strategiesreectingthereal-functioningofthecomplex.

Wehaveillustratedthisframeworkusinganon-trivialspecicationofavariantofEuropeantrain

controlsystem(ETCS).Thiscasestudy demonstratesinparticularthesuitabilityofthisframework

fordealingcomplexreal-worlddistributedsystemsinaveryexible.However,afterachievingthisrst

stepwe areconsciousthat muchmoreworkremainsahead. Particularly,weare planningtoextend

this case study variant to morecomplex one. Also, we are focusing on theintegrationof temporal

aspectsforverifying,andnotonlyvalidatingsystemproperties.

(21)

[1] N.Aoumeur. SpecifyingDistributedandDynamicallyEvolvingInformationSystemsUsinganExtended

Co-NetsApproach. InG.Saake,K.Schwarz, andC Turker, editors, Transactions andDatabase Dy-

namics,volume1773ofLectureNotesinComputerScience,Berlin,pages91{111.Springer-Verlag,2000.

Selectedpapersfromthe 8thInternationalWorkshoponFoundations ofModelsandLanguagesforData

andObjects,Sep. 1999,Germany.

[2] N.AoumeurandG.Saake.TowardsanObjectPetriNetsModelforSpecifyingandValidatingDistributed

Information Systems. InM. Jarke andA. Oberweis, editors, Proc.of the 11thInt. Conf.on Advanced

InformationSystemsEngineering,CAiSE'99,volume1626ofLecture Notesin ComputerScience,pages

381{395.Springer-Verlag,1999.

[3] N.AoumeurandG.Saake.Co-nets: AFormalOOFrameworkforSpecifyingandValidatingDistributed

InformationSystems. PreprintNr.2,FakultatfurInformatik,UniversitatMagdeburg,2000.

[4] M. Bettaz, M. Maouche, M. Soualmi, and S. Boukebeche. Protocol Specication using ECATNets.

ReseauxetInformatique Repartie,3(1):7{35, 1993.

[5] M. Clavel, F. Duran, S. Eker, J. Meseguer, and M. Stehr. Maude : Specication and Program-

ming in Rewriting Logic. Technical report, SRI, Computer Science Laboratory, March 1999. URL :

http://maude.csl.sri.com.

[6] M.ClavelandJ.Meseguer. ReectionandStrategiesinrewritinglogic. InG.Kiczales,editor,Proc.of

Reection'96,pages263{288.XeroxPARC,1996.

[7] Goguen,J.etal. IntroducingOBJ. TechnicalReportSRI-CSL-92-03,ComputerScienceLaboratory,SRI

International,1992.

[8] C.L.HeitmeyerandN.Lynch.TheGeneralizedRailroadCrossing: ACasestudyinFormalVerication

ofreal-timeSystems. InProc.oftheIEEReal-TimeSystemsSymposium,1994.

[9] K.Jensen.ColouredPetriNets: BasicConcepts,AnalysisMethodsandpracticalUse-Volume1: Basic

Concepts. EATCSMonographsinComputerScience,26, 1992.

[10] P.KosiuczenkoandWirsing. TimedRewritingLogicwithanApplicationtoObject-BasedSpecication.

Scienceof ComputerProgramming,28:225{246,1997.

[11] N.Marti-OlietandJ.Meseguer.Rewritinglogicasalogicalandsemanticframework.InJ.Meseguer,edi-

tor,Proc.ofFirstInternationalWorkshoponRewritingLogic,volume4ofElectronicNotesinTheoretical

ComputerScience,pages189{224,1996.

[12] J. Meseguer. Conditional rewriting logic as a unied model for concurrency. Theoretical Computer

Science,96:73{155,1992.

[13] J. Meseguer. Solving the Inheritance Anomaly in Concurrent Object-Oriented Programming. In

ECOOP'93 - Object-Oriented Programming, volume 707 of Lecture Notes in Computer Science, pages

220{246.SpringerVerlag,1993.

[14] ConradS,J.Ramos,G.Saake,andC.Sernadas. EvolvingLogicalSpecicationinInformationSystems.

InJ.Chomickiand G.Saake, editors, Logics for Databases andInformation Systems, chapter 7,pages

167{198.KluwerAcademicPublishers,Boston,1998.

[15] E.Schneider. Referenzfallstudie Verkehrsleittechnik. Informatik-bericht,TechnischeUniversitatBraun-

schweig,2000. URL:http://www.ifra.ing.tu-bs.de/m33/spezi(InGerman).

[16] P.Wegner. ConceptsandparadigmsofObject-OrientedProgramming. OOPSMessenger,1:7{87,1990.

[17] M.WirsingandA.Knapp.AFormalApproachtoObject-OrientedSoftwareEngineering.InJ.Meseguer,

editor,Proc.oftheFirstInter.WorkshoponRewritingLogic,volume4.ElectronicNotesinTheoretical

ComputerScience,1996.

Gatecomponent signature:

obj Gate is

protecting Object-stateGRCStructure .

subsort Id.Gate < OId .

(22)

op hjPosition: i :

Id.Gate POSITION-G ! External Gate .

op Lower: OId Id.Gate ! LOWER .

op Raise: OId Id.Gate ! RAISE .

op Defect: OId Id.Gate ! DEFECT .

op Repair: OId Id.Gate ! REPAIR .

endo.

<G | Pos : Dw, Trk : T.[Tk,fr], SateG : ok>

<G | SateG : off>

Rep(G)

<G | SateG : ok>

Raise(G,r1)

GATE

Rep(G1) Dfct(G) Lw(G1,..)

<G | SateG : ok>

Lower(G,Tk)

<G | Pos : Up, Trk : T.[Tk,fr], SateG : ok>

<G | Pos : Dw, Trk: T1.[Tk,oc].T2, SateG : ok>

<G | Pos : St, Trk:T1.[Tk,fr].T2, SateG : ok>

<G | Pos : Dw, Trk : T.[Tk,oc], SateG : ok>

The Gate Component as a Co-net

< G1 | SatetG : ok, Trk : [Tk1, oc].[Tk2, fr].., Pos : Up>

Raise(G, Tk)

Dfct(G)

True True

SOON

REPAIR DEFECTG Else

. . ..

St = Up or St = Dw Lower

Raise

DFCG

. . ..

all-free-in(T)

LOWER

Repair . . ..

. . ..

Figure9: TheGateComponentasaCo-net.

Controllercomponentsignature:

obj Controller is

subsort Id.Controller < OId .

subsort LocalController External Controller

< Controller .

subsort REMVSCHD ADDSCHD < Local ControlMes .

subsort RESCHED SOON-ARV < ObsControlMes .

op hjSoonAr: ;NoSoonAr: i :

Id.Controller bool bool ! Local Controller .

(* observedattributes *)

op hjSchedTr: i :

Id.Controller SCHED-TR ! ExternalController .

(* localmessages *)

op Remschd : Id.Controller Id.Train Id.Gate ! REMSCHD .

op Addschd : Id.Controller Id.Train Id.Gate Time ! ADDSCHD .

op SonArv: Id.Controller OId ! SOON-ARV .

endo.

The Lightcontrolcomponent signature:

obj Light is

subsort Id.Light < OId .

subsort LocalLight ExternalLight

< Controller .

subsort G2R R2G DFCTL < ObsLight Mes .

op hjatGate: ;StateL: i :

Id.Light Id.Gate StateL ! LocalLight .