197,735 research outputs found
Modeling adaptation with a tuple-based coordination language
No full textIn recent years, it has been argued that systems and applications, in order to deal with their increasing complexity, should be able to adapt their behavior according to new requirements or environment conditions. In this paper, we present a preliminary investigation aiming at studying how coordination languages and formal methods can contribute to a better understanding, implementation and usage of the mechanisms and techniques for adaptation currently proposed in the literature. Our study relies on the formal coordination language Klaim as a common framework for modeling some adaptation techniques, namely the MAPE-K loop, aspect- and context-oriented programming
Modeling Adaptation with Klaim
No full textIn recent years, it has been argued that systems and applications, in order to deal with their increasing complexity, should be able to adapt their behavior according to new requirements or environment conditions. In this paper, we present an investigation aiming at studying how coordination languages and formal methods can contribute to a better understanding, implementation and use of the mechanisms and techniques for adaptation currently proposed in the literature. Our study relies on the formal coordination language Klaim as a common framework for modeling some well-known adaptation techniques: the IBM MAPE-K loop, the Accord component-based framework for architectural adaptation, and the aspect- and context-oriented programming paradigms. We illustrate our approach through a simple example concerning a data repository equipped with an automated cache mechanism
Onychiuridae Fanciulli, Loreti & Dallai, 2010, sp. nov
No full textFamily Onychiuridae Deuteraphorura caprelleana sp. nov . Figs 1–13, Tab. 1 –3 Type locality. Italy, Caprelle cave (41 MA/MC; Coord gauss-boaga 2355275–4777580), 880 m a.s.l. in the karstic plain of Mount Lago of Sefro-Pioraco (Province of Macerata). Type material. Holotype (female) and 3 paratypes (females), Caprelle cave (41 MA/MC; Coord gaussboaga 2355275–4777580), (June 2007, leg. Loreti M.). All types deposited in Collembola collection, Department of Evolutionary Biology, University of Siena. Description. Body length 2.4–2.6 mm, cylindrical in shape with uniform cuticle granulation. Colour white in alcohol. Length of Ant. I, II, III and IV as 57, 105, 120 and 160 µm. Ratio antennae/head diagonal = 0.86. Antennal base well marked. Ant. IV with subapical organite and microsensillum at its base in latero-external position (Fig. 9); some sensilla not well distinguishable from ordinary chaetae. Ant. segments I, II and III with 8, 14 and 18 chaetae respectively (Fig. 9). Antennal III sense organ as in Fig. 10, consisting of five papillae, two sensory rods, two ribbed sensory clubs, five guard chaetae and microsensillum (Fig. 10). PAO consisting of 19–21 compound vesicles disposed in two parallel rows (Fig. 11). Labrum as in Fig. 7 with 5,4, 2 chaetae, chaetotaxy of the labium (submentum) with 4 + 4 chaeta (Fig. 4), basolateral field (mentum) with 5 chaetae (Fig. 4); outer maxillary lobe with one basal chaeta and two sublobal hairs (Fig. 5). Labial palp of type AB (Fjellberg 1999) with six proximal chaetae; labial papillae A, B, C, D and E with 1, 4, 0, 3 and 3 guard chaetae respectively (Fig. 6). Mandible with four apical teeth as in Fig. 12; maxillary head as in Fig. 13. VT with 7–8 + 7–8 apical chaetae, without basal chaetae. Body chaetotaxy made of mesochaetae, macrochaetae and lateral microsensilla on thoracic terga II and III. Chaetotaxy type and distribution of dorsal chaetae as in Fig. 1 and Tables 1 –3, sometimes extra chaetae and asymmetries have been observed. Abdominal terga IV and VI with chaeta p0. Ratio chaetae M/s = 2.2 on abdominal tergum V. Thoracic sterna without chaetae along linea ventralis; ventral chaetotaxy of abdomen and head as in Figs 2 and 3 respectively. Furca reduced to finely granulated area with 2 + 2 chaetae disposed in one row; female genital area with 17–20 chaetae. Tibiotarsi I, II, and III with 18, 18 and 17 chaetae respectively; distal whorl with 9 chaetae. Claw without inner tooth, small outer tooth present; empodial appendage slender, reaching about 80 % of the inner edge, without basal lamella (Fig. 8). d m0, m 1, m 2, m 3, m 4 sd m 1, m 2, m 3, m 3 ’, m 4, M 5, sd’ m 1, m 3, m 5 v m 1, m 2, m 3, M 4 ca m 5, cm m 3, m 4 cb m 1, m 3, m 5, m 6 cp m 1, m 4, m 6 p m 2, m 3, m 4, m 5, m 6 g 11 chaeta m: micro-mesochaetae; M: macrochaetae. row Thorax I Thorax II Thorax III a m 2, m 4, m 6 m 2, m 3, m 4, m 5, m 6, M 7 m 2, m 3, m 4, m 5, m 6, M 7 m M 1, m 2, m 3, m 4, M 5, m 6?, M 7 m 1, M 2, m 3, m 4, m 5, m 6, M 7, M 8 ca m 3, m 5 m 4, m 5 cp m 1, m 2, m 4, M 6 m 1, m 2, m 4, m 6 p M 1, m 2, m 3, m 4, M 5, m 6, m 7, M 8 m 1, m 2, M 3, m 4, M 5, m 6, m 7, M 8 m 1, m 2, M 3, m 4, M 5, m 6, M 7, M8 m: micro-mesochaetae; M: macrochaetae. Dorsal pseudocellar formula: 32 /033/ 33354. Ventral pseudocellar formula: 3 /011/ 3212. Holotype with 1, 1 and 2 pseudocelli on subcoxae 1 of I, II and III pairs of leg; in the paratypes subcoxa 1 of I, II and II pairs of leg with two pseudocelli each; all femura with one ventral parapseudocellus; not well visible in other parts of the body. Etymology. The species name is derived from the name of the cave in which it was found. Discussion. Some Deuteraphorura species: D. ghidinii (Denis, 1938), D. pseudoghidinii (Dallai, 1969), D. handschini (Denis, 1924), D. hussoni (Denis, 1935) share the same formula of dorsal pseudocelli as the new species. However, all of them differ from the new species for the different ventral formula that is 3 /011/ 3212 in D. caprelleana sp. nov. while it is 2 /011/ 2212 in D. ghidinii, 2 /011/ 3111 in D. handschini, and 2 /011/ 2111 in D. hussoni and 3 /011/ 2212 in D. pseudoghidinii. On the contrary, there are some species of Deuteraphorura with the same ventral formula as in the new species (3 /011/ 3212) but differ for the dorsal formula. Among these D. cebennaria (Gisin, 1956) (32 / 133 / 33354), D. frasassii Fanciulli, 1999 (32 /033/ 33353), D. gemae (Simon & Luciáñez, 1994) (32 / 133 / 33353), D. nevoi (Gruia, Poliakov & Broza, 2000) (32 / 122 / 33343). Based on the pseudocellar formula, the new species appears very closely related to D. pseudoghidinii and D. frasassii. TABLE 3. Deuteraphorura caprelleana sp. nov. Chaetotaxy of the abdominal tergites. row Abdomen I Abdomen II Abdomen III a m 5, m 6, m 7, M 8 m 5, m 6, m 7 m 3, m 4, m 6, m m 1, M 2, m 4, m 6, m 7, M 7, M 8 m 1, M 2, m 4,, m 6, M 7, M 8 m 1, M 2, m 4, m 6, M 7, M 8 ca m 1, m 4, m 5 m 1, m 4,m 5 m 1, m 4,m 5 p m 1, m 2, m 3, M 4, m 5, m 6, m 7, M 8 m 1, m 2, m 3, M 4, m 5, m 6, M 7, M 8 m 1, m 2, m 3, M 4, m 5, m 6, M 7, M 8 continued. row Abdomen IV Abdomen V Abdomen VI a m 2, m 3, m 4, m 5, m 6, m7 m m 1, M 2, m 3,, m 5, m 6, M 7 m 2, m 3, m 4, m 5, M 7 m 1 ca m 1, m 3, m 4, m 5, m 6, m 7 m 3, m 4 cp m 5, m 6 p m0, m 1, m 2, M 5, m 6, m 7, M 8 m 1, M 2, m 3 s’, M 5, m 6, M 7 M0, m 1, M 2, m 3, M 4 m: micro-mesochaetae; M: macrochaetae.Published as part of Fanciulli, Pietro Paolo, Loreti, Mara & Dallai, Romano, 2010, A new cave species of Deuteraphorura (Collembola: Onychiuridae) and redescription of four species of the genus from Italy, pp. 34-54 in Zootaxa 2609 on pages 35-38, DOI: 10.5281/zenodo.19777
Uniform Labeled Transition Systems for Nondeterministic, Probabilistic, and Stochastic Processes
No full textRate transition systems (RTS) are a special kind of transition systems introduced for defining the stochastic behavior of processes and for associating continuous-time Markov chains with process terms. The transition relation assigns to each process, for each action, the set of possible futures paired with a measure indicating the rates at which they are reached. RTS have been shown to be a uniform model for providing an operational semantics to many stochastic process algebras. In this paper, we define Uniform Labeled TRAnsition Systems (ULTraS) as a generalization of RTS that can be exploited to uniformly describe also nondeterministic and probabilistic variants of process algebras. We then present a general notion of behavioral relation for ULTraS that can be instantiated to capture bisimulation and trace equivalences for fully nondeterministic, fully probabilistic, and fully stochastic processes
Implementing Session Centered Calculi
No full textRecently, specific attention has been devoted to the development of service oriented process calculi. Besides the foundational aspects, it is also interesting to have prototype implementations for them in order to assess usability and to minimize the gap between theory and practice. Typically, these implementations are done in Java taking advantage of its mechanisms supporting network applications. However, most of the recurrent features of service oriented applications are re-implemented from scratch. In this paper we show how to implement a service oriented calculus, CaSPiS (Calculus of Services with Pipelines and Sessions) using the Java framework IMC, where recurrent mechanisms for network applications are already provided. By using the session oriented and pattern matching communication mechanisms provided by IMC, it is relatively simple to implement in Java all CaSPiS abstractions and thus to easily write the implementation in Java of a CaSPiS process
Towards a Formal Verification Methodology for Collective Robotic Systems
No full textWe introduce a UML-based notation for graphically modeling
systems’ security aspects in a simple and intuitive
way and a model-driven process that transforms graphical
specifications of access control policies in XACML. These
XACML policies are then translated in FACPL, a policy
language with a formal semantics, and the resulting policies
are evaluated by means of a Java-based software tool
A SPATIAL LOGIC FOR SIMPLICIAL MODELS
No full textCollective Adaptive Systems often consist of many heterogeneous components typically organised in groups. These entities interact with each other by adapting their behaviour to pursue individual or collective goals. In these systems, the distribution of these entities determines a space that can be either physical or logical. The former is defined in terms of a physical relation among components. The latter depends on logical relations, such as being part of the same group. In this context, specification and verification of spatial properties play a fundamental role in supporting the design of systems and predicting their behaviour. For this reason, different tools and techniques have been proposed to specify and verify the properties of space, mainly described as graphs. Therefore, the approaches generally use model spatial relations to describe a form of proximity among pairs of entities. Unfortunately, these graph-based models do not permit considering relations among more than two entities that may arise when one is interested in describing aspects of space by involving interactions among groups of entities. In this work, we propose a spatial logic interpreted on simplicial complexes. These are topological objects, able to represent surfaces and volumes efficiently that generalise graphs with higher-order edges. We discuss how the satisfaction of logical formulas can be verified by a correct and complete model checking algorithm, which is linear to the dimension of the simplicial complex and logical formula. The expressiveness of the proposed logic is studied in terms of the spatial variants of classical bisimulation and branching bisimulation relations defined over simplicial complexes
Topology of univoque sets in real base expansions
No full textGiven a positive integer M and a real number q∈(1,M+1], an expansion of a real number x∈[0,M/(q−1)] over the alphabet A={0,1,...,M} is a sequence (ci)∈AN such that x=∑i=1∞ciq−i. Generalizing many earlier results, we investigate in this paper the topological properties of the set Uq consisting of numbers x having a unique expansion of this form, and the combinatorial properties of the set Uq′ consisting of their corresponding expansions. We also provide shorter proofs of the main results of Baker in [3] by adapting the method given in [12] for the case M=1
A uniform definition of stochastic process calculi
No full textWe introduce a unifying framework to provide the semantics of process algebras, including their quantitative variants useful for modeling quantitative aspects of behaviors. The unifying framework is then used to describe some of the most representative stochastic process algebras. This
provides a general and clear support for an understanding of their similarities and differences. The framework is based on State to Function Labeled Transition Systems, FuTSs for short, that are state-transition structures where each transition is a triple of the form (s; α;P). The first andthe second components are the source state, s, and the label, α, of the transition, while the third component is the continuation function, P, associating a value of a suitable type to each state s0. For example, in the case of stochastic process algebras the value of the continuation function on s0 represents the rate of the negative exponential distribution characterizing the duration/delay of the action performed to reach state s0 from s. We first provide the semantics of a simple formalism used to describe Continuous-Time Markov Chains, then we model a number of process algebras that permit parallel composition of models according to the two main interaction paradigms (multiparty and one-to-one synchronization). Finally, we deal with formalisms where actions and rates are kept separate and address the issues related to the coexistence of stochastic, probabilistic, and non-deterministic behaviors. For each formalism, we establish the formal correspondence between the FuTSs semantics and its original semantics
- …
