Algebraic–coalgebraic specification in CoCasl

We introduce CoCasl as a light-weight but expressive coalgebraic extension of the algebraic specification language Casl. CoCasl allows the nested combination of algebraic datatypes and coalgebraic process types. Moreover, it provides syntactic sugar for an observer-indexed modal logic that allows e.g. expressing fairness properties. This logic includes a generic definition of modal operators for observers with structured equational result types. We prove existence of final models for specifications in a format that allows the use of equationally specified initial datatypes as observations, as well as modal axioms. The use of CoCasl is illustrated by specifications of the process algebras CSP and CCS.     

Bytecode Rewriting in Tom

In this paper, we present a term rewriting based library for manipulating Java bytecode. We define a mapping from bytecode programs to algebraic terms, and we use Tom, an extension of Java that adds pattern-matching facilities, to describe transformations. An originality of Tom is that it provides a powerful strategy language to express traversals over trees and to control how transformation rules are applied. To be even more expressive, we use CTL formulae as conditions and we show how their satisfiability can be ensured using the strategy formalism. Through small examples, we show how bytecode analysis and transformations can be defined in an elegant way. In particular, we outline the implementation of a ClassLoader parameterized by a security policy that restricts file access.     

A research agenda for query processing in large-scale peer data management systems

Peer Data Management Systems (Pdms) are a novel, useful, but challenging paradigm for distributed data management and query processing. Conventional integrated information systems have a hierarchical structure with an integration component that manages a global schema and distributes queries against this schema to the underlying data sources. Pdms are a natural extension to this architecture by allowing each participating system (peer) to act both as a data source and as an integrator. Peers are interconnected by schema mappings, which guide the rewriting of queries between the heterogeneous schemas, and thus form a P2P (peer-to-peer)-like network.Despite several years of research, the development of efficient Pdms still holds many challenges. In this article we first survey the state of the art on peer data management: We classify Pdms by characteristics concerning their system model, their semantics, their query planning schemes, and their maintenance. Then we systematically examine open research directions in each of those areas. In particular, we observe that research results from both the domain of P2P systems and of conventional distributed data management can have an impact on the development of Pdms.     

Enantioselective, potentiometric membrane electrodes based on cyclodextrins for the determination of l-histidine

Four enantioselective, potentiometric membrane electrodes based on carbon paste impregnated with α-, β-, 2-hydroxyl-3-trimethylammoniopropyl-β-(as chloride salt) and γ-cyclodextrins (γ-CDs) are proposed for the assay of l-histidine (l-his). The proposed electrodes showed near-Nernstian response over l-his but not over d-histidine (d-his). The recovery of l-his in the presence of d-his was higher than 99.10% with R.S.D. lower than 0.1%. The surfaces of the electrodes are easily renewable by simply polishing on an alumina paper.     

ReSpecT Nets: Towards an Analysis Methodology for ReSpecT Specifications

A key feature for infrastructures providing coordination services is the ability to define the behaviour of coordination abstractions according to the requirements identified at design-time. We take as a representative for this scenario the logic-based language ReSpecT (Reaction Specification Tuples), used to program the reactive behaviour of tuple centres. ReSpecT specifications are at the core of the engineering methodology underlying the TuCSoN infrastructure, and are therefore the “conceptual place” where formal methods can be fruitfully applied to guarantee relevant system properties.In this paper we introduce ReSpecT nets, a formalism that can be used to describe reactive behaviours that can succeed and fail, and that allows for an encoding to Petri nets with inhibitor arcs. ReSpecT nets are introduced to give a core model to a fragment of the ReSpecT language, and to pave the way for devising an analysis methodology including formal verification of safety and liveness properties. In particular, we provide a semantics to ReSpecT specifications through a mapping to ReSpecT nets. The potential of this approach for the analysis of ReSpecT specifications is discussed, presenting initial results for the analysis of safety properties.     

Multicast inference of temporal loss characteristics

Multicast-based inference has been proposed as a method of estimating average loss rates of internal network links, using end-to-end loss measurements of probes sent over a multicast tree. We show that, in addition to loss rates, temporal characteristics of losses can also be estimated. Knowledge of temporal loss characteristics has applications for services such as voip which are sensitive to loss bursts, as well as for bottleneck detection. Under the assumption of mutually independent, but otherwise general, link loss processes, we show that probabilities of arbitrary loss patterns, mean loss-run length, and even the loss-run distribution, can be recovered for each link. Alternative estimators are presented which trade-off efficiency of data use against implementation complexity. A second contribution is a novel method of reducing the computational complexity of estimation, which can also be used by existing minc estimators. We analyse estimator performance using a combination of theory and simulation.     

Exogenous Probabilistic Computation Tree Logic

We define a logic EpCTL for reasoning about the evolution of probabilistic systems. System states correspond to probability distributions over classical states and the system evolution is modelled by probabilistic Kripke structures that capture both stochastic and non–deterministic transitions. The proposed logic is a temporal enrichment of Exogenous Probabilistic Propositional Logic (EPPL). The model-checking problem for EpCTL is analysed and the logic is compared with PCTL; the semantics of the former is defined in terms of probability distributions over sets of propositional symbols, whereas the latter is designed for reasoning about distributions over paths of possible behaviour. The intended application of the logic is as a specification formalism for properties of communication protocols, and security protocols in particular; to demonstrate this, we specify relevant security properties for a classical contract signing protocol and for the so–called quantum one–time pad.     

Towards the Semantics and Verification of BPEL4WS

In this paper, we discuss the semantics of BPEL4WS language which is a de facto standard for specifying and execution workflow specification for web service composition and orchestration. We propose a language μ-BPEL that includes most primitive and structured activities of BPEL4WS, and define its semantics. As the Timed Automata (TA) is powerful in designing real-time models with multiple clocks and has well developed automatic tool support, we define a map from μ-BPEL into composable TA. Therefore, the properties we want to check can be verified in TA network correspondingly. Furthermore, we prove that the mapping from μ-BPEL to TA is a simulation, which means that the TA network simulates correctly the corresponding μ-BPEL specification. The case study with model checker Uppaal shows that our method is effective, and a Java supporting tool based on Uppaal model checker engine has been developed.     

A Petri Net Semantics of a Simple Process Algebra for Mobility

In this paper, we propose a structural translation of terms from a simple variant of the Klaim process algebra into behaviourally equivalent finite high level Petri nets. This yields a formal semantics for mobility allowing one to deal directly with concurrency and causality.     

Verification of Random Graph Transformation Systems

In this paper we describe some statistical results obtained by the verification of random graph transformation systems (GTSs). As a verification technique we use over-approximation of GTSs by Petri nets. Properties we want to verify are given by markings of Petri nets. We also use counterexample-guided abstraction refinement approach to refine the obtained approximation. A software tool (Augur) supports the verification procedure. The idea of the paper is to see how many of the generated systems can be successfully verified using this technique.     

Design of a magnetostrictive (MS) actuator

Several advanced technologies are introduced in automotive applications. Higher energy density and dynamic performance are demanding new and cost-effective actuator structures. Magnetostriction (MS), change in shape of materials under the influence of an external magnetic field, is one of the advanced technologies. Good understanding of specific design constrains is required to define and optimize a magnetostrictive actuator. This paper presents parametrical analysis with magnetic simulation of a magnetostrictive actuator. Proposed actuator has been designed, and the performance has been evaluated on experimental rig. Strain, elongation of the shaft, of 1000 ppm at 10 A and a blocked force over 4500 N has been achieved with shaft of 8 mm diameter, made of Terfenol-D. Furthermore, the effect of pre-stress of the Terfenol-D shaft has been evaluated experimentally. The study shows that excellent features can be obtained by magnetostrictive materials for many advanced applications.     

Parameterized algorithmics for d-Hitting Set

Based on the methodology we presented in earlier work on parameterized algorithms for 3-Hitting Set, we develop simple search tree-based algorithms for d-Hitting Set. We considerably improve on the bounds that were elsewhere derived for these problems.     

Timed verification of hierarchical communicating real-time state machines

Hierarchical Communicating Real-Time State Machines (H-CRSM) is a formal modelling language for the modular development of distributed real-time systems. The formalism is characterized by the use of state transitions with guarded commands and timing constraints, the adoption of a few distilled statecharts constructs, and the modular specification of timing constraints along a state hierarchy. This paper proposes a translation of H-CRSM into Uppaal which enables model checking. Translation rests on unfolding a hierarchical model on a flat representation. The resultant approach is demonstrated by means of a case study.     

Virtual Organizations in Arigatoni

Arigatoni is a lightweight overlay network that deploys the Global Computing Paradigm over the Internet. Communication for over the behavioral units of the overlay is performed by a simple resource discovery protocol (RDP). Basic Global Computers Units (GC) can communicate by first registering to a brokering service and then by mutually asking and offering services.Colonies and communities are the main entities in the model. A colony is a simple virtual organization composed by exactly one leader and some set (possibly empty) of individuals. A community is a raw set of colonies and global computers (think it as a soup of colonies and global computer without a leader).We present an operational semantics via a labeled transition system, that describes the main operations necessary in the Arigatoni model to perform leader negotiation, joining/leaving a colony, linking two colonies and moving one GC from one colony to another. Our formalization results to be adequate w.r.t. the algorithm performing peer logging/delogging and colony aggregation.     

On the relationship between the problem of anisotropy-based controller synthesis and classical optimal control problems

Consideration is given to the interrelation between different problems of \(\mathcal{H}_2 \)-and \(\mathcal{H}_\infty \)-optimization and their relationship with the theory of anisotropy-based control. It was shown that the anisotropy-based controller of the full order for the completely defined linear system minimizes the mean amount of the transmitted information between the input and output of the closed system.     

Direct amperometric determination of l-ascorbic acid (Vitamin C) at octacyanomolybdate-doped-poly(4-vinylpyridine) modified electrode in fruit juice and pharmaceuticals

The glassy carbon electrode (GCE) modified with Mo(CN)₈⁴⁻-incorporated-poly(4-vinylpyridine) (PVP/Mo(CN)₈⁴⁻), which has been recently shown to possess several attractive attributes as an efficient electrocatalytic electrode for l-ascorbic acid oxidation and its estimation, is used for l-ascorbic acid estimation directly in orange fruit juice and Celin tablet in a 0.1 M H₂SO₄ acid solution without any special treatment. Constant potential amperometry at 570 mV (saturated calomel electrode, SCE) in stirred solutions is used for this purpose. A good correlation is attained with the official titrametric method. To understand the possible electrocatalytic reaction mechanism for the electro-oxidation of l-ascorbic acid, calibration graphs over the range 1 × 10⁻⁵ to 1 × 10⁻² mol dm⁻³ l-ascorbic acid are compared for the three electrodes, ca. PVP/Mo(CN)₈⁴⁻, undoped PVP, and GCE; the curvature at high ascorbic acid concentration for the PVP/Mo(CN)₈⁴⁻ electrode is explained in terms of Michaelis–Menten (MM) saturation kinetics. The apparent MM constant (K_M), the maximum catalytic current (i_M), the complex decomposition rate constant (k_c), and the heterogeneous modified electrode rate constant (k^′_ME) are calculated from three different approaches. A reasonably high value of ≈1 × 10⁻² cm s⁻¹ is obtained for k^′_ME, indicating efficient l-ascorbic acid mediation at the PVP/Mo(CN)₈⁴⁻ electrode, thus accounting for quite a high sensitivity of this modified film electrode compared to several other modified electrodes.