Automatic code generation: from process algebraic architectural descriptions to multithreaded java programs

Process algebraic architectural description languages provide a formal means for modeling software systems and assessing their properties. In order to bridge the gap between system modeling and system im- plementation, in this thesis an approach is proposed for automatically generating multithreaded object-oriented code from process algebraic architectural descriptions, in a way that preserves – under certain assumptions – the properties proved at the architectural level. The approach is divided into three phases, which are illustrated by means of a running example based on an audio processing system. First, we develop an architecture-driven technique for thread coordination management, which is completely automated through a suitable package. Second, we address the translation of the algebraically-specified behavior of the individual software units into thread templates, which will have to be filled in by the software developer according to certain guidelines. Third, we discuss performance issues related to the suitability of synthesizing monitors rather than threads from software unit descriptions that satisfy specific constraints. In addition to the running example, we present two case studies about a video animation repainting system and the implementation of a leader election algorithm, in order to summarize the whole approach. The outcome of this thesis is the implementation of the proposed approach in a translator called PADL2Java and its integration in the architecture-centric verification tool TwoTowers.

Profili critici in materia di transnational group action

La presente tesi di dottorato ha ad oggetto l’analisi dei profili critici emersi nella prassi in relazione alle transnational damages group actions. All’interno di tale esteso ambito di ricerca, senza pretese di esaustività, si affronteranno determinati aspetti, tenendo in considerazione quanto accaduto negli ordinamenti che, sebbene in modo assai limitato, hanno già conosciuto tali problematiche. A seguito di una prima parte meramente introduttiva, nel secondo capitolo, si inquadreranno brevemente gli strumenti di tutela collettiva risarcitoria, indicando in che cosa consistano, a quali esigenze rispondano e quale origine abbiano; si indicheranno altresì i criteri distintivi e di classificazione che maggiormente possono rilevare nell’ottica di una cross border litigation. Nel terzo capitolo si analizzerà in termini essenziali la disciplina delle azioni collettive di alcuni Paesi, al fine di porre le basi necessarie per comprendere in quale contesto normativo si pongano le problematiche inerenti alle multi-jurisdictional collective redress actions. Nel quarto capitolo, si prenderà in considerazione la dimensione transnazionale delle azioni collettive, tenendo presenti le categorie e le regole affermatesi nel diritto internazionale privato e processuale e, soprattutto, quelle esistenti nell’ordinamento italiano e comunitario. Si individueranno poi gli obiettivi prioritari che si deve porre il giudice richiesto di giudicare sull’azione collettiva nella necessità di rendere una pronuncia o approvare una transazione che, da un lato, sia riconosciuta ed eseguita nei Paesi in cui dovrà essere riconosciuta ed eseguita e che, dall’altro lato, in ipotesi di opt out procedure, precluda ai soggetti che la pronuncia o la transazione dovrebbe vincolare successive azioni individuali e/o collettive in altri Paesi. Nel quinto capitolo, alla luce dei dati indicati nel terzo capitolo e delle considerazioni effettuate nel quarto capitolo, si analizzeranno alcuni dei profili critici posti dalla dimensione transnazionale delle azioni collettive; a tal fine, la trattazione verrà suddivisa in diversi punti che, pur essendo necessariamente connessi tra loro, nella loro individualità riescano ad evidenziare l’importanza e la centralità di determinate questioni. Peraltro, nell’intento di rispondere in modo adeguato alle problematiche analizzate, si indicheranno alcune delle soluzioni sperimentate dalla pratica giudiziaria o proposte dalla recente letteratura sul tema. Seguirà, infine, un ultimo capitolo contenente le osservazioni conclusive sugli esiti del lavoro.

Type Systems for Distributed Programs: Components and Sessions

Modern software systems, in particular distributed ones, are everywhere around us and are at the basis of our everyday activities. Hence, guaranteeing their cor- rectness, consistency and safety is of paramount importance. Their complexity makes the verification of such properties a very challenging task. It is natural to expect that these systems are reliable and above all usable. i) In order to be reliable, compositional models of software systems need to account for consistent dynamic reconfiguration, i.e., changing at runtime the communication patterns of a program. ii) In order to be useful, compositional models of software systems need to account for interaction, which can be seen as communication patterns among components which collaborate together to achieve a common task. The aim of the Ph.D. was to develop powerful techniques based on formal methods for the verification of correctness, consistency and safety properties related to dynamic reconfiguration and communication in complex distributed systems. In particular, static analysis techniques based on types and type systems appeared to be an adequate methodology, considering their success in guaranteeing not only basic safety properties, but also more sophisticated ones like, deadlock or livelock freedom in a concurrent setting. The main contributions of this dissertation are twofold. i) On the components side: we design types and a type system for a concurrent object-oriented calculus to statically ensure consistency of dynamic reconfigurations related to modifications of communication patterns in a program during execution time. ii) On the communication side: we study advanced safety properties related to communication in complex distributed systems like deadlock-freedom, livelock- freedom and progress. Most importantly, we exploit an encoding of types and terms of a typical distributed language, session π-calculus, into the standard typed π- calculus, in order to understand their expressive power.