scieee AI-readable full text Open interactive document viewer

Specifying Dynamic Software Architectures by Using Membrane Systems

Cavaliere, Matteo; Deufemia, Vincenzo

Abstract

We present a formalism for the definition of dynamic software architectures in terms of membrane systems, distributed computational models inspired from the structure and the functioning of living cells. The dynamics (the evolution) of the overall architecture is defined by rules that modify the contents (data) and structure of the membrane system. The evolution of the membrane system can be statically checked to ensure that some properties imposed by the architecture are preserved.

Full text

Specifying Dynamic Software Architectures by Using Membrane Systems Matteo Cavaliere1, Vincenzo Deufemia2 1Research Group on Natural Computing Department of Computer Science and Artificial Intelligence University of Sevilla Avda. Reina Mercedes s/n, 41012 Sevilla, Spain E-mail: [email protected] 2Dipartimento di Matematica e Informatica Universit`a di Salerno Fisciano(SA), Italy E-mail: [email protected] Summary. We present a formalism for the definition of dynamic software architectures in terms of membrane systems, distributed computational models inspired from the structure and the functioning of living cells. The dynamics (the evolution) of the overall architecture is defined by rules that modify the contents (data) and structure of the membrane system. The evolution of the membrane system can be statically checked to ensure that some properties imposed by the architecture are preserved. 1 Introduction A software architecture provides a high-level system description in terms of a collection of computational components and connectors. Components typically encapsulate information or functionality while connectors coordinate the communication between components. In particular, software architectures describe the decomposition of a system into components, the interconnection of the components, and component interaction [18] allowing developers to abstract away the details of the individual components of an application. Dynamic software architectures are those that change their structure and enact the modifications during the system’s execution [10]. In the last years several architecture description languages (ADL) have been proposed to provide behavioral descriptions of the components and connectors [10]. However, to support the development of robust and correct architectures a variety of formal approaches have been introduces (see [11, 3, 6] among others). The importance of having a formal basis for the design of system architectures is underlined in the survey [1]. 88 M. Cavaliere, V. Deufemia Besides the possibility of analyzing software architecture properties rigorously (like for instance, deadlock freeness), the formalisms for specifying software architectures are particularly useful for the description of dynamic software systems since their development is “challenging in terms of correctness, robustness, and efficiency” [19]. Indeed, the possibility of instantiating and removing components at run-time makes dynamic software architectures hard to model and analyze since they may have infinite different configurations. Here, we propose to formally define (dynamic) software architectures in terms of membrane systems, that are parallel and distributed computational devices inspired by the structure and by the working of living cells. For an introduction to this topic, the reader can consult [14] or the guide [15]. The updated literature on this field can be found in the web page [21]. Some similarities with our approach can be found with the approach proposed in [8] where a language based on chemical reactions have been used to formally describe a software system. On the other hand in the approach presented here we introduce many operations typical of the functioning of living cells, that, up to our knowledge, have not been used so far in software system modelling. The underlying idea of our approach is to represent a certain software architecture by means of a membrane system. Each region of the membrane system represents an abstract component of the software system, with a certain type (indicated by a label taken in a certain alphabet) that defines certain associated rules (operations), used to evolve and to move objects (data). Objects can also have different types (indicated by different symbols of an alphabet) and each occurrence of an object can be involved in certain rules, depending on its type. The objects have also associated information about the membranes they cross during their movements. All the objects (data) are processed and moved in a parallel way. In this way, the evolution of a membrane system can describe the evolution of a software architecture. Therefore by investigating the representing membrane system, it is possible to formally verify the properties of the modelled software architecture. 2 Preliminaries: Membrane Systems Membrane systems (also referred to as P systems) are a class of parallel and distributed computing devices inspired from the structure and the functioning of living cells. The basic model considers a membrane structure, consisting of several cell-like membranes which are hierarchically embedded in a main membrane, called the skin membrane. The membrane delimits regions, where are placed occurrences of objects representing chemicals. The occurrences of the objects evolve according to given evolution rules, representing the chemical reactions, that are associated to the regions; here we also associate labels to the membranes and we consider rules that can change the membrane structure (in other words, the membranes are considered as active elements). Specifying Dynamic Software Architectures by Using Membrane Systems 89 It is also possible to associate rules to the membranes that move the objects from a region to another one (symport/antiport rules). As a general idea, a single step of the evolution of a P system is done by applying, in a non-deterministic maximally parallel manner, the rules associated to the regions and to the membranes of the system. The evolution of the P system halts when no further rule can be applied to the occurrences of objects and to membranes. A more formal definition of the evolution will be specified later when a specific model of membrane computing will be introduced. The membrane system model used in this paper is a compound of many (generalized) features taken from the membrane systems area. To give a reference to the current literature, the model used here is a kind of evolution-communication model (where evolution rules, together with symport/antiport rules are present) extended with rules of membrane systems using active membranes. The evolution-communication model has been originally introduced in [4], while membrane systems using active membranes have been investigated in several papers (for instance, [12, 13]). In this paper, we are mainly interested in the dynamics of a membrane system, not in its computational power, and then, we will not specify the output region of the system, contrarily to what is usually done in the membrane computing area. In this paper we introduce a feature that is not present in any of the membrane models considered up to this moment and that seems necessary for software system modelling, i.e. the association of a unique identifier to each membrane. Notice that such an identifier differs from the label of the membrane that indicates the type of the membrane; while several membranes can have the same label (i.e., can have the same type), the identifier of a membrane is unique (i.e., can be imagined as an integer number) and different membranes (even with the same label) have different identifiers; the identifier is associated to a membrane when the membrane is created. Because our goal is to model software systems, we can suppose to take a set of identifiers (ID), large “enough”, to be “compatible” with the physical limits (for instance, memory limits) of the software system we plan to model. In the membrane model defined here, also the occurrences of objects make use of the mentioned identifiers. In fact, each object present in the regions of the membrane system is associated with a string (possibly empty) composed of some of the identifiers of the membranes present in the current configuration. This string is used to keep trace, during the evolution of the system, of the membranes visited by the object occurrence. The rules that move and manipulate the objects can also update the string of identifiers associated to such objects, in a specified way. Some of the rules may be active only when a specified boolean predicate defined over the identifiers is true. To make more readable the formal definition given later, we introduce some basic operations involving identifiers and strings of identifiers. The hierarchical structure of a P system can be represented by a string of correctly matching parentheses; there is an unique external pair of parentheses representing the skin 90 M. Cavaliere, V. Deufemia membrane. We can represent a configuration of a P system adding to such string of parentheses the contents of the regions in form of strings representing multisets. Given a string µrepresenting a configuration of a P system, then µ(i) denotes the ith membrane of µ(i.e., the ith open parenthesis [ ), reading µas a string, from left to right; µ(i).id denotes the identifier associated to the ith membrane present in µ. As already mentioned, each membrane of a system has associated a unique identifier. For instance, given µ= [h1ab[h2c[h1a]h1b]h2]h1, then µ(3).id denotes the identifier associated to the innermost membrane (as mentioned above, to each object occurrence is associated a string of identifiers and such string may even be empty); given a multiset of objects, described by a string m,m(i) denotes the i object occurrence present in the multiset, reading the string mlike a string, from left to right; m(i).list denotes the string of identifiers associated to the ith object occurrence present in the multiset m. For instance, given the multiset m=aabcc, then m(4).list denotes the string of identifiers associated to the first occurrence of c, reading the string mfrom left to right. Given a string of identifiers list, we denote by list−the new string of identifiers obtained by removing the rightmost symbol from the string list; the addition of a symbol to a string of identifiers is done by using the standard string concatenation, indicated here by + to avoid confusions. Given a string of identifiers list, then last(list) denotes the rightmost symbol (then the rightmost identifier) of the string. As the reader can see, the string of identifiers is actually used like a stack, and this is enough for our goal, due to the hierarchical structure of a membrane system. The other operations involving a string of identifiers will be not formally defined, since their meaning is rather intuitive. Moreover boolean predicates over the set of identifiers will also be used. The definition of the model used here as follows. Definition 1. An evolution-communication P system with active membranes (in short, an ECam P system), of degree m≥1, is defined as Π= (O, H, ID, µ, w1, w2, . . . , wm, R), where: •Ois the alphabet of Π; its elements are called objects; to each occurrence of an object present in the system is associated a string (possibly empty) over the alphabet ID; •His a finite set of labels for membranes; •ID is the set of identifiers; at any time, each membrane of the system has associated, in a unique way, one of the identifiers present in ID; as a general assumption we suppose that the set ID is finite but large enough to identify, at any time, all the membranes present in the system; •µis a membrane structure consisting of mmembranes labelled with elements in H, not necessarily in a one-to-one manner; Specifying Dynamic Software Architectures by Using Membrane Systems 91 •wi,1≤i≤m, specifies the multiset of objects present in the corresponding region iwhen the system is created; to each occurrence of an object is associated an empty string of identifiers; if an object has an unbounded number of occurrences, then we indicate it by using the index ∞; •Ris a set of developmental rules, of the following forms: (a) : [hu→v]hor [h1[h2u→v]h2]h1, for h, h1, h2∈H, u ∈O+, v ∈O+, with |u| ≥ |v|; object evolution rules, associated with membranes and depending on the label of the membrane (or on the labels of the membranes in the second case) but not involving the membranes, in the sense that the membranes are neither taking part in the application of these rules nor modified by them; the objects present in the multiset uare rewritten into the objects described by the multiset v; each object occurrence in vis associated with a string of identifiers chosen as one of the strings of identifiers associated to the object occurrences present in u; formally, if |u|=m, and |v|=n, then we set v(j).list =u(i).list, for 1≤i≤m, 1≤j≤n; (b) : (µ1= [h1u[h2v]h2]h1→µ2= [h1v0[h2u0]h2]h1, c)h1, h2∈H, u ∈O+, v ∈ O+; antiport rules, that realize a synchronized exchange of objects; they are associated with membranes and depend on the labels of the membranes but do not change the membranes; the objects in u0and v0are exactly the objects in uand v, respectively (the objects are only moved), except for the associate strings of identifiers, updated in the following manner. Suppose |v0|=|v|=n; then for 1≤i≤n, we set v0(i).list =½v(i).list−if last(v(i).list) = µ1(1).id, v(i).list +µ1(2).id if last(v(i).list)6=µ1(1).id. The identifiers associated to the objects in u0are updated in a symmetric way. Suppose |u0|=|u|=m, then, for 1≤i≤n, we set u0(i).list =½u(i).list−if last(u(i).list) = µ1(2).id, u(i).list +µ1(1).id if last(u(i).list)6=µ1(2).id. The idea that leads the update of the strings of identifiers is the following one. If an object enters exactly the membrane whose identifier is the last one inserted in the associated string of identifiers then the last identifier is removed (because the object is coming back in “its” region); if this is not the case, then the identifier of the membrane that the object is leaving, is added to the string of identifiers; cis a boolean predicate over the set of identifiers; if it is specified, then the rule is active, if and only if, the boolean predicate is true; (c) : (µ1= [h1[h2u]h2]h1→µ2= [h1[h2]h2u0]h1, c) (µ1= [h1u[h2]h2]h1→µ2= [h1[h2u0]h2]h1, c),for h1, h2∈H, u ∈O+; symport rules, that move objects from inside to outside a membrane, or viceversa; they are associated to the membranes and depend on the labels but do not involve any change on the membranes; the objects in u0are exactly the same 92 M. Cavaliere, V. Deufemia in u(the objects are only moved), except their associated strings of identifiers updated in the following way. Suppose |u0|=|u|=n; then, for any 1≤i≤n, we set, in the first case, u0(i).list =½u(i).list−if last(u(i).list) = µ1(1).id, u(i).list +µ1(2).id if last(u(i).list)6=µ1(1).id. In the second case, u0(i).list =½u(i).list−if last(u(i).list) = µ1(2).id, u(i).list +µ1(1).id if last(u(i).list)6=µ1(2).id. The string of identifiers associated to the objects in u0are updated like in the case of antiport rules described above; if the boolean predicate cis specified, then the rule is active, if and only if, the specified predicate is true; (d) : [iu]i→[iv[hw]h]i, h, i ∈H, w, u, v ∈O+,|u| ≥ |v|+|w|; creation rules; in reaction with some specified objects present in membrane i, a new membrane with label his created inside the one with membrane i, and having inside the objects specified by w; the strings of identifiers, associated to the objects in ware the empty strings; to the new created membrane is associated a certain identifier from the set ID, not assigned to any membrane currently present in the membrane system; the objects present in uare possibly changed and the strings of identifiers for the objects in vare fixed like in the case of the object evolution rule u→v; (e) : [h1u]h1[h2u0]h2→[h2[h1v]h1v0]h2,|u|+|u0|≥|v|+|v0|; endocytosis; an elementary membrane labelled h1enters the adjacent membrane labelled h2that can be non-elementary, under the control of the objects in u,u0and labels h1, h2; the labels of the two membranes remain unchanged; the objects in uand u0are possibly changed; the strings of identifiers of the objects in vand v0are fixed like in the case of the objects evolution rules, u→vand u0→v0, respectively; all the remaining objects present in membrane h1and h2 as well their strings of identifiers are left unchanged in the same membrane; (f) : [h2[h1u]h1u0]h2→[h1v]h1[h2v0]h2,|u|+|u0| ≥ |v|+|v0|; exocytosis; an elementary membrane labelled h1is sent out of a membrane labelled h2, under the control of the objects in uand u0and the labels h1, h2; the labels of the two membranes remain unchanged; the objects in uand u0are possibly changed; the strings of identifiers of the objects in vand v0are fixed like in the case of objects evolution rules, u→vand u0→v0, respectively; all the remaining objects present in membrane h1and h2as well their strings of identifiers are left unchanged in the same membrane. The evolution of the membrane system is defined in the following way. It starts from an initial configuration represented by the initial membrane structure µand the multiset of objects available in its compartments at the beginning, hence (µ, w1, w2,· · · , wm). Some of the objects, in some of the regions, can be present in Specifying Dynamic Software Architectures by Using Membrane Systems 93 an unbounded number of occurrences. As mentioned, to each membrane is associated a unique identifier taken from the set of identifiers; such set is finite but we suppose is big enough to contain an unique identifier for each membrane present in the configuration of the system, during any possible computation; this assumption is justified by the fact that the number of membranes that can be created is bounded by the physical resources of the software system we are modelling. To each object present in the regions of the membrane system is associated a string of identifiers (initially empty) updated during the evolution of the system in the way specified by the rules. A single step of the evolution of the membrane system is composed by two sub-steps, applied one after the other one. In the first sub-step, the rules of type (a), (b), (c) are used in a non-deterministic maximally parallel manner. The non-deterministic maximally parallel manner means that we assign the object occurrences to the rules, non-deterministically choosing the rules and the objects, until no further assignments is possible. These rules realize the evolution of the objects by using the objects evolution rules and the movement of the objects by using the symport/antiport rules. Each object occurrence can be used by only one of these rules. The strings of identifiers associated to the objects involved are updated as specified by the rules. The symport/antiport rules are active only for the membranes where the boolean predicate, if any, specified by c, is true. In the second sub-step, the rules of type (d)-(f), are used, still in a maximally parallel non-deterministic way. These rules modify the membrane structure of the membrane system. Each object occurrence and each membrane can be involved in only one of these rules. Also in this case, the strings of identifiers associated to the involved objects are updated in the way specified by the rules. Notice that never during the entire evolution new object occurrences are created; they are only transformed. The evolution of the membrane system halts when the system reaches a halting configuration, that is a configuration where no rules can be further applied. On the other hand, there might be membrane systems whose evolution can run forever. 3 Membrane Systems as Dynamic Software Architectures Specifications In this section, first we show how membrane systems can be used to formally specify static architectures: the number and type of components and connections do not change. Successively, we address the problem of capturing dynamic architectures: systems for which composition of interacting components changes during the course of a single evolution. A software architecture specification describes the high-level design of a system in terms of the structure of the components and their communication relationships. 94 M. Cavaliere, V. Deufemia Thus, the specification focuses on the interaction behaviors exhibited by the components, not on the algorithms used internally by the components to carry out their functional roles. The idea of the proposed approach is to describe the components (or entities) of the system, which can be classes, procedures, processes, etc., with the membranes of the membrane system, which evolve and communicate according to the rules associated to them. In particular, the membrane systems description of a static software architecture consists of the mentioned hierarchical structure of membranes where: 1. the associated multisets of objects (abstract data) and the associated set of evolution rules (abstract manipulation of data) represent the static components of the architecture, 2. the associated sets of symport/antiport rules represent the connectors of the architecture. For instance, consider the simple client-server system shown in Fig. 1(a). It consists of one client and one server interacting via a link. This system is described by the membrane system graphically depicted in Fig. 1(b). In particular, to each entity of the system corresponds a membrane, and the communication between these membranes is accomplished by antiport rules of the type [server r2[client r1 ]client ]server →[server r1[client r2]client ]server (shown in Fig. 1(b) with an arrow), which describe the request r1sent by the client to the server, and the response r2sent by the server to the client. The client membrane has also associated a multiset of objects representing its internal state, and a set of evolution rules that evolve the objects according to the requests made to the server and the responses received. As an example, when the previous antiport rule is applied, the object r2will activate some rules in the client membrane that evolve its internal state. Moreover, some of the evolution rules can be executed only if the client membrane is inside the server one, that is the rules are of the form [server [client a→b]client ]server. Client Server client server (a) (b) Fig. 1. A simple client-server system (a) and the membrane system modelling it (b). Now, let us consider a client-server system that changes the configuration during the evolution. As an example, suppose that the system has two servers: a Specifying Dynamic Software Architectures by Using Membrane Systems 95 primary server that provides many services, but it may go down suddenly, and a secondary server that provides less services, but it is reliable. Thus, a client interacts with a primary server and if, and only if, the primary server fails then it would start to interact with the secondary one, as shown in Fig. 2(a) and 2(b). Client Primary Client SecondarySecondary Primary (a) (b) Fig. 2. A dynamic client-server system. These dynamic aspects are supported by the membrane systems through the active membrane rules, which represent reconfiguration of the membrane structure. The behavior of the previous client-server system can be described by the membrane system graphically depicted in Fig. 3. Here new membranes representing the clients can be created in the environment by using creation rules, and can enter into the primary server membrane by using the endocytosis rule [client ]client [primaryu]primary →[primaryu[client ]client]primary if and only if the state of the primary server is up (i.e., it contains the object u) as in Fig. 3(a). In the case the primary server goes down, its state changes from uto dand the secondary server is activated by setting its state to up. Moreover, the client membrane leaves the primary server by using the exocytosis rule [primary d[client ]client]primary→[client ]client [primary d]primary, and enters into the secondary server by executing the endocytosis rule [client ]client [secondary u]secondary →[secondary u[client ]client]secondary, as shown in Fig. 3(b). The exclusive access to the two servers for the clients is guaranteed by the following endocytosis and exocytosis rules: [primary u]primary [secondary u]secondary → [primary [secondary d]secondary u]primary [primary [secondary d]secondary u]primary → [primary u]primary [secondary d]secondary [primary [secondary d]secondary d]primary → [primary d]primary [secondary u]secondary [primary d]primary [secondary d]secondary → [primary [secondary u]secondary d]primary [primary [secondary u]secondary d]primary → [primary d]primary [secondary u]secondary [primary [secondary u]secondary u]primary → [primary u]primary [secondary d]secondary 102 M. Cavaliere, V. Deufemia where SEQΠis the set of all possible sequences of configurations during any computation (halting or non halting) of the system Π. Notice that Bobs(Π) is a language consisting of finite and infinite words over the alphabet Σ. Simply by intersecting Bobs(Π) with a regular language we can select finite behavior Bfin obs (Π) and infinite behavior Binf obs (Π). Formally: Bfin obs (Π) = Bobs(Π)∩Σ∗, Binf obs (Π) = Bobs(Π)∩Σω. The partition obs plays the role of an observer of the system Π: it groups, in a specified way, the configurations of the system Π. The defined languages may be too complex to be investigated. In fact, it is known, that, for every recursively enumerable language Lis possible to construct a (simple) system Π, a partition obs such that Bfin obs (Π) = L(for details we refer to [5]). Therefore, it seems necessary to find two languages, b Bobs fin(Π) and b Bobs inf (Π) that are “approximations” of the behaviors Bfin obs (Π) and Binf obs (Π). The definition of approximation is not formally given here and is left for the future work. For our goal here is enough to have the intuitive idea that, given a language L, then the language b Lapproximates Lif L⊆b L. Of course, a rather trivial approximation of any language Lover an alphabet Σis the language Σ∗. But intuitively this approximation is “too far” from Lbecause it loses every information on the original language. Therefore the problem is to find good approximations, meaning with that a language easy to analyze but not too far from the original language. Coming back to our goal, given a behavior B(infinite or finite), we need to find a behavior b Bthat is an approximation of B. A possible approximation of a behavior is called automata approximation and it is constructed in the following way. Given a P system Πand a partition obs =CΠ1∪CΠ2· · · ∪ CΠkof the set CΠ, we construct a finite state automaton A0= (K, V, s0, δ, F) in the following way. Each state in Kcorresponds in a unique way to one of the subset composing obs. The input alphabet Vcoincides with the set of states. The initial state s0 corresponds to the subset in obs having the initial configuration of Π. The set f of states corresponds to the subsets of obs containing a halting configuration. The transition δis fixed in the following way. δ(CΠi, CΠj) = CΠj,1≤i, j ≤k, if and only if, the system Πcan move, in one step of evolution, from a configuration present in CΠito a configuration present in CΠj. In similar way we can construct a B¨uchi automaton A00, except that in this case the set of final states Fcoincides with K. It is clear that Bfin obs (Π)⊆L(A0) and Binf obs (Π)⊆L(A00) (so L(A0) and L(A00) are approximations of Bfin obs (Π) and Binf obs (Π), respectively). Specifying Dynamic Software Architectures by Using Membrane Systems 103 Notice that the procedure given may be not effective. For this reason we say that a behavior can be automata approximated if and only if the automaton defined earlier can be effectively constructed. Moreover, a system Πcan be automata approximated if, and only if, its behavior can be automata approximated. If the system Πhas a finite number of configurations (i.e., the cardinality of CΠis finite), then the system can be automata approximated by using the trivial partition obstotal constructed by just considering each configuration in CΠas a unitary set of the partition obstotal. Actually, in this trivial case we do not have an approximation but actually the equality Bfin obstotal (Π) = L(A0) and Binf obstotal (Π) = L(A00). Find good approximations for complicate behaviors is a rather challenging topic, with several possible implications in different fields. On the other hand, it is also interesting to individuate classes of systems that can be automata approximated when using specified observers. These two problems are left as open problems for further investigations. We conclude by showing that it is possible to construct an observer obs such that the system defined in Section 4 can be automata approximated and is possible to investigate properties of the system by using such an approximation. Informally, to construct the observer of the system, one needs to fix the components of the system that have to be investigated. For instance, in our case, one of the components of the system that may be interesting to study is the patient. Initially we individuate the states of the patient which we consider interesting for our investigation. For instance, these might correspond to: patient with some symptoms, recovered in the hospital but not yet visited by a doctor;patient visited by the doctor;patient under treatment;patient that is taking medicine;patient restored. Now, suppose that in the original configuration of the system Π, there exists a patient represented by a membrane with label patient and with identifier id. Then, it is possible to partition the set of all reachable configurations CΠ according to the states of such specified patient. In particular, we can construct the partition of CΠ,obspatient =C1∪C2∪C3∪ C4∪C5, where: C1={c|the membrane with identifier id contains the occurrence sd,d∈ {1,· · · , m}}. This set contains all the configurations in CΠwhere the specified patient has certain symptoms (indicated by s) but has not yet been visited by the doctor. C2={c|the membrane with identifier id contains two occurrences of xband the membrane is inside a membrane with label doctor,b∈ {1,· · · , l}}. This set contains all the configurations in CΠwhere the specified patient has been visited by the doctor; xbindicates the health state associated by the doctor to the patient, according to the symptoms. 104 M. Cavaliere, V. Deufemia C3={c|the membrane with identifier id contains two occurrences of xb, the membrane is inside a membrane with label nurse and xbis not a restored health state, b∈ {1,· · · , l}}. This set contains all the configurations in CΠwhere the patient is under treatment (it is associated to a nurse); xbindicates the current health state of the patient. C4={c|the membrane with identifier id contains an occurrence of ma, a ∈ {1,· · · k}}. This set contains all the configurations where the patient is taking a medicine; maidentifies the medicine. C5={c|the membrane with identifier id contains an occurrence of xband xb is a restored health state, b∈ {1,· · · , l}}. This set contains all the configurations in CΠwhere the patient has been restored; xbindicates a restored health state. It is possible to see that obspatient is a partition of CΠ. We are interested in Binf obspatient (Π). Looking at the P system Πdescribed in Section 4 we can construct the finite state automata that approximate Binf obspatient (Π), in the way previously described. In particular, looking to the rules of Πand following the procedure given earlier is possible to construct the B¨uchi automaton represented in Fig. 6. The language accepted by this automaton is exactly Binf obspatient (Π). C1C2 C5 C3 C4 C2 C3 C4 C5 C2 C3 Fig. 6. The automaton for Binf obspatient (Π). The automaton can be used to prove properties of the constructed system Π. For instance, using the automaton it is possible to infer two important properties of the system: the patient cannot take a medicine if s/he is not under treatment because all the paths from state C1to state C4pass through state C3; moreover, is also true that a patient cannot be under treatment if it has not been visited by a doctor (in fact, the state C3in the automaton can be reached only passing through the state C2). We can also see that the patient evolves in a deterministic way, that means given a state (among the ones investigated), there is an unique possible next state (among the ones investigated), except for the state C4; in this case, in fact, the Specifying Dynamic Software Architectures by Using Membrane Systems 105 patient can either be restored (state C5) or can remain under treatment (state C3). It is possible to construct several automata, for each possible component we are interested. For instance, it is possible to investigate the behavior of a nurse and of a doctor by using the same approach used for a patient. Moreover it is also possible to investigate properties concerning the entire system and the interactions between the different components by using the cross-product operation, [17], among the realized automata. On the other hand, the entire problem of approximation can be formally investigated in the framework of rough sets theory dedicated to the formal study of approximation, [16]. We leave these interesting topics for further works. References 1. R. Allen, D. Garlan: A formal basis for architectural connection. ACM Transactions on Software Engineering and Methodology, 6, 3 (1997), 213–249. 2. J. Berstel, J.E. Pin: Infinite Words. Elsevier, Amsterdam, 2004. 3. N. Carriero, D. Gelerntern: Linda in context. Communications of the ACM, 32, 4 (1989), 444–458. 4. M. Cavaliere: Evolution–communication P systems. In Membrane Computing (Gh. P˘aun, G. Rozenberg, A. Salomaa, C. Zandron, eds.), LNCS 2597, Springer-Verlag, Berlin, 2003, 134–145. 5. M. Cavaliere, P. Leupold: Evolution and observation – A new way to look at membrane systems. In Membrane Computing (C. Mart´ın-Vide, G. Mauri, Gh. P˘aun, G. Rozenberg, A. Salomaa, eds.), LNCS 2933, Springer-Verlag, Berlin, 2004, 70–88. 6. A.A. Holzbacher: A software environment for concurrent coordinated programming. Proc. First International Conference Coordination Models, Languages and Applications, LNCS 1061, Springer-Verlag, Berlin, 1996, 249–266. 7. J.E. Hopcroft, J.D. Ullman: Introduction to Automata Theory, Languages, and Computation. Addison-Wesley, 1979. 8. P. Inverardi, A.L. Wolf: Formal specification and analysis of software architecture using the chemical abstract machine model, IEEE Transactions On Software Engineering, 21, 4 (1995), 373–386. 9. J. Kramer: Configuration programming. A framework for the development of distributable systems. Proc. COMPEURO ’90, IEEE, 1990, 374–384. 10. N. Medvidovic, R.N. Taylor: A classification and comparison framework for software architecture description languages. IEEE Trans. on Software Engineering, 26, 1 (2000), 70–93. 11. D. Le M´etayer: Describing software architecture styles using graph grammars. IEEE Transactions on Software Engineering, 24, 7 (1998), 521–533. 12. Gh. P˘aun: Computing with membranes: Attacking NP-complete problems. In Unconventional Models of Computation (I. Antoniou, C.S. Calude, M.J. Dinneen eds.), Springer-Verlag, London, 2000, 94–115. 13. Gh. P˘aun: P systems with active membranes: Attacking NP-complete problems. Journal of Automata, Languages and Combinatorics, 6, 1 (2001), 75–90. 14. Gh. P˘aun: Membrane Computing. An Introduction. Springer-Verlag, Berlin, 2002. 106 M. Cavaliere, V. Deufemia 15. Gh. P˘aun, G. Rozenberg: A guide To membrane computing. Theoretical Computer Science, 287, 1 (2002), 73–100. 16. Z. Pawlak: Rough sets. International Journal of Computer and Information Sciences, 11 (1981), 341–356. 17. G. Rozenberg, A. Salomaa, eds.: Handbook of Formal Languages. Springer-Verlag, Berlin, 1997. 18. D. Soni, R.L. Nord, C. Hofmeister: Software architecture in industrial applications. Proc. of the Int. Conf. on Software Engineering, 1995, 196–207. 19. C. Szyperski: Component technology: What, where, and how? Proc. of the Int. Conf. on Software Engineering, 2003, 684–693. 20. M. Wermelinger: Towards a chemical model for software architecture reconfiguration. IEE Proceedings - Software, 145, 5 (1998), 130–136. 21. The P Systems Web Page: http://psystems.disco.unimib.it