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.

The environmental DNA in the risk assessment and decision making processes for the invasive species management in agri-food sector, hydraulic security and biodiversity conservation

The use of environmental DNA (eDNA) analysis as a monitoring tool is becoming more and more widespread. The eDNA metabarcoding methods allow rapid community assessments of different target taxa. This work is focused on the validation of the environmental DNA metabarcoding protocol for biodiversity assessment of freshwater habitats. Scolo Dosolo was chosen as study area and three sampling points were defined for traditional and eDNA analyses. The gutter is a 205 m long anthropic canal located in Sala Bolognese (Bologna, Italy). Fish community and freshwater invertebrate metazoans were the target groups for the analysis. After a preliminary study in summer 2019, 2020 was devoted to the sampling campaign with winter (January), spring (May), summer (July) and autumn (October) surveys. Alongside with the water samplings for the eDNA study, also traditional fish surveys using the electrofishing technique were performed to assess fish community composition; census on invertebrates was performed using an entomological net and a surber sampler. After in silico analysis, the MiFish primer set amplifying a fragment of the 12s rRNA gene was selected for bony fishes. For invertebrates the FWHF2 + FWHR2N primer combination, that amplifies a region of the mitochondrial coi gene, was chosen. Raw reads were analyzed through a bioinformatic pipeline based on OBITools metabarcoding programs package and QIIME2. The OBITools pipeline retrieved seven fish taxa and 54 invertebrate taxa belonging to six different phyla, while QIIME2 recovered eight fish taxa and 45 invertebrate taxa belonging to the same six phyla as the OBITools pipeline. The metabarcoding results were then compared with the traditional surveys data and bibliographic records. Overall, the validated protocol provides a reliable picture of the biodiversity of the study area and an efficient support to the traditional methods.