文档库 最新最全的文档下载
当前位置:文档库 › Counting Interface Automata and their Application in Static Analysis of Actor Models

Counting Interface Automata and their Application in Static Analysis of Actor Models

Counting Interface Automata and their Application in Static Analysis

of Actor Models

Ernesto Wandeler?J¨o rn W.Janneck?Edward A.Lee?Lothar Thiele?

Abstract

We present an interface theory based approach to static analysis of actor models.We?rst introduce a new interface theory,which is based on Interface Automata, and which is capable of counting with https://www.wendangku.net/doc/368593013.html,ing this new interface theory,we can capture temporal and quan-titative aspects of an actor interface as well as an ac-tor’s token exchange rate.We will show,how to extract this information from actors written in the Cal Actor Language(C al),and we also present a method to cap-ture the interface information as well as the structure of data?ow models into an interface automaton.This au-tomaton acts as glue between the automata of all actors in the model,and by successfully composing all actor au-tomata with it,we can prove interface compatibility of all actors with the composition framework.After successful composition,the resulting automaton will contain infor-mation that can be used for further static analysis of the composite actor model.

1.Introduction

Component based design is an approach to software and system engineering in which new software designs are created by combining pre-existing software compo-nents.The ability to check the compatibility of such components,and to detect errors in the composite sys-tem of components is thereby an important factor for software development productivity and software qual-ity.

Many modern programming languages which make extensive use of component libraries,such as Java or C#,provide a component interface compatibility checking on a data type level.By checking whether the 1Computer Engineering and Networks Laboratory,Swiss Fed-eral Institute of Technology(ETH)Z¨u rich

2Department of Electrical Engineering and Computer Sciences, University of California at Berkeley data types of arguments in a method call to a compo-nent are compatible with the speci?ed interface they ensure a certain level of component compatibility.

Interface theories for component based design[6] take this interface compatibility checking one step fur-ther by providing formalisms to specify component in-terfaces in more detail.One recent approach in this area is Interface Automata[5],which is an interface theory de?ning a light-weight formalism that can cap-ture the temporal aspects of software component inter-faces.In particular,Interface Automata can capture as-sumptions on the order in which the methods of a com-ponent may be called,as well as guarantees on the or-der in which a component itself calls external meth-ods.

In the Ptolemy II project[12,2],which studies ac-tor based modeling,simulation and design of concur-rent,real-time,embedded systems,e?orts were made recently to use Interface Automata to capture the tem-poral aspects of an actor’s interface towards its compo-sition framework,into what was called the behavioral type of an actor[15].Using this behavioral type,type checking can be done towards the behavioral type of an actor composition framework,to ensure compatibil-ity on a behavioral type level between an actor and its composition framework.

Contributions In this paper,we present a new interface theory that is tailored towards the use in actor systems and that allows us to capture more aspects of an ac-tor’s interface into its behavioral type than we could with original Interface Automata.We call this inter-face theory Counting Interface Automata(CIA).

We present a method to extract the interface infor-mation of an actor written in the Cal Actor Language (C al)[8,1]into a CIA,and we also present how to cre-ate a CIA of a composition framework with a data?ow model of computation.

With the successful composition of this framework automaton and all actor automata,we can prove be-havioral type compatibility of all actors with the com-position framework.

in Proceedings of the 3rd International Conference on Software Engineering and Formal Methods - SEFM 2005

Koblenz, Germany, September 5-9, 2005

The successful composition leads to a new CIA, which contains the complete token exchange informa-tion of the composite actor model and which can be used for further static analysis of the composite actor model.We will show,how the token exchange informa-tion contained in this automaton can be extracted. 2.An Introduction to Actor Based

Modeling

Actor based modeling is an approach to systems de-sign in which entities called actors[10,3]communi-cate with each other through ports and communica-tion channels.From the point of view of component based design,actors are the components in actor ori-ented modeling.

In the context of this work,an actor is a computa-tional entity with a well de?ned component interface.It has input ports,output ports,state and parameters.An actor communicates with other actors by sending and receiving atomic pieces of data,called tokens,through its ports,along unidirectional connections,called chan-nels.Actors are connected through channels to form models.When an actor is executed it is said to be?red and it may consume tokens from its input ports,pro-duce tokens on its output ports and update its inter-nal state,based on consumed tokens,its parameters and its former state.

The syntactic structure of an actor-oriented design alone says little about the semantics of the model.The semantics is largely orthogonal to the syntax and is de-termined by a so-called model of computation(MoC).

A MoC governs the interaction of actors in a model by de?ning operational rules for executing the actors as well as for the communication between actors.

In this work we concentrate on two data?ow mod-els of computation.In data?ow models,actor computa-tions are triggered by the availability of input data,and connections between actors represent the?ow of data from a producer actor to a consumer actor and are typ-ically bu?ered with FIFO queues.Data?ow models are especially useful to model data-driven processing as in signal processing.The two di?erent data?ow models of computation we use in this work are:

SDF-Synchronous Data?ow:The synchronous data?ow model of computation[13]is a particu-larly restricted special case of data?ow,where all actors in a model must have constant data con-sumption and production rates.This leads to the extremely useful property that deadlock and bu?er boundedness are decidable,and more-over,the scheduling of actor?rings as well as the

bu?er capacity for communication can be com-puted.Note,that SDF in this context is not the SDF of Lustre[9],although it may be possi-ble to adapt these methods to the SDF of Lus-tre.

DDF-Dynamic Data?ow:The dynamic data?ow model of computation does not restrict the data consumption and production rates of actors,but properties such as deadlock and boundedness are often not statically decidable.

We will call the actor model framework in which an actor is embedded its composition framework.The composition framework thereby contains all informa-tion of the actor model except the actors themselves, i.e.it contains the model of computation together with ?ring strategies for the?ring of the actors,as well as the actor’s interconnection information in the model.

For communication,the composition framework pro-vides a set of primitive communication operations that allow an actor to query the state of communication channels and to retrieve or send information from and to channels:

?get(k)retrieves k data tokens via a port,

?put(k)produces k data tokens via a port,?hasToken(k)tests whether get(k)can be success-fully called on a port,

?hasRoom(k)tests whether put(k)can be success-fully called on a port.

These communication operations might be imple-mented di?erently,depending on the model of com-putation,but they always must be present and actors should only communicate using these operations[14]. The exact way an actor is using these operations,deter-mines whether it can work under a given model of com-putation in composition framework,and is captured into what we call an actor’s behavioral type[15].

3.An Automata Based Analysis Strat-

egy

The ability to analyze systems in component based design,in order to check the compatibility of compo-nents and to detect errors in the composite system,is an important factor for system development productiv-ity and system quality.

Instead of performing such analysis directly on the source code of complete actor models,we propose to use a light-weight formalism,based on interface au-tomata,to capture only selected aspects of the actors and the composition framework,which are important for the analysis.

System

Analysis Figure1:The relation of an actor model,its composi-tion and interface automata.

Figure1depicts this analysis strategy.On the top, an actor model and its composite actor are shown. The transformation c MoC is a program transformation from an actor model with a particular model of com-putation into its composition[11].To analyze such a composite actor from its source code is usually very hard,in particular if it is implemented using a conven-tional Turing-complete imperative programming lan-guage.This is because then much of the important in-formation is often not easily accessible anymore or is even not contained explicitly anymore.

In our analysis strategy,we independently extract the necessary information of all actors and the compo-sition framework into separate interface automata at the very beginning,and we then build the composite actor model in the interface automata domain,where the necessary information is preserved during compo-sition.

The framework automaton IA F is extracted from the actor model using a transformation?c MoC.It con-tains all information needed from the composition framework,namely the behavioral type of the model of computation,the interconnection information of the actors in the model and the?ring schedule of the ac-tor model.

The actor automata IA1,IA2and IA3on the other hand are extracted from the actors A1,A2and A3,us-ing a transformation f,and contain the behavioral type of the respective actor in the actor model together with its token consumption and production rate.

This clear separation of actors and their composi-tion frameworks in the automaton domain re?ects the original idea of actor oriented modeling and enables ef-fortlessly replacing one actor automaton by another ac-tor automaton in the automata domain,as we would replace one actor by another actor in the real actor model.

After building these automata,the successful com-position of all actor automata with the framework au-tomaton corresponds to behavioral type checking and ensures component compatibility of all actors with the model of computation of the actor model.The result of this composition is an interface automaton IA Model of the composite actor model,which explicitly contains the interconnection information of the actors,and the ?ring schedule as well as the complete internal token exchange rates of the composite actor model.This in-formation can be used for further static analysis of the actor model to detect errors in the composite system.

In order to capture all the above described informa-tion of actors and their composition frameworks,we present a new interface theory which is tailored towards the use in actor systems and which we call Counting In-terface Automata(CIA).

4.Counting Interface Automata

In this section,we provide an informal description of Counting Interface Automata.For a strictly formal de?nition,which we cannot give here due to space re-strictions,please refer to[18].In Section4.3we will dis-cuss some aspects of Counting Interface Automata and highlight di?erences to other interface theories as Inter-face Automata[5],Resource Interfaces[4]and Timed Interfaces[7].

4.1.Automaton

Counting interface automata consist of a?nite set of states,of which one is the initial state,and a?nite set of transitions.A subset of the states may be labeled as reset states.As other automata,Counting Interface Automata are usually depicted by bubble-and-arc dia-grams.

We distinguish three di?erent kinds of transitions, namely input transitions,output transitions and inter-nal transitions.When modeling a software component, input transitions correspond to the invocation of meth-ods on the component,or the returning of method calls from other components.Output transitions correspond to the invocation of methods on other components,or the returning of method calls from the modeled compo-nent.Internal transitions correspond to computations inside the component.

All transitions are labeled by actions,which are also divided into input actions,output actions and internal actions,depending on the kind of transition they label.

As the name suggests,Counting Interface Automata have the ability to count with numbers.To keep track of counted values,the automaton has a?nite set of counter variables,which can be divided into two dis-joint sets of so-called persistent counter variables and transient counter variables.The values of these counter variables may represent anything countable of interest, as for example the length of a token queue in a com-munication channel of an actor model.The di?erence between the persistent counter variables and the tran-sient counter variables is that the latter ones are re-set to the value nil in every reset state,while the oth-ers keep their value.We will see the importance of this distinction in Section6.

Every transition may contain a guard,which ex-presses a condition on the counter variable values,and which determines whether the transition is enabled. Furthermore,a transition may contain a set of counter declarations and counter assignments,which declare new counter variables or update their values respec-tively when the transition is taken.

So called action quantities on input and output tran-sitions express quantitative aspects of actions on a transition and may also be used to exchange and com-pare counter variable values between two automata during their composition.When modeling a software component,an action quantity could correspond to a countable argument of a method call,as for example the number of data tokens that get consumed dur-ing the method call.Action quantities are particularly interesting during composition,where the equality of quantities is an additional constraint on synchronized shared transitions.

In place of an action quantity,an input transition may also have a so called action quantity declaration. In this case,the action quantity of the input transi-tion does not express a restriction but is instead open and may take on any action quantity value during com-position with another automaton.This value then gets bound to a counter variable which is speci?ed in the ac-tion quantity declaration.This mechanisms allows two automata to exchange counter values during composi-tion and is one of the main features of Counting Inter-face Automata.

For the semantics of the automaton,it is important to note that on a transition,the guard is evaluated af-ter a possible action quantity declaration,but before all counter declarations and counter assignments. Example1Figure2shows an automaton describing the behavioral type of a DDF model of computation to-wards an actor with one input port and one output port, and its output port connected to two input ports of other actors.The number of tokens available in the bu?er of the input ports of the actor and the two connected actors are represented by the persistent counter variables T,Ta and Tb respectively.

State0is the initial state and an internal action step triggers the start of an actor?ring.Then in state1,the model of computation?res an actor,expressed by the out-put action f.In state2,the model of computation is ready to receive any input action hT,g,hR,p or fR,corre-sponding to an actors method calls hasToken(n),get(n), hasRoom(n),put(n)or the return of?re.

All input transitions leaving from state2,except fR, have an action quantity declaration,expressing that the calling actor can pass an argument,namely its own ac-tion quantity,which is then bound to the transient counter variable n.

Using guards and the transient counter variable cT, which represents the number of tokens whose availabil-ity was checked using the hasToken(n)method,the au-tomaton can ensure that the actor can only call the get(n) method after checking the availability of at least n to-kens.During a call to get(n),both counter variables T and cT get decremented by n.Further,a call to has-Room always returns true and a call to put(n)increases the counter variables Ta and Tb,which represent the in-put port bu?ers of the two connected actors,by n.

When describing a software component,a path through a Counting Interface Automaton corre-sponds to an execution of a part of the software component.Therefore,we call a state trajectory an ex-ecution fragment.We call an execution fragment which starts at the initial state of an automa-ton an execution path of the automaton.Further,an execution fragment or execution path is called un-conditional,if it contains only output and inter-nal transitions.Otherwise an execution fragment is called conditional.This distinction is important,be-cause the execution of a conditional execution frag-ment can be avoided by the environment,while the execution of an unconditional execution fragment can-not be avoided.

https://www.wendangku.net/doc/368593013.html,position

Two Counting Interface Automata are only com-posable,if their sets of input actions,output actions and counter variables are disjoint respectively.Input actions of one automaton,may however coincide with output actions of the other automaton.These actions are then called shared actions of the two automata.

hT?[$n]

T>=n / hTT!cT=n,

T

f!

step;

cT>=n / g?[$n]cT-=n, T-=n,

t!

hR?[$n]

hRT!

p?[$n]

Ta+=n, Tb+=n,

pR!

Persistent counter variables: T, Ta, Tb,Transient counter variables: cT, n,

05

4

1

2

3

6

f

fR

hT

hTT hTF g t

hR hRT hRF p pR

Figure 2:An automaton describing the behavioral type of a DDF model of computation.Input,output and internal actions are labeled with ”?”,”!”and ”;”re-spectively and reset states are grey colored.On the right side,input and output actions of the automaton are listed,depicted as communication ports of the au-tomaton to other automata.Note that action quanti-ties equal to 1are often not shown explicitly.

To get the composition of two composable automata,we ?rst build their product .The product of two au-tomata consists of the union of their counter variables and the product of their states.The transitions of the original automata which are labeled with non-shared actions are still present in the product automata,while pairs of transitions with shared actions get synchro-nized and become a single transition with an internal action in the product automaton.A state invariant ,which is added to the start state of such a shared syn-chronized transition during product building,ensures that either the guard of the shared output transition must evaluate to false or that otherwise the guard of the shared input transition must evaluate to true and the action quantities of the shared action must match.Recall that a shared input action with an action quan-tity declaration matches with any output action quan-tity.

Further,if an output transition labeled with a shared action starts at a state in the product where no corresponding input transition labeled with the same shared action exists,another state invariant must en-sure that the guard of the output transition never evaluates to true.

Note,since guards on a transition are evaluated af-ter a possible action quantity declaration,the counter context with which state invariants are evaluated is the

one after evaluating all possible action quantity decla-rations of leaving transitions.

A state in the product automaton is an error state if for any unconditional execution path or for all con-ditional execution paths which lead to this state,the state invariant evaluates to false.

We now get the composition of the two initial au-tomata by removing all states in the product from where there exists an unconditional execution fragment to any error state.If this composition is not empty,the two initial automata are said to be compatible .

An example of the composition of two Counting In-terface Automata is given in Example 4.

4.3.Discussion

The composition and with it the question of com-patibility of two Counting Interface Automata is un-decidable in general.In Section 6we will however see that generated actor and composition framework au-tomata exhibit special topological structures that make the question of composition and compatibility decid-able for behavioral type checking in composite actor models.

Compared to original Interface Automata [5],Counting Interface Automata allow us to create more re?ned interface descriptions of both actors and com-position frameworks.

Counting Interface Automata let us express the to-ken consumption and production rate of an actor in its https://www.wendangku.net/doc/368593013.html,ing original Interface Automata,we could express this information using a number of consecutive calls to getToken()or putToken(),but the behavioral type of the composition framework would then be re-quired to be ready to receive exactly the same number of calls to these methods.This would break the sepa-ration of actors and their composition framework that is central to actor based modelling.Alternatively,the composition framework could be ready to receive any number of calls to these methods,in which case the be-havioral type of the composition framework could not express anymore that an actor may only consume the number of tokens whose availability he initially checked using a call to hasToken().

Using the transient counters and guards of Count-ing Interface Automata,we can express that a com-position framework may be ready to receive calls to a number of methods at a time while still putting require-ments on partial orders between these methods calls.For example a framework may express that for any call to getToken(n)there must have been a call to hasTo-ken(n)somewhen in the past,but that there may be any number of calls to hasRoom()or putToken()in be-

https://www.wendangku.net/doc/368593013.html,ing Interface Automata we could only express this by enumerating all possible valid method call se-quences,which would usually be prohibitive.

As a last point to mention,using assignments to per-sistent counters allows us to model the actor intercon-nection information of a composition framework and the token exchange information of a complete actor model,which is not possible with Interface Automata.

Two other recent interface theories,Timed Inter-faces[7]and Resource Interfaces[4],also have capabil-ities to count in a certain way.One main di?erence be-tween them and Counting Interface Automata is the ability of Counting Interface Automata to exchange counted values between automata during composition, using action quantity declarations.The use of this fea-ture is central in the creation of a composition frame-work automaton as we will see in the next section.Fur-ther,while Resource Interfaces do not allow arbitrary counter variables at all,the counter variables in Timed Automata have di?erent semantics than the ones in Counting Interface Automata in that they model con-tinuously increasing time and their values may only in-crease in automata states.

5.Generating Counting Interface Au-

tomata

The information needed for an actor’s or a frame-work’s counting interface automaton is contained in the actor’s source code and the composition framework it-self.In this section,we will show how to extract this information from actors written in the Cal Actor Lan-guage(C al)[8,1]and from frameworks with an SDF or DDF model of computation.Similar methods could be used to extract this information from other actor de?nition languages as for example StreamIT[17].

5.1.Generating Actor Automata

C al is a domain speci?c language for de?ning the functionality and behavior of actors.Its key goal is to make actor programming easier,and to enable an ac-tor programmer to explicitly express the information and behavioral properties of an actor that are relevant to its usage.This facilitates automatic extraction of ac-tor properties needed to generate counting interface au-tomata.

Example2The code below shows a non-deterministic merge actor,written in C al.

1:actor Mrg()T In1,T In2==>T Out;

2:A1:action[a],[]==>[a]end

3:A2:action[],[a]==>[a]end 4:selector

5:(A1|A2)*

6:end

7:end

The?rst line de?nes the interface of the actor to its en-vironment.This actor has two input ports In1and In2, and one output port Out,and all require tokens of type T.On lines2and3,two actions A1and A2are speci-?ed.Both read one token from input port In1or In2re-spectively,and write the read token out to Out.On line 5,an action selector speci?es the order in which actions are chosen when the actor is?red,using a?nite state ma-chine or equivalently a regular expression.If the actor is ?red,one of the actions is chosen and executed,depend-ing on the action selector and the availability of tokens on the input ports.

The?rst step of generating the counting interface automaton of a C al actor,is to transform the actor code from the rather declarative C al to the impera-tive Cal?ow[18],which is an intermediate format of C al.There,all data dependencies are explicitly re-solved and a sequential schedule for so-called atomic steps that get executed during the?ring of an action, is given.Examples for such atomic steps are checking the availability of tokens,consuming tokens,produc-ing tokens,or computing statements.

With the information on the number of consumed and produced tokens,each of these atomic steps can directly be transformed to a short state trajectory that is speci?c for every type of atomic step.Put together in the order of the sequential schedule of the original atomic steps,all these short state trajectories lead to a larger state trajectory which describes the interaction of an actor with its composition framework during the execution of one action of the actor.

We then take the action selector in its?nite state machine form,and replace all states with reset states of counting interface automata and all transitions,each corresponding to the execution of one action,with the above state trajectories.This leads to the complete counting interface automaton of the actor.

Example3Figure3shows the counting interface au-tomaton of the non-deterministic merge actor Mrg from Example2.

In its initial state,the actor waits for a?re input ac-tion f from the director.Then one of the actions is cho-sen non-deterministically.In each action,the actor?rst checks whether one token is available with the hT action. It then waits for an answer from the director and if pos-itive,it gets one token and puts one token to the output port.It returns to its initial state with a?re return out-put action fR.

124

356

7

8910111213

14

Mrg:director:fR!

Mrg:In2:hTF?

Mrg:Out:pR?

Mrg:In2:hT![1]Mrg:In2:hTT?Mrg:In2:g![1]Mrg:In2:t?Mrg:Out:p![1]

Mrg:In1:hT![1]Mrg:In1:hTT?Mrg:In1:g![1]Mrg:In1:t?Mrg:Out:p![1]

Mrg:director:fR!

Mrg:In1:hTF?

Mrg:Out:pR? Mrg:director:f?

Mrg:In1:hT

Mrg:In1:hTT

Mrg:In1:hTF

Mrg:In1:g

Mrg:In1:t

Mrg:In2:hT

Mrg:In2:hTT

Mrg:In2:hTF

Mrg:In2:g

Mrg:In2:t

Mrg:Out:hR

Mrg:Out:hRT

Mrg:Out:hRF

Mrg:Out:p

Mrg:Out:pR Mrg:director:f

Mrg:director:fR

*

Figure3:The automaton of a non-deterministic merge actor.

5.2.Generating Framework Automata

When generating the framework automaton of an actor model,we need to capture the behavioral type of the model of computation,the connection informa-tion and the scheduling information of the actor model into it.

First,we represent the current number of tokens in every communication channel using one persistent counter variable for each channel.

To capture the behavioral type of the model of com-putation,we separately create partial automata to han-dle every actor in the model.Each of these partial au-tomata starts with an output transition to?re the ac-tor,which leads to a state in which the actor is active and may execute,and from where an input transition leaves again which receives the?re return from the ac-tor.

In the state where the actor is active and may exe-cute,the composition framework must be ready to re-ceive commands from the actor in any valid order.For this,a short transition sequence for every valid com-mand leaves this state and returns again to it in a cy-cle.The valid execution order of the commands is en-sured with a set of transient counters and guards on the leaving transitions.

An example of a partial automaton with a DDF model of computation is shown in Example1in Sec-tion4.

The connection information of the original actor model is preserved using counter assignments on the automata sequence of the put command.Whenever an actor calls the put command on one of its output ports, all persistent counter variables that represent bu?ers in communication channels connected to this output port get incremented by the number of tokens speci?ed by the actor.

Finally,for the scheduling information,we assume that an execution schedule is available in form of a?-nite state machine,where transitions represent actor ?rings.To create the framework automaton,we then take this execution schedule and replace its states with reset states of counting interface automata and its tran-sitions with the corresponding partial automata,which we built above.

For frameworks with one of the two data?ow models of computation,which we introduced at the beginning, we make the following assumptions:

SDF The actor?ring schedule is completely known and deterministic,which enables the composition framework to compute the size of all communica-tion bu?ers and to ensure the availability of to-kens prior to?ring any actor.An actor is there-fore not required to check the availability of to-kens on its input ports or the availability of room on its output ports.

DDF The actor?ring schedule is completely non-deterministic and there are in?nite bu?ers in all communication channels.An actor must therefore check the availability of tokens on its input ports, but is not required to check the availability of room on its output ports.

6.Behavioral Type Checking

As we mentioned in Section4.3,the question of com-patibility of two Counting Interface Automata is unde-cidable in general.We will however show that the au-tomata we generated in the last section exhibit special topological structures and features which make behav-ioral type checking decidable.

6.1.Topological Structures of Generated

Automata

Figure4a)shows some examples of typical actor au-tomata topologies.By construction,all paths between two reset states in an actor automaton are?nite and each path corresponds to one possible?ring of the ac-tor.

In contrast,typical framework automata topologies have loops and therefore in?nite paths between reset sates,as can be seen in Fig.4b).An important prop-erty of all of these loops is however,that they all start

with an input transition and their execution can thus be controlled from outside.Further,any path between two reset states corresponds again to one ?ring of an actor.

When we build the product of all actor automata of a model and its framework automaton,the above men-tioned topologies and properties lead to a product au-tomaton,that consists of the product of the reset states of all automata,interconnected by ?nite paths,each corresponding to an actor ?ring.Some typical prod-uct automata topologies are shown in Fig.1

c).

a)c)

b)Figure 4:Typical topological structures of a)generated actor automata,b)generated framework automata,and c)products of actor and framework automata.

https://www.wendangku.net/doc/368593013.html,position and Decidability

Let us ?rst remind that the behavioral type of both an actor and a model of computation,expresses what behavior an actor and a model of computation expect from each other during one ?ring of the actor in a com-position framework with a given model of computa-tion.Thus,when we look at the generated automata from Section 5and their typical topological structures,which were highlighted above,we see that the au-tomata parts important for behavioral type checking,are only the state trajectories starting and ending at re-set states.

Further let us remind,that when we built the frame-work automaton of a composition framework,we used persistent counter variables only to represent the cur-rent number of tokens in communication channels.But to express the behavioral type of the model of compu-tation in a composition framework,we only used tran-sient counters variables.For behavioral type checking,

persistent counter variables in the automata are there-fore of no importance and we can ignore their values.We must then however assume that all guards and in-variants on persistent counter values may evaluate to both true and false during composition.

For behavioral type checking,we are now only car-ing about the values of transient counters and we know that they are reset in every reset state.Further we know,that by construction,the product of all state trajectories between two reset states are state trajec-tories of ?nite length.These properties make the com-position of state trajectories between two reset states in the product automaton decidable.And since each state trajectory between two reset states in the prod-uct automaton corresponds to one actor ?ring in the actor model,the successful composition proofs behav-ioral type compatibility of the corresponding actor with the model of computation of the composition frame-work.

By successfully composing all state trajectories be-tween reset states in the product automaton,we can therefore ensure behavioral type compatibility of all ac-tors with the composition framework.We will end up with a composite actor automaton in which the internal token exchange information is contained in the previ-ously ignored persistent counter assignments along the composed state trajectories between reset states.Example 4In this example,we check the behavioral type compatibility of a simple actor,which was imple-mented to run with an SDF model of computation,with a DDF model of computation.The actor consumes one to-ken on its input port and produces one token on its out-put port,and since it was implemented to run with a SDF model of computation,it does not check the availability of tokens prior to consuming them.

Figure 5shows the actor automaton on the top left,the relevant part of the framework automaton on the top right,and their product automaton,annotated with the context of the transient counters of each state,at the bot-tom.Note that the counter context of a state must already re?ect action quantity declarations of leaving transitions,because guards on a transition are evaluated after the ac-tion quantity declarations on the same transition.When the actor tries to get a token without ?rst checking its availability,the guard on the corresponding input transi-tion of the framework automaton evaluates to false and the transition will therefore not be active,leading to the error state 2:1in the product.After pruning,the compo-sition will be empty,showing as expected the interface in-compatibility of the SDF actor with the DDF model of computation.

T-=3,

Ta+=2, Tb+=2,

f?

g![3]

t?

stmt;

p![2]

pR?

fR!

1

2

3

4

5

6

*f fR

g

t p pR

h T ?[$

n ]T >=

n

/ h T T !

c T =n ,

T

h

T F !

fR?f!

step;

cT>=n / g?[$n]cT-=n, T-=n,

t!

hR?[$n]

hRT!

p ?[$n ]

T a +=n , T b

+=n ,

p R !

Persistent counter variables: T, Ta, Tb,Transient counter variables: cT, n,

5

4

1

23

6

f fR hT hTT

hTF

g t hR hRT hRF p pR

*Context:cT=nil,n=nil,

Context:cT=nil,n=3,Context:cT=nil,n=nil,

Context:cT=nil,n=3,

Context:cT=nil,n=3,

Context:cT=nil,n=2,

Context:cT=nil,n=2,

Context:cT=nil,n=2,

Figure 5:The composition of a simple SDF actor with a DDF model of computation.

https://www.wendangku.net/doc/368593013.html,posite Actor Model Analysis

The information contained in the model automaton can be analyzed using a variety of di?erent analysis techniques.Here,we only show as an example,how the token exchange information can be extracted from the model automaton.A case study,where Petri nets [16]are used to analyze this information is given in [18].We can extract the token exchange information of a model automaton into another automaton,which we call the token exchange automaton .The states of this automaton are the reset states of the model automaton,and the transitions correspond to the paths between the reset states of the model automaton and contain all assignments to persistent counter variables along these paths.In this new automaton,the states repre-sent the internal states of the composite actor model and each transition represents one internal actor ?r-ing,with the assignments on the transition represent-ing the token exchange rates.

Example 5Consider an actor model with feedback loops,as in Fig.6.The actor Src alternatingly gen-erates one token on its upper or its lower port,each time it is ?red.The actors FA and FB are identi-cal and both consume one token from each of their in-put ports and produce one token on their output port,each time they are ?red.Finally,the actor Mrg is the non-deterministic merge actor from Ex.2.

FA

Mrg

Src

FB

Figure 6:An actor model with feedback.After automata generation and composition of the above actor model,we will eventually get a model automa-ton from which the token exchange automaton shown in Fig.7can be extracted.

The analysis of this extracted token exchange infor-mation will show that the upper input port of actor FA and/or the lower input port of actor FB,will eventually over?ow.

8.Conclusions

We proposed a new interface theory that is capable of counting with numbers,called Counting Interface Automata (CIA).In our presented actor model analy-sis strategy,we used this interface theory to represent the interface information of actors and their compo-sition framework.Thereby,its capabilities allowed us to capture temporal and quantitative aspects of an ac-

Mrg;

Mrg:In1:T-=1,FA:In2:T+=1,FB:In2:T+=1,

Mrg;

Mrg:In2:T-=1,FA:In2:+=1,FB:In2:T+=1,

FA;

FA:In1:T-=1,FA:In2:T-=1,Mrg:In1:T+=1,

FB;

FB:In1:T-=1,FB:In2:T-=1,Mrg:In2:T+=1,

Src;

FA:In1:T+=1,

Src;

FB:In1:T+=1,

Mrg;

Mrg:In1:T-=1,FA:In2:T+=1,FB:In2:T+=1,

Mrg;

Mrg:In2:T-=1,FA:In2:+=1,FB:In2:T+=1,

FA;

FA:In1:T-=1,FA:In2:T-=1,Mrg:In1:T+=1,

FB;

FB:In1:T-=1,FB:In2:T-=1,Mrg:In2:T+=1,

1

*Persistent counter variables:

FA:In1:T, FA:In2:T, FB:In1:T, FB:In2:T, Mrg:In1:T, Mrg:In2:T,

Figure 7:The token exchange information of the ac-tor model in Fig.6,extracted from the composite ac-tor automaton.

tors interface towards its composition framework and we could also capture the interconnection information,the ?ring schedule as well as the token exchange infor-mation of the the complete actor model.

We then presented a method to generate CIAs of actors written in C al and for composition frameworks with an SDF or DDF model of computation.

We showed,that by composing all CIAs,we could ?rstly prove behavioral type compatibility of all ac-tors with a composition framework and secondly get a single automaton that contained much information for further static analysis of the composite actor model.

References

[1]The Caltrop Project.

https://www.wendangku.net/doc/368593013.html,/caltrop.[2]The Ptolemy II Project.

https://www.wendangku.net/doc/368593013.html,.

[3]G.A.Agha.ACTORS:A Model of Concurrent Compu-tation in Distributed Systems .The MIT Press Series in Arti?cial Intelligence.MIT Press,Cambridge,1986.[4] A.Chakrabarti,L.de Alfaro,T.A.Henzinger,and

M.Stoelinga.Resource Interfaces.In Proceedings of the Third International Conference on Embedded Soft-ware (EMSOFT),Lecture Notes in Computer Science 2855,pages 117–133.Springer-Verlag,2003.

[5]L.de Alfaro and T.A.Henzinger.Interface Automata.

In Proceedings of the Ninth Annual Symposium on Foun-dations of Software Engineering (FSE),pages 109–120.ACM Press,2001.

[6]

L.de Alfaro and T.A.Henzinger.Interface Theories for Component-based Design.In Proceedings of the First International Workshop on Embedded Software (EM-SOFT),Lecture Notes in Computer Science 2211,pages 148–165.Springer-Verlag,2001.

[7]

L.de Alfaro,T. A.Henzinger,and M.Stoelinga.Timed Interfaces.In Proceedings of the Second Inter-national Workshop on Embedded Software (EMSOFT),Lecture Notes in Computer Science 2491,pages 108–122.Springer-Verlag,2002.

[8]

J.Eker and J.Janneck.Caltrop —Language re-port (Draft).Technical memorandum,Electronics Research Lab,Department of Electrical Engineering and Computer Sciences,University of California at Berkeley California,Berkeley,CA 94720,USA,2002.https://www.wendangku.net/doc/368593013.html,/caltrop.

[9]

N.Halbwachs,P.Caspi,P.Raymond,and D.Pilaud.The Synchronous Data Flow Programming Language Lustre.Proceedings of the IEEE ,79(9):1305–1319,1991.[10]

C.Hewitt.Viewing Control Structures as Patterns of Passing Messages.Journal of Arti?cial Intellingence ,8(3):323–363,June 1977.

[11]

J.W.Janneck.Actors and Their Composition.to ap-pear in:Formal Aspects of Computing ,2003.prelimi-nary version:Technical Report UCB/ERL M02/37.[12]

E.A.Lee.Overview of the Ptolemy Project.Techni-cal Memorandum UCB/ERL M01/11,Electronics Re-search Lab,Department of Electrical Engineering and Computer Sciences,University of California at Berke-ley California,Berkeley,CA 94720,USA,March 2001.[13]

E.A.Lee and D.Messerschmitt.Synchronous Data Flow.Proceedings of the IEEE ,pages 55–64,Septem-ber 1987.

[14]

E.A.Lee,S.Neuendor?er,and M.J.Wirthlin.Actor-Oriented Design of Embedded Hardware and Software Systems.Journal of Circuits,Systems,and Computers ,12(3):231–260,2003.

[15]

E.A.Lee and Y.Xiong.A Behavioral Type System and Its Application in Ptolemy II.to appear in:Aspects of Computing Journal,special issue on Semantic Founda-tions of Engineering Design Languages.,2003.This ver-sion:November 10,2003.

[16] C.A.Petri.Kommunikation mit Automaten .PhD the-sis,Bonn:Institut f¨u r Instrumentelle Mathematik,1962.[17]

W.Thies,M.Karczmarek,and S.Amarasinghe.Streamit:A Language for Streaming Applications.In Proceedings of the 11th International Conference on Compiler Construction,Grenoble,France,LNCS 2304.Springer-Verlag,April 2002.

[18]

E.Wandeler.Static Analysis of Actor Networks.Techni-cal Memorandum UCB/ERL M03/7,Swiss Federal In-stitute of Technology,Zurich,Switzerland,March 2003.(Diploma Thesis).

相关文档