Rapporti tecnici

The integration of BPM and SOA has the potential to lead to increased agility, lower development and maintenance costs and a better alignment between business and IT. However, it still requires large efforts by highly skilled personnel. The Service-Targeted Policy-Oriented WorkfLow Approach attacks this problem by integrating workflows and services with policies to clearly distinguish between the core process description and the variations. This paper presents a first assessment of the impact of the approach on the design of business processes. To this end, we exploit a case study, namely the activation of VoIP services by a re-seller of telecommunication services.

The paper concers the problem of minimizing the maximum link utilization of IP telecommunication networks under the joint use of the traditional IS-IS/OPSF protocol and the more sophisticated MPLS-TE technology. Both working conditions and single link failure scenarios are addressed. An innovative Linear Programming mathematical model is proposed that, while optimizing the network utilization, provides optimal user performance, efficient use of network resources, and 100\% survivability in case of single link failure. The hybrid approach takes advantage of both IGP and MPLS-TE technologies providing a flexible tool for IP networks traffic engineers. The proposed model is validated by a wide experimentation performed on synthetic and real networks, both in working and failure conditions. The obtained results show that the new approach considerably reduces the maximum utilization of the network, thereby allowing a more efficient use of the network resources; setting a limited number of LSPs yields better results than those obtained by simply optimizing the IGP weights. In addition, an optimized set of IGP weigths allows to further improve the network performance in case of failures. The computational time needed to solve the LP model is very limited and it well matches the real time requirements.

Electoral systems are complex entities composed of a set of phases that form a process to which performance parameters can be associated. One of the key points of every electoral system is represented by the electoral formula that can be characterized by a wide spectrum of properties that, according to Arrow's Impossibility Theorem and other theoretical results, cannot be all satisfied at the same time. Starting from these basic results the aim of this paper is to examine such properties within a hierarchical framework, based on {Analytic Hierarchy Process} proposed by T. L. Saaty, performing pairwise comparisons at various levels of a hierarchy so to get a global ranking of such properties. Since any real electoral system is known to satisfy some of such properties but not others it should be possible, in this way, to get a ranking of the electoral systems according also to the political goals both of the voters and the candidates. In this way it should be possible to estimate the relative importance of each property with respect to the final ranking of every electoral formula.

The operational semantics of interactive systems is usually decsribed by labeled transition systems. Abstract semantics is defined in terms of bisimilarity, that in the finite case, can be computed via the well-known partition refinement algorithm. However, the behavoiur of interactive systems is in many case infinite and thus checking bisimilarity in this way is unfeasible. Symbolic semantics allows to define smaller, possibly finite, transition systems, by employing symbolic actions and avoiding some source of infiniteness. Unfortunately, the standard partition refinement algorithm does not work with symbolic bisimilarity. In a previous paper, we have introduced an abstract theory of symbolic semantics. In this paper, we introduce a partition refinement algorithm for symbolic bisimilarity.

In \cite{bellia2008} an extension of Java is described which allows methods to have other methods as parameters and a meaning preserving transformation is defined, which maps programs in the extended language into ordinary Java programs. In this paper we present an implementation for such extended language, based on the transformation defined. We also discuss the integration of the programs in the extended language with ordinary first order programs, and hence Java API . Eventually the language is extended with mc\_parameters for which an implementation with callbacks \cite{horstmann2007} is shown.

The present Technical Report contains a concise analysis of some participatory methods and a discussion of the bold;method of consensusas a formal tool for decisionmaking.The treatment is kept at an informal and colloquial level with the aim to be precise and concise.Thei Technical Report relies mainly on classical results, so that it may be considered as a real primer on these topics, but contains also novel materials and results.Reports of errors and inaccuracies are greatefully appreciated.

Annotations are a recent feature introduced in languages such as Java, C#, and other languages of the .NET family, which allow programmers to attach arbitrary, structured and typed metadata to their code. These languages run on top of so-called virtual execution environments, e.g. the JVM for Java, and the CLR for .NET languages, which allow for the run-time generation of executable code. In this report we explore how annotations and the dynamic code generation capability can be used together to provide programmers with high-level methods for dynamic generation and modification of an application’s code — at run-time. The report describes the framework @Java system, the Java libraries it is constituted by, and the @Java language, which is an extension to Java allowing annotation of arbitrary statements. The strategy we developed consists in parsing a source file written using @Java language to produce a Java 5 compatible source file. Once compiled, information about annotated statements,such as their bytecode instructions, can be recovered at run-time. We developed two libraries, one that works at low level to do generic bytecode engineering called JDAsm, and one at high level called JCodeBrick.Together, these two libraries allow type-safe and totally symbolic runtime code modification and generation without any need to explicitly address bytecode instructions, letting a programmer to easily manipulate existing classes or to synthesize new ones, by inserting, deleting or extruding pieces of code. After an overview of the Annotations in Section 2, we address the @Java language and its parser in Section 3. Then a full description of the two libraries for bytecode engineering and code manipulation follows in Section 4 and 5. We introduce then in Section 6 a few motivating examples of applications of @Java, and provide a more developed case study in Section7.The last section offers conclusions and ideas for future work. The documentation of the two libraries is provided in Appendix A, completing the report.

The paper presents a case study on the synthesis of labelled transition systems (LTSs) for process calculi, choosing as testbed Cardelli and Gordon's Mobile Ambients (MAs). The proposal is based on a graphical encoding: each process is mapped into a graph equipped with suitable interfaces, such that the denotation is fully abstract with respect to the usual structural congruence. Graphs with interfaces are amenable to the synthesis mechanism proposed by Ehrig and Koenig and based on borrowed contexts (BCs), an instance of relative pushouts, introduced by Leifer and Milner. The BC mechanism allows the effective construction of a LTS that has graphs with interfaces as both states and labels, and such that the associated bisimilarity is automatically a congruence. Our paper focuses on the analysis of a LTS over (processes as) graphs with interfaces, as distilled by exploiting the graphical encoding of MAs. In particular, we use the LTS on graphs to recover a suitable LTS directly defined over the structure of MAs processes.

There are several important reasons (biological, evolutionary, clinical, etc.) to give a segment-based description of genomic sequences, and, in particular, to detect repeated segments, written both direct and complemented inverted. In some applications, in particular in medical genomics, it is also necessary to count the number of occurrences of a segment. Moreover, by detecting common segments shared by two different sequences it is possible to define a sort of genomic distance between them. Here we propose BpMatch: an algorithm that, working on a suitably modified suffix-tree data structure, allows us to achieve all these three goals (identify repeated segments, including the complemented inverted copies of them, count repeats number and calculate genomic distance) in a fast and efficient way.BpMatch is able to identify exact copies (and complemented inverted copies) of a segment. The operator should define a priori the minimum length of a string, in order to be considered a segment, and the minimum number of occurrences, so that only segments having a number of occurrences greater than are considered to be significant. BpMatch is very efficient; we determined the complexity in time to calculate the self-covering of a string, the alphabet dimension. On the worst case, assuming the alphabet dimension is a constant, the time required to calculate the coverage is O. On the average, using the time required to calculate the coverage is only O. It is important to note that this estimation includes the time required to complete all of the three different tasks: to identify copied segments, to localize them, to count the number of occurrences and to evaluate the sequence coverage.

In this paper, we introduce a new notion of motifs, called \emph{masks}, that succinctly represent the repeated patterns for an input sequence $T$ of $n$ symbols drawn from an alphabet $\Sigma$. We show how to build the set of all maximal masks of length~$L$ and quorum~$q$, in $O(2^L n)$ time and space in the worst case. We analytically show that our algorithms perform better than constant-time enumerating and checking all the potential $(|\Sigma|+1)^L$ candidate patterns in~$T$ after a polynomial-time preprocessing of $T$. Our algorithms are also cache-friendly, attaining $O(2^L\, \mathit{sort}(n))$ block transfers, where $\mathit{sort}(n)$ is the cache oblivious complexity of sorting $n$ items.

After having joined forces with the International Workshop on Coalgebraic Methods in Computer Science (CMCS) for the Second International Conference on Algebra and Coalgebra in Computer Science (CALCO 2007), the Nineteenth International Workshop on Algebraic Development Techniques (WADT 2008) was held as an individual workshop and in its traditional form in Pisa, Italy, from the 13th to the 16th of June 2008. This report contains the thirtythree abstracts presented during the workshop: they were selected by the Steering Committee on the basis of the submitted abstracts according to originality, significance, and general interest. In addition to the presentations of ongoing research results, the programme included three invited lectures by Egon Boerger (Dipartimento di Informatica, Pisa), Luca Cardelli (Microsoft Research, Cambridge) and Stephen Gilmore (Laboratory for Foundations of Computer Science, Edinburgh).

The Perspective Relaxation is a general approach for constructing tight approximations to MINLP problems with semicontinuous variables. Two different reformulations have been proposed for solving it, one resulting in a Second-Order Cone Program, the other based on representing the perspective function by (an infinite number of) cutting planes. We compare the two reformulations on two sets of test problems to determine which one is most effective in the context of exact or approximate Branch-and-Cut algorithms.

Fast minimization time, compact area and low delay are important issues in logic circuit design. In order to orchestrate these main goals, in this paper we propose a new four level logic form ({\em Generalized EXOR-Projected Sum of Products}, in short {\em GEP-SOP}) with low delay and compact area. Even if the problem of finding an optimal GEP-SOPs is computationally hard, we propose an efficient approximation algorithm that gives guaranteed near optimal solutions. A wide set of experimental results confirms that the GEP-SOP forms are often more compact than the SOP forms, and their synthesis is always a very fast reoptimization phase after SOP minimization.

We introduce weak binders, a lightweight construct to deal with fresh names in nominal calculi. Weak binders do not define the scope of names as precisely as the standard nu-binders, yet they enjoy strong semantic properties.We provide them with a denotational semantics, an equational theory, and a trace inclusion preorder. Furthermore, we present a trace-preserving mapping between weak binders and nu-binders.

The presente Technical Report contains a few notes about the roles of System Dynamics for the solution of environmental problems. It is not an introduction to System Dynamics. More about the content in the abstract. Reports of errors and inaccuracies are gratefully appreciated.

In-network storage of data in wireless sensor networks (such as DCS-GHT, for instance) is considered a viable alternative to external storage since it contributes to reduce the communications inside the network and to favor data aggregation. In current approaches it exploits pure data replication to assure data availability. In this paper, we consider the use of codes and data dispersal in combination to in-network storage. In particular, given an abstract model of in-network storage we show how codes can be employed, and we discuss how this can be achieved in three cases of study. Since the configuration of the network is particularly critical with respect to correct data encoding, we define framework aimed at evaluating the probability of correct data encoding and decoding. Then we exploit this result and simulations to show how, in the cases of study, the parameters of the codes and the network should be configured in order to achieve correct data coding and decoding with high probability.

An integrated model for ranking scientific publications together with authors and journals recently presented in [Bini, Del Corso, Romani,ETNA 2008]is closely analyzed. The model, which relies on certain adjacency matrices $H,K$ and $F$ obtained from the relations of citation,authorship and publication, provides the ranking by means of the Perron vector of a stochastic matrix obtained by combining $H,K$ and $F$. Some perturbation theorems concerning the Perron vector previously introduced by the authors are extended to more general cases and a counterexample to a property previously addressed by the authors is presented. The theoretical results confirm the consistency and effectiveness of our model. Some paradigmatic examples are reported together with some results obtained on a real set of data.

An important issue of the service oriented approach is the possibility to aggregate, through programmable coordination patterns, the activities involved by service interactions. Two different approaches can be adopted to tackle service coordination: orchestration and choreography. In this paper, we introduce a formal methodology for the with the aim of handling coordinationamong services from the perspective of a global observer in the spirit of choreography models. In particular, we address the problem of verifying compliance and consistency between the design of service interactions and the choreography constraints.

The present Technical Report contains two papers that have been accepted at the S.I.N.G. 4 Conference, Wroklav, Poland, 26-28 June 2008. Both papers have been also presented in seminars at the Computer Science Department, the former on June 3 2008 and the latter on January 23 2008. The first paper presents the use of auction mechanisms for the allocation of chores instead of goods. The latter paper presents and analyzes a small set of models that can be used by two players for the barter of goods without the intervention of any numerary good.

The notion of a session is fundamental in service oriented applications, as it serves to separate interactions between different instances of the same services, and to group together logical units of work. Recently, SCC has been proposed as a calculus centered around the concept of a dyadic session, where service interaction protocols and service orchestration can be conveniently expressed. In this paper we propose a generic type system to collect services' behaviors and then we fix a class of well typed processes that are guaranteed to be deadlock free. The type system is based on previous research on traditional mobile calculi, here conveniently extended and simplified thanks to the neat discipline imposed by the linguistic primitives of SCC.

We propose a model for specifying, analysing and enforcing safe usage of resources.Our usage policies allow for parametricity over resources, and they can be enforced through finite state automata. The patterns of resource access and creation are described through a basic calculus of usages. In spite of the augmented flexibility given by resource creation and by policy parametrization, we devise an efficient (polynomial-time)model-checking technique for deciding when a usage is resource-safe,i.e. when it complies with all the relevant usage policies.

We introduce LocUsT, a tool to statically check whether a given resource usage complies with a local policy. LocUsT takes as input an abstraction of the behaviour of a program, called a usage. Usages are expressed in a simple process calculus, and over-approximate all the resource accesses of the program itself. As additional input, LocUsT takes a policy that defines the allowed resource access patterns, represented through a finite state automaton parametrized over resources. Finally, LocUsT decides whether some trace of the given usage violates some instantiation of the policy.

Autonomic management can improve the QoS provided by parallel/distributed applications. Within the CoreGRID Component Model, the autonomic management is tailored to the automatic - monitoring-driven - alteration of the component assembly and, therefore, is defined as the effect of (distributed) management code. This work yields a semantics based on hypergraph rewriting suitable to model the dynamic evolution and non-functional aspects of Service Oriented Architectures and component-based autonomic applications. In this regard, our main goal is to provide a formal description of adaptation operations that are typically only informally specified. We contend that our approach makes easier to raise the level of abstraction of management code in autonomic and adaptive applications.

Web services represent a promising technology for the development of distributed heterogeneous software systems. In this setting, a major issue is to establish whether two services can be used interchangeably in any context. This paper illustrates - through a concrete scenario from banking systems - how a suitable notion of behavioural equivalence over Petri nets can be effectively employed for checking the correctness of service specifications and the replaceability of (sub)services.

Some integrated models for ranking scientific publications together with authors and journals are presented and analyzed. The models rely on certain adiacency matrices obtained from the relations of citation,authorship and publication, which concurr to forming a suitable irreducible stochastic matrix whose Perron vector provides the ranking. Some perturbation theorems concerning the Perron vector of nonnegative irreducible matrices are proved. These theoretical results provide a validation of the consistency and effectiveness of our models. Several paradigmatic examples are reported together with some results obtained on a real set of data.

A simple type confusion attack occurs in a security protocol, when a principal interprets data of one type as data of another. These attacks can be successfully prevented by tagging types of each field of a message. Complex type confusions occur instead when tags can be confused with data and when fields or sub-segments of fields may be confused with concatenations of fields of other types. Capturing these kinds of confusions is not easy in a process calculus setting, where it is generally assumed that messages are correctly interpreted. In this paper, we model in the process calculus LySa only the misinterpretation due to the confusion of a concatenation of fields with a single field, by extending the notation of one-to-one variable binding to multi-to-one binding. We further present a formal way of detecting these possible misinterpretations, based on a Control Flow Analysis for this version of the calculus. The analysis over-approximates all the possible behaviour of a protocol, including those effected by these type confusions. As an example, we considered the amended Needham-Schroeder symmetric protocol, where we succeed in detecting the type confusion that lead to a complex type flaw attacks it is subject to. Therefore, the analysis can capture potential type confusions of this kind on security protocols, besides other security properties such as confidentiality, freshness and message authentication.

The paper discusses a general framework for outer approximation type algorithms for the canonical DC optimization problem. The algorithms rely on a polar reformulation of the problem and exploit an approximated oracle in order to check global optimality. Consequently, approximate optimality conditions are introduced and bounds on the quality of the approximate global optimal solution are obtained. A thorough analysis of properties which guarantee convergence is carried out; two families of conditions are introduced which lead to design six implementable algorithms, whose convergence can be proved within a unified framework.