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.

Seismotectonic study on two strategic infrastructures in Southern Italy

With the entry into force of the latest Italian Building Code (NTC 2008, 2018), innovative criteria were provided, especially for what concerns the seismic verifications of large infrastructures. In particular, for buildings considered as strategic, such as large dams, a seismotectonic study of the site was declared necessary, which involves a re-assessment of the basic seismic hazard. This PhD project fits into this context, being part of the seismic re-evaluation process of large dams launched on a national scale following the O.P.C.M. 3274/2003, D.L. 79/2004. A full seismotectonic study in the region of two large earth dams in Southern Italy was carried out. We identified and characterized the structures that could generate earthquakes in our study area, together with the definition of the local seismic history. This information was used for the reassessment of the basic seismic hazard, using probabilistic seismic hazard assessment approaches. In recent years, fault-based models for the seismic hazard assessment have been proposed all over the world as a new emerging methodology. For this reason, we decided to test the innovative SHERIFS approach on our study area. The occasion of the seismotectonic study gave also the opportunity to focus on the characteristics of the seismic stations that provided the data for the study itself. In the context of the work presented here, we focused on the 10 stations that had been active for the longest time and we carried out a geophysical characterization, the data of which merged into a more general study on the soil-structure interaction at seismic stations and on the ways in which it could affect the SHA. Lastly, an additional experimental study on the two dams and their associated minor structures is also presented, aimed at defining their main dynamic parameters, useful for subsequent dynamic structural and geotechnical studies.