Specification, Testing and Analysis of (Dynamic) Software Architecture with the Chemical Ab
Speci?cation,Testing and Analysis of(Dynamic)Software Architecture with the Chemical Abstract Machine
Michel Wermelinger
Departamento de Inform′a tica,Universidade Nova de Lisboa
2825Monte da Caparica,Portugal
E-mail:mw@di.fct.unl.pt
ABSTRACT
We feel that the Chemical Abstract Machine(CHAM)is a useful formal description technique for static and dynamic software architectures that facilitates analysis and testing. Our position is based on work done so far and on the poten-tial of rewriting approaches,of which the CHAM is a special case.
1INTRODUCTION
The chemical model of computation was introduced by Ban?a tre and Le M′e tayer[2]and then re?ned by Berry and Boudol[3].Inverardi and Wolf[7]were the?rst to apply it to Software Architecture but since then other papers have appeared[9,8,16,15].
The next section brie?y recapitulates the CHAM formalism for those readers not familiar with it.The third section sur-veys its application to Software Architecture and section4 presents a simple example.The last two sections show some possible future research paths and make some concluding re-marks.
2THE CHAM MODEL
The chemical model views computation as a sequence of re-actions between data elements,called molecules.The struc-ture of molecules is de?ned by the designer.The system state is described by a multiset of molecules,the solution. The possible reactions are given by rules of the form
m1m i m1m j
where m1i and m1j are molecules.If the current solution contains the molecules given on the left-hand side of a rule, that rule may be applied,replacing those molecules by the ones on the right-hand https://www.sodocs.net/doc/0517801601.html,ually a CHAM is presented using rule schemata,the actual rules being instances of those schemata.There is no control mechanism.At each moment, several rules may be applied,and the CHAM chooses one of them non-deterministically.A solution is inert when no reaction rule can be applied.
Any solution can be considered as a single molecule using the membrane operator.A solution within a membrane can thus be a subsolution of another solution or an argument of a molecule operator.For example,if the molecule con-structors are the constant0and the unary function s,then
s(0,s(0)),0
is a solution containing two molecules.Membranes encap-sulate molecules and thus force reactions to be local.In other words,the solution inside a membrane evolves inde-pendently of the solution outside the membrane.For exam-ple,if a CHAM included the rule
then the above solution could be transformed into
s(s(0))
after two(possibly simultaneous)rewriting steps.
The airlock operator constructs a molecule m S from a solution S m S,where is the multiset union operator.In words,it picks a molecule from a solution and puts the rest of that solution within a membrane.The operator is reversible, which means that S can again be obtained from m S. For example,using twice the airlock operator it is possible to transform the original solution into
0s(s(0)0)
3SOFTW ARE ARCHITECTURE AND THE CHAM In[7]the CHAM was used to specify and analyze the com-putational behavior of static software architectures.That ar-ticle uses the multi-phase compiler architecture as an exam-ple.For each component(phase)there is a molecule repre-senting its state.Depending on their state,certain molecules may interact,exchanging data(characters,tokens,etc.).Two different architectures—a sequential and a concurrent one—were speci?ed and it was proven that the latter terminates (for?nite input)and subsumes the https://www.sodocs.net/doc/0517801601.html,ing membranes to represent modular architectures,a third architecture was described with one membrane including the compiler’s back-end while another contained its front-end.The correctness of
the module interfaces was also proven.Other kinds of anal-ysis performed on the CHAM model are architecture re?ne-ment[9]and deadlock detection[8].
In[16,15]we have proposed to apply the CHAM to dynamic software architectures,i.e.,architectures that can be changed by the system itself(based on its current state or topology) or by the user(and thus in an unpredictable way).We call it programmed and ad-hoc recon?guration,respectively,fol-lowing[6].To explicitly represent the topology and the user-requested changes we introduced molecules to represent con-nections and the four basic recon?gurations commands used by most languages([6,12,1]among others),namely addi-tion and removal of components and connections.
Related to programmed recon?guration is the idea of self-organizing architectures[10].The goal is to minimize the amount of explicit management.Ideally,the architecture “knows”what to do when a recon?guration triggering event (like component failure,or addition of a new component) occurs.It is obvious that the CHAM is ideally suited for these architectures because the evolution of the solution(that represents such an architecture)depends only on the exist-ing molecules,i.e.,on the solution itself.This absence of an external control mechanism also means that the reactions will only stop when no reaction rule is applicable.Thus the CHAM is adequate to represent architectures with poten-tially in?nite distinct con?gurations,something an approach like[1]cannot handle.
A previous proposal to deal with dynamic architectures[14] views an architecture as a graph,where nodes denote com-ponents and arcs represent connections,and an architectural style as a class of graphs.This means that recon?gurations are speci?ed by graph rewriting rules and architectural styles are given by context-free grammars.Moreover,[14]pro-vides a general method to check whether the rewriting rules keep the architectural style or not,i.e.,whether the resulting graph belongs to the same class as the original one.
This approach can be straightforwardly adapted to the chem-ical model because graph grammars and rewriting rules are basically CHAMs with one kind of molecules to represent non-terminal symbols and two kinds of molecules for ter-minal symbols(the graph’s nodes and arcs).We thus pro-posed[16]to specify architecture style and recon?guration by two different CHAMs,the creation CHAM and the evo-lution CHAM.The former uses the initial solution to impose global system modi?cation constraints(e.g.,the maximal number of components)while the reaction rules enforce lo-cal component properties(e.g.,the number of bindings[10]). The reaction rules of the evolution CHAM specify how the solution that describes the architecture can be transformed. Even if the creation CHAM is not context-free(i.e.,at least one of its rules has more than one molecule on its left-hand side),it may be possible to prove straightforwardly that the evolution CHAM keeps the architectural style by showing (through inspection)that its rules are invariants regarding the style’s properties.
In[15]we have also shown how a restricted form of code mobility can be easily achieved by encoding rules as molecules with a special operator symbol.Such molecules, like any other,can permeate through membranes to another part of the system where they are interpreted by rules whose left-hand sides check for molecules with the special syntax. 4EXAMPLES
To illustrate the speci?cation and analysis of architectural style and ad-hoc recon?guration we will repeat the example presented in[16]which is an extension of the example used by Le M′e tayer[14].It is a client-server system with a cen-tralized manager.A client sends a request to the manager which forwards it to an available server.The server’s reply is sent back to the correct client via the manager.There must always be at least one server.
The structure of molecules is thus given by the following grammar,which leaves the precise syntax of component identi?ers open.
Molecule:=Component Link Command
Component:=Id:Type
Type:=C M S
Link:=Id—Id
Command:=cc(Component)rc(Id)
The CHAM that speci?es the client-server style is
cc(m:M)c:C,c—m,cc(m:M)
cc(m:M)s:S,m—s,cc(m:M)
s:S,cc(m:M)s:S,m:M
Assuming that the initial solution given by the user contains just the creation command cc()with the manager’s name, the?rst rule adds a client and its link,the second rule adds a server and its connection,and the last rule actually creates the manager,if at least one server has been previously cre-ated.
Now we turn to the evolution of such an architecture.Be-sides adding and deleting clients as in[14],we also deal with server and manager creation and removal.Each change must be explicitly invoked by an appropriate command,to be handled by(at least)one reaction rule of the recon?guration CHAM.
cc(c:C),m:M c:C,c—m,m:M
cc(s:S),m:M s:S,m—s,m:M
rc(c),c:C,c—m
s:S,rc(s),s:S,m—s s:S
m:M,rc(m),cc(m:M)m:M
m—s,m:M m—s,m:M
c—m,m:M c—m,m:M
The?rst four rules deal with client and server creation and removal,while the other rules handle manager substitution, which is indicated by a pair of creation/removal commands. The last two rules relink the existing clients and servers to the new manager.Notice that we assume different variables to be instantiated with different identi?ers.Otherwise the right-hand sides would be instances of the left-hand sides.In other words,those two rules could be immediately reapplied (although provoking no change in the architecture)and the solution would never become inert.
This CHAM illustrates ad-hoc recon?guration because the recon?guration commands appear only on the left-hand sides of rules.In other words,the commands are only consumed by the CHAM and thus must have been put into the solution by the user.As an example of recon?guration,let us assume that we have an architecture with a single server(and man-ager,of course),and we want to add a client and replace the manager.The initial solution for the evolution CHAM is
m1:M,m1—s1,s1:S,cc(c1:C),rc(m1),cc(m2:M)
and the states of the solution until it becomes inert are
m1:M,m1—s1,s1:S,c1:C,c1—m1,rc(m1),cc(m2:M) m2:M,m1—s1,s1:S,c1:C,c1—m1
m2:M,m2—s1,s1:S,c1:C,c1—m1
m2:M,m2—s1,s1:S,c1:C,c1—m2
In general,to make sure that the speci?cation is correct,it is necessary to prove that a CHAM terminates,i.e.,that an inert solution can be https://www.sodocs.net/doc/0517801601.html,ually this involves some assumptions on the initial solution.For our example we are assuming the initial solution contains just one molecule of the form cc(m:M).Then it is quite easy to prove that the style CHAM always terminates(assuming fairness in rule selection):the third rule consumes the cc()command that is necessary for any of the rules to be triggered.Hence the computation terminates.
Another issue is to prove that the architectures generated by the creation CHAM are really those that we intended.To-wards that end it is necessary to write down the properties of the architectural style and then,given the initial solution, prove that any inert solution will obey those properties. Returning to our example,the properties of the client-server style are:
there is exactly one manager;
there are x0clients,each one linked to the manager;
there are y0servers,each one linked to the manager. As an illustration,we will just prove that the third propo-sition is true of the creation CHAM.If the solution is in-ert,then there is no cc(m:M)command because otherwise the?rst two reaction rules could be applied.Since there is such a command in the initial solution,it must have been consumed somehow.By inspection of the rules,this is only possible by the third reaction rule.However,that rule can only have been applied if there existed a server.Since no rule decreases the number of servers,it is proven that at least one server must have been created and that it has not been removed by the application of some other rule.As for the server links,the only rule that creates servers connects them to the component whose name is given by the cc()command. This completes the proof of the third property,assuming that while proving the?rst one it has been established that the manager’s name is the one given by the cc()command. Sometimes it is necessary to prove that a recon?guration will not“break”the style.For some properties this can be done inductively:prove that the initial solution of the recon?gura-tion CHAM satis?es the property and that each rule keeps it. The?rst part is usually not needed since it is assumed that the initial solution is either an inert solution of the creation CHAM(and thus satis?es the properties as proven before) or it is the inert solution of a previous recon?guration(and therefore satis?es the properties as it will be proven by in-spection of the rules).It thus suf?ces to prove that for each rule L R,if it is applied to a solution S that satis?es the property,then S L R also satis?es it.
As an illustration we will prove that the client-server recon-?guration CHAM keeps at least one server.Let y(resp.y) be the number of servers immediately before(resp.after)the application of a rule.One has to prove that y0y0for each rule.The second rule states that y y1,the fourth
rule that y2y y1,and for the remaining rules y y.It is obvious that for each one the implication is true. However,the second part of the third property,namely that each server is linked to the manager,cannot be proven in this way because it is not an invariant of the system.In fact,due to rule5of the evolution CHAM,the solution does not repre-sent a graph temporarily:there are links m—s but there is no m!The connectivity property can thus only be established for inert solutions.The proof goes as follows.First show that there is always exactly one manager.Next prove that there is always exactly one connection m—s for each server s.Finally show that for inert solutions,if m:M is the man-ager and m—s is a server connection,then m=m.The?rst two statements can be proven inductively,the third results from the fact that in an inert solution the last two rules of the evolution CHAM cannot be applied.
To illustrate programmed recon?guration we show how the lazy pipeline described in[11]can be speci?ed with a CHAM.The pipeline is a composite component with two communication ports called in and out.Internally,the pipeline consists of a?lter and another pipeline.The archi-tecture is thus recursive.A?lter has three ports:an input port prev and two output ports next and out.The con-
nections to the enclosing and enclosed pipelines are shown in the following
diagram.
The main characteristic of the example is that pipelines are only created on demand,in particular,when a message is sent to its in port.The example is used in[11]to illustrate the use of the dyn keyword of the Darwin architecture description language.We will show how it is possible to obtain the same effect with the CHAM.
First we de?ne the syntax of molecules.We use positive integers in unary notation to uniquely identify components. Molecule:=Component Connection Command Component:=Port Number:Molecule
Port:=PortName/Molecule
PortName=PortName=Message PortName:=Number.Id Id
Connection:=PortName—PortName
Command:=cp(Number)
Number:=11Number
Next we need some general rules to describe communication between components.The?rst rule describes how a message is passed from a port p to a port q linked to p and ready to receive a message.
p=msg,p—q,q=p=,p—q,q=msg
The next two rules allow messages to cross membranes and thus permit communication between composite components. One rule makes a port visible to the environment,the other rule“internalizes”the port once it has received a message. After the component has processed the message,the former rule may be used again.
n:p=S n.p=,n:S
n.p=msg,n:S n:p=msg S
The last communication rule is the more important one for this example.It allows to attach an arbitrary solution to a port and add that solution to the system once the?rst message is received by or sent from that port.The solution may con-tain arbitrary recon?guration commands,new components and connections.It thus generalizes Darwin’s dyn construct.
p=msg,p/S p=msg,S
For the example,only one recon?guration command is nec-essary,namely to create a pipeline.We assume the initial solution contains the molecule cp(1)to create the outermost pipeline according to the following rule:
cp(n)n:in=,out=,
1n:prev=,next=,out=,
in—1n.prev,1n.out—out,
1n.next/cp(11n),
1n.next—11n.in,11n.out—out
When the?lter sends its?rst message through port next,a new pipeline and its connections will be created.We have thus programmed recon?guration and the recursive structure of the architecture is immediately apparent from the rule be-cause the cp()command appears on both sides.
5FUTURE WORK
Although work done so far already shows how the CHAM can be used to specify and analyze both static and dynamic architectures,it is possible to further explore this formalism. On the one hand,a CHAM is a term rewriting system(TRS) with an associative and commutative operator(namely mul-tiset union).We thus seek to use or adapt techniques de-veloped for TRS to prove termination of recon?guration and uniqueness of the resulting architecture.
On the other hand,the CHAM can be encoded in rewriting logic[13]and thus tools for that framework can be used to test architecture speci?cations written in CHAM.We will look at Maude[5]and ELAN[4].The latter allows the sepa-rate speci?cation of a computational system(in our case,the CHAM model),a particular instance(in our case,a CHAM representing a dynamic architecture style),and a query(a speci?c architecture with given recon?guration commands). ELAN would then compute the resulting architecture,allow-ing the user to check whether the outcome is the expected one.The computation can be traced,which helps the user debug the speci?cation.
6CONCLUDING REMARKS
We perceive the following general advantages of the CHAM: It is a simple and operational programming model.
There is a single data structure(multisets)and a single programming construct(rewrite rules),both of which are familiar and intuitive concepts.The speci?cations tend thus to be rather compact and easy to write and read.
It is a general-purpose formalism.Its?exibility stems mainly from the fact that the de?nition of the molecules is left to the designer.This has a two fold advantage.
First,as much or as little detail can be included as nec-essary for the application at hand.Second,the most ap-propriate representation can be chosen for each element of the application.
It is suitable for systems whose global evolution de-pends on local states(namely of those molecules that appear on the left-hand sides of rules).This makes it easier to build systems incrementally and to prove prop-erties about them.
Of course,the CHAM is not a universal panacea,and there-fore some architectures,especially those that rely on global state or negative properties may be hard or even impossi-ble to specify.Also,since molecules are entirely built from the constants and operators de?ned by the user,architectures which need common data types(like booleans and integers) and operations(like sum and comparison)are a bit tedious and lengthy to specify,and not very readable.
However,all in all we feel that the CHAM is an adequate formalism for the speci?cation,analysis and testing of cer-tain classes of(possibly modular)static and dynamic soft-ware architectures due to its characteristics:it is simple, making proofs often straightforward;it is?exible,allow-ing the representation of components,connections,and re-con?guration commands;it is an abstract formalism,sub-suming other approaches like context-free grammars for ar-chitectural style speci?cation;it is a term rewriting system, thus potentially making use of available theoretical results and practical tools.
ACKNOWLEDGEMENTS
The?nancial support of FCT through project PRAXIS XXI 2/2.1/TIT/1662/95(SARA)is gratefully acknowledged. REFERENCES
[1]R.Allen,R.Douence,and D.Garlan.Specifying and
analyzing dynamic software architectures.In Funda-mental Approaches to Software Engineering,volume 1382of LNCS,pages21–37.Springer-Verlag,1998. [2]J.-P.Ban?a tre and D.L.M′e tayer.Gamma and the chem-
ical reaction model:Ten years after.In J.-M.An-dreoli,C.Hankin,and D.L.M′e tayer,editors,Coordi-nation programming:mechanisms,models and seman-tics,pages3–41.Imperial College Press,1996.
[3]G.Berry and G.Boudol.The chemical abstract ma-
chine.Theoretical Computer Science,(96):217–248, 1992.
[4]P.Borovansk′y,C.Kirchner,H.Kirchner,P.-E.Moreau,
and M.Vittek.ELAN:A logical framework based on computational systems.In Proceedings of the First In-ternational Workshop on Rewriting Logic,volume4of Electronic Notes in Theoretical Computer Science.El-sevier,1996.
[5]M.Clavel,S.Eker,P.Lincoln,and J.Meseguer.Prin-
ciples of Maude.In Proceedings of the First Interna-tional Workshop on Rewriting Logic,volume4of Elec-tronic Notes in Theoretical Computer Science,pages 65–89.Elsevier,1996.
[6]M.Endler.A language for implementing generic dy-
namic recon?gurations of distributed programs.In Pro-ceedings of the12th Brazilian Symposium on Computer Networks,pages175–187,1994.
[7]P.Inverardi and A.L.Wolf.Formal speci?cation and
analysis of software architectures using the chemical abstract machine.IEEE Transactions on Software En-gineering,21(4):373–386,Apr.1995.
[8]P.Inverardi,A.L.Wolf,and D.Yankelevich.Checking
assumptions in component dynamics at the architecture level.In Coordination Languages and Models,volume 1282of LNCS,pages46–63.Springer-Verlag,1997. [9]P.Inverardi and D.Yankelevich.Relating CHAM de-
scriptions of software architectures.In Proceedings of the8th International Workshop on Software Speci?ca-tion and Design,pages66–74.IEEE Computer Society Press,1996.
[10]J.Kramer and J.Magee.Self organising software ar-
chitectures.In Joint Proceedings of the SIGSOFT’96 Workshops,pages35–38.ACM Press,1996.
[11]J.Magee and J.Kramer.Dynamic structure in soft-
ware architectures.In Proceedings of the Fourth ACM SIGSOFT Symposium on the Foundations of Software Engineering,pages3–14.ACM Press,1996.
[12]N.Medvidovic.ADLs and dynamic architecture
changes.In Joint Proceedings of the SIGSOFT’96 Workshops,pages24–27.ACM Press,1996.
[13]J.Meseguer.Rewriting logic as a semantic frame-
work for concurrency:a progress report.In CON-CUR’96:Concurrency Theory,7th International Conference,volume1119of LNCS,pages331–372.
Springer-Verlag,1996.
[14]D.L.M′e tayer.Software architecture styles as graph
grammars.In Proceedings of the Fourth ACM SIG-SOFT Symposium on the Foundations of Software En-gineering,pages15–23.ACM Press,1996.
[15]M.Wermelinger.Software architecture evolution and
the chemical abstract machine.In International Work-shop on the Principles of Software Evolution,pages 93–97,Kyoto,Japan,Apr.1998.
[16]M.Wermelinger.Towards a chemical model for soft-
ware architecture recon?guration.In Proceedings of the Fourth International Conference on Con?gurable Distributed Systems,pages111–118.IEEE Computer Society Press,1998.