Specification, execution and verification of interaction protocols: an approach based on computational logic

Interaction protocols establish how different computational entities can interact with each other. The interaction can be finalized to the exchange of data, as in 'communication protocols', or can be oriented to achieve some result, as in 'application protocols'. Moreover, with the increasing complexity of modern distributed systems, protocols are used also to control such a complexity, and to ensure that the system as a whole evolves with certain features. However, the extensive use of protocols has raised some issues, from the language for specifying them to the several verification aspects. Computational Logic provides models, languages and tools that can be effectively adopted to address such issues: its declarative nature can be exploited for a protocol specification language, while its operational counterpart can be used to reason upon such specifications. In this thesis we propose a proof-theoretic framework, called SCIFF, together with its extensions. SCIFF is based on Abductive Logic Programming, and provides a formal specification language with a clear declarative semantics (based on abduction). The operational counterpart is given by a proof procedure, that allows to reason upon the specifications and to test the conformance of given interactions w.r.t. a defined protocol. Moreover, by suitably adapting the SCIFF Framework, we propose solutions for addressing (1) the protocol properties verification (g-SCIFF Framework), and (2) the a-priori conformance verification of peers w.r.t. the given protocol (AlLoWS Framework). We introduce also an agent based architecture, the SCIFF Agent Platform, where the same protocol specification can be used to program and to ease the implementation task of the interacting peers.

Specification and Verification of Declarative Open Interaction Models - A Logic-based framework

The advent of distributed and heterogeneous systems has laid the foundation for the birth of new architectural paradigms, in which many separated and autonomous entities collaborate and interact to the aim of achieving complex strategic goals, impossible to be accomplished on their own. A non exhaustive list of systems targeted by such paradigms includes Business Process Management, Clinical Guidelines and Careflow Protocols, Service-Oriented and Multi-Agent Systems. It is largely recognized that engineering these systems requires novel modeling techniques. In particular, many authors are claiming that an open, declarative perspective is needed to complement the closed, procedural nature of the state of the art specification languages. For example, the ConDec language has been recently proposed to target the declarative and open specification of Business Processes, overcoming the over-specification and over-constraining issues of classical procedural approaches. On the one hand, the success of such novel modeling languages strongly depends on their usability by non-IT savvy: they must provide an appealing, intuitive graphical front-end. On the other hand, they must be prone to verification, in order to guarantee the trustworthiness and reliability of the developed model, as well as to ensure that the actual executions of the system effectively comply with it. In this dissertation, we claim that Computational Logic is a suitable framework for dealing with the specification, verification, execution, monitoring and analysis of these systems. We propose to adopt an extended version of the ConDec language for specifying interaction models with a declarative, open flavor. We show how all the (extended) ConDec constructs can be automatically translated to the CLIMB Computational Logic-based language, and illustrate how its corresponding reasoning techniques can be successfully exploited to provide support and verification capabilities along the whole life cycle of the targeted systems.

Previdenza complementare: evoluzione e tendenze

La tesi si articola in tre capitoli. Il primo dà conto del dibattito sorto attorno alla problematica dell’inquadramento della previdenza complementare nel sistema costituzionale dell’art. 38 Cost. che ha diviso la dottrina tra quanti hanno voluto ricondurre tale fenomeno al principio di libertà della previdenza privata di cui all’ art. 38, comma 5, Cost. e quanti lo hanno invece collocato al 2° comma della stessa norma, sulla base di una ritenuta identità di funzioni tra previdenza pubblica e previdenza complementare. Tale ultima ricostruzione in particolare dopo la c.d. Riforma “Amato” è culminata nella giurisprudenza della Corte Costituzionale, che ha avuto modo di pronunciarsi sulla questione con una serie di pronunce sulla vicenda del c.d. “contributo sul contributo” e su quella della subordinazione dei requisiti di accesso alle prestazioni pensionistiche complementari alla maturazione dei requisiti previsti dal sistema obbligatorio. Il capitolo successivo si occupa della verifica della attualità e della coerenza dell’impostazione della Corte Costituzionale alla luce dell’evoluzione della disciplina dei fondi pensione. Nel terzo capitolo, infine, vengono affrontate alcune questioni aperte in relazione ai c.d. fondi pensione “preesistenti” suscettibili di sollevare preoccupazioni circa la necessità di garantire le aspettative e i diritti dei soggetti iscritti.