Lista dei rapporti tecnici dell'anno 2008

Fantini, Paola and Montangero, Carlo and Palasciano, Claudio and Reiff-Marganiec, Stephan and Semini, Laura
Supporting user-friendly design of flexible Business Processes in StPowla
December 5, 2014
UnipiEprints view

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.

Cherubini, Davide and Fanni, Alessandra and Frangioni, Antonio and Murgia, Cristian and Scutellà, Maria Grazia and Zuddas, Paola
A Linear Programming Model for Traffic Engineering in 100% Survivable Networks under combined IS-IS/OSPF and MPLS-TE Protocols
December 5, 2014
UnipiEprints view

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.

Cioni, Lorenzo
Using a hierarchical properties ranking with AHP for the ranking of electoral systems
December 4, 2014
UnipiEprints view

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.

Bonchi, Filippo and Montanari, Ugo
Minimization Algorithm for Symbolic Bisimilarity
December 4, 2014
UnipiEprints view

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.

Occhiuto, Maria Eugena and Bellia, Marco
Java$\Omega$: The Structures and the Implementation of a Preprocessor for Java with m\_parameters
December 4, 2014
UnipiEprints view

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.

Cioni, Lorenzo
Participative methods and consensus theory
December 4, 2014
UnipiEprints view

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.

Galilei, Giacomo A.
Design and implementation of the @Java system
December 4, 2014
UnipiEprints view

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.

Bonchi, Filippo and Gadducci, Fabio and Monreale, Giacoma Valentina
Labeled Transitions for Mobile Ambients
December 4, 2014
UnipiEprints view

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.

Felicioli, C. and Marangoni, Roberto
BpMatch: an efficient algorithm for segmenting sequences, calculating genomic distance and counting repeats.
December 4, 2014
UnipiEprints view

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.

Battaglia, Giovanni and Cangelosi, Davide and Grossi, Roberto and Pisanti, Nadia
Masking Patterns in Sequences: a New Class of Motif Discovery with Don't Cares
December 4, 2014
UnipiEprints view

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.

Corradini, Andrea and Gadducci, Fabio
Preliminary proceedings of WADT 2008
December 4, 2014
UnipiEprints view

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).

Frangioni, Antonio and Gentile, Claudio
A Computational Comparison of Reformulations of the Perspective Relaxation: SOCP vs. Cutting Planes
December 4, 2014
UnipiEprints view

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.

Bernasconi, Anna and Ciriani, Valentina and Cordone, Roberto
An Approximation Algorithm for Generalized EXOR Projected Sum of Products
December 4, 2014
UnipiEprints view

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.

Bartoletti, Massimo and Degano, Pierpaolo and Ferrari, Gianluigi and Zunino, Roberto
Hard life with weak binders
December 4, 2014
UnipiEprints view

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.

Cioni, Lorenzo
The roles of System Dynamics in environmental problem solving
December 4, 2014
UnipiEprints view

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.

Chessa, Stefano and Albano, Michele
Replication vs Erasure Coding in Data Centric Storage for Sensor Networks
December 4, 2014
UnipiEprints view

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.

Bini, Dario A. and Del Corso, Gianna M. and Romani, Francesco
A combined approach for evaluating papers, authors and scientific journals
December 4, 2014
UnipiEprints view

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.

Ciancia, Vincenzo and Ferrari, Gianluigi and Guanciale, Roberto and Strollo, Daniele
Global Coordination Policies for Services
December 4, 2014
UnipiEprints view

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.

Cioni, Lorenzo
Models of interaction
December 4, 2014
UnipiEprints view

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.

Bruni, Roberto and Mezzina, Leonardo Gaetano
Types and deadlock free sessions for SCC
December 4, 2014
UnipiEprints view

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.

Zunino, Roberto and Bartoletti, Massimo and Degano, Pierpaolo and Ferrari, Gianluigi
Model checking usage policies
December 4, 2014
UnipiEprints view

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.

Bartoletti, Massimo and Zunino, Roberto
LocUsT: a tool for checking usage policies
December 4, 2014
UnipiEprints view

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.

Aldinucci, Marco and Tuosto, Emilio
Toward a Formal Semantics for Autonomic Components
December 4, 2014
UnipiEprints view

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.

Bonchi, Filippo and Brogi, Antonio and Corfini, Sara and Gadducci, Fabio
Compositional Specification of Web Services via Behavioural Equivalence of Nets: A Case Study
December 4, 2014
UnipiEprints view

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.

Bini, Dario A. and Del Corso, Gianna M. and Romani, Francesco
Evaluating scientific products by means of citation-based models: a first analysis and validation
December 4, 2014
UnipiEprints view

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.

Bodei, Chiara and Gao, Han and Degano, Pierpaolo
A Formal Analysis of Complex Type Flaw Attacks on Security Protocols.
December 4, 2014
UnipiEprints view

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.

Frangioni, Antonio and Zhang, Qinghua
Outer Approximation Algorithms for Canonical DC Problems
December 4, 2014
UnipiEprints view

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.



NOTA. Da gennaio 2015 il Technical reports possono essere inseriti nel deposito Open Access UnipiEprints.
Una volta pubblicati saranno visibili anche in queste pagine. L'importazione dei dati da UnipiEprints è ancora da perfezionare. Il vecchio sistema TR non è più mantenuto.

Dati importati da UnipiEprints