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.

Architectures and design patterns for functional design of logic control and diagnostics in industrial automation

Recently in most of the industrial automation process an ever increasing degree of automation has been observed. This increasing is motivated by the higher requirement of systems with great performance in terms of quality of products/services generated, productivity, efficiency and low costs in the design, realization and maintenance. This trend in the growth of complex automation systems is rapidly spreading over automated manufacturing systems (AMS), where the integration of the mechanical and electronic technology, typical of the Mechatronics, is merging with other technologies such as Informatics and the communication networks. An AMS is a very complex system that can be thought constituted by a set of flexible working stations, one or more transportation systems. To understand how this machine are important in our society let considerate that every day most of us use bottles of water or soda, buy product in box like food or cigarets and so on. Another important consideration from its complexity derive from the fact that the the consortium of machine producers has estimated around 350 types of manufacturing machine. A large number of manufacturing machine industry are presented in Italy and notably packaging machine industry,in particular a great concentration of this kind of industry is located in Bologna area; for this reason the Bologna area is called “packaging valley”. Usually, the various parts of the AMS interact among them in a concurrent and asynchronous way, and coordinate the parts of the machine to obtain a desiderated overall behaviour is an hard task. Often, this is the case in large scale systems, organized in a modular and distributed manner. Even if the success of a modern AMS from a functional and behavioural point of view is still to attribute to the design choices operated in the definition of the mechanical structure and electrical electronic architecture, the system that governs the control of the plant is becoming crucial, because of the large number of duties associated to it. Apart from the activity inherent to the automation of themachine cycles, the supervisory system is called to perform other main functions such as: emulating the behaviour of traditional mechanical members thus allowing a drastic constructive simplification of the machine and a crucial functional flexibility; dynamically adapting the control strategies according to the different productive needs and to the different operational scenarios; obtaining a high quality of the final product through the verification of the correctness of the processing; addressing the operator devoted to themachine to promptly and carefully take the actions devoted to establish or restore the optimal operating conditions; managing in real time information on diagnostics, as a support of the maintenance operations of the machine. The kind of facilities that designers can directly find on themarket, in terms of software component libraries provides in fact an adequate support as regard the implementation of either top-level or bottom-level functionalities, typically pertaining to the domains of user-friendly HMIs, closed-loop regulation and motion control, fieldbus-based interconnection of remote smart devices. What is still lacking is a reference framework comprising a comprehensive set of highly reusable logic control components that, focussing on the cross-cutting functionalities characterizing the automation domain, may help the designers in the process of modelling and structuring their applications according to the specific needs. Historically, the design and verification process for complex automated industrial systems is performed in empirical way, without a clear distinction between functional and technological-implementation concepts and without a systematic method to organically deal with the complete system. Traditionally, in the field of analog and digital control design and verification through formal and simulation tools have been adopted since a long time ago, at least for multivariable and/or nonlinear controllers for complex time-driven dynamics as in the fields of vehicles, aircrafts, robots, electric drives and complex power electronics equipments. Moving to the field of logic control, typical for industrial manufacturing automation, the design and verification process is approached in a completely different way, usually very “unstructured”. No clear distinction between functions and implementations, between functional architectures and technological architectures and platforms is considered. Probably this difference is due to the different “dynamical framework”of logic control with respect to analog/digital control. As a matter of facts, in logic control discrete-events dynamics replace time-driven dynamics; hence most of the formal and mathematical tools of analog/digital control cannot be directly migrated to logic control to enlighten the distinction between functions and implementations. In addition, in the common view of application technicians, logic control design is strictly connected to the adopted implementation technology (relays in the past, software nowadays), leading again to a deep confusion among functional view and technological view. In Industrial automation software engineering, concepts as modularity, encapsulation, composability and reusability are strongly emphasized and profitably realized in the so-calledobject-oriented methodologies. Industrial automation is receiving lately this approach, as testified by some IEC standards IEC 611313, IEC 61499 which have been considered in commercial products only recently. On the other hand, in the scientific and technical literature many contributions have been already proposed to establish a suitable modelling framework for industrial automation. During last years it was possible to note a considerable growth in the exploitation of innovative concepts and technologies from ICT world in industrial automation systems. For what concerns the logic control design, Model Based Design (MBD) is being imported in industrial automation from software engineering field. Another key-point in industrial automated systems is the growth of requirements in terms of availability, reliability and safety for technological systems. In other words, the control system should not only deal with the nominal behaviour, but should also deal with other important duties, such as diagnosis and faults isolations, recovery and safety management. Indeed, together with high performance, in complex systems fault occurrences increase. This is a consequence of the fact that, as it typically occurs in reliable mechatronic systems, in complex systems such as AMS, together with reliable mechanical elements, an increasing number of electronic devices are also present, that are more vulnerable by their own nature. The diagnosis problem and the faults isolation in a generic dynamical system consists in the design of an elaboration unit that, appropriately processing the inputs and outputs of the dynamical system, is also capable of detecting incipient faults on the plant devices, reconfiguring the control system so as to guarantee satisfactory performance. The designer should be able to formally verify the product, certifying that, in its final implementation, it will perform itsrequired function guarantying the desired level of reliability and safety; the next step is that of preventing faults and eventually reconfiguring the control system so that faults are tolerated. On this topic an important improvement to formal verification of logic control, fault diagnosis and fault tolerant control results derive from Discrete Event Systems theory. The aimof this work is to define a design pattern and a control architecture to help the designer of control logic in industrial automated systems. The work starts with a brief discussion on main characteristics and description of industrial automated systems on Chapter 1. In Chapter 2 a survey on the state of the software engineering paradigm applied to industrial automation is discussed. Chapter 3 presentes a architecture for industrial automated systems based on the new concept of Generalized Actuator showing its benefits, while in Chapter 4 this architecture is refined using a novel entity, the Generalized Device in order to have a better reusability and modularity of the control logic. In Chapter 5 a new approach will be present based on Discrete Event Systems for the problemof software formal verification and an active fault tolerant control architecture using online diagnostic. Finally conclusive remarks and some ideas on new directions to explore are given. In Appendix A are briefly reported some concepts and results about Discrete Event Systems which should help the reader in understanding some crucial points in chapter 5; while in Appendix B an overview on the experimental testbed of the Laboratory of Automation of University of Bologna, is reported to validated the approach presented in chapter 3, chapter 4 and chapter 5. In Appendix C some components model used in chapter 5 for formal verification are reported.

The special rights other than shares in cross-border mergers of limited liability companies within the European Union. A perspective from the Spanish Law

The present research aims to study the special rights other than shares in Spanish Law and the protection of their holders in cross-border mergers of limited liability companies within the European Union frame. Special rights other than shares are recognised as an independent legal category within legal systems of some EU Member States, such as Germany or Spain, through the implementation of the Third Directive 78/855/CEE concerning mergers of public limited liability companies. The above-cited Directive contains a special regime of protection for the holders of securities, other than shares, to which special rights are attached, consisting of being given rights in the acquiring company, at least equivalent to those they possessed in the company being acquired. This safeguard is to highlight the intimate connection between this type of rights and the company whose extinction determines the existence of those. Pursuant to the Directive 2005/56/CE on cross-border mergers of limited liability companies, each company taking part in these operations shall comply with the safeguards of members and third parties provided in their respective national law to which is subject. In this regard, the protection for holders of special rights other than shares shall be ruled by the domestic M&A regime. As far as Spanish Law are concerned, holders of these special rights are recognized a right of merger information, in the same terms as shareholders, as well as equal rights in the company resulting from the cross-border merger. However, these measures are not enough guarantee for a suitable protection, thus considering those holders of special rights as special creditors, sometimes it will be necessary to go to the general protection regime for creditors. In Spanish Law, it would involve the recognition of right to the merger opposition, whose exercise would prevent the operation was completed until ensuring equal rights.

Pratiche del possibile: i Participatory Guarantee Systems e le scelte d'acquisto del consumatore brasiliano

Negli ultimi anni, parallelamente all’espansione del settore biologico, si è assistito a un crescente interesse per i modelli alternativi di garanzia dell’integrità e della genuinità dei prodotti biologici. Gruppi di piccoli agricoltori di tutto il mondo hanno iniziato a sviluppare approcci alternativi per affrontare i problemi connessi alla certificazione di terza parte. Queste pratiche sono note come Sistemi di Garanzia Partecipativa (PGS). Tali modelli: (i) si basano sugli standard di certificazione biologica dell’IFOAM, (ii) riguardano il complesso dei produttori di una comunità rurale, (iii) comportano l’inclusione di una grande varietà di attori e (iv) hanno lo scopo di ridurre al minimo burocrazia e costi semplificando le procedure di verifica e incorporando un elemento di educazione ambientale e sociale sia per i produttori sia per i consumatori. Gli obiettivi di questo lavoro di ricerca: • descrivere il funzionamento dei sistemi di garanzia partecipativa; • indicare i vantaggi della loro adozione nei Paesi in via di sviluppo e non; • illustrare il caso della Rede Ecovida de Agroecologia (Brasile); • offrire uno spunto di riflessione che riguarda il consumatore e la relativa fiducia nel modello PGS. L’impianto teorico fa riferimento alla Teoria delle Convenzioni. Sulla base del quadro teorico è stato costruito un questionario per i consumatori con lo scopo di testare l’appropriatezza delle ipotesi teoriche. I risultati finali riguardano la stima del livello di conoscenza attuale, la fiducia e la volontà d’acquisto dei prodotti PGS da parte dei consumatori nelle aree considerate. Sulla base di questa ricerca sarà possibile adattare ed esportare il modello empirico in altri paesi che presentano economie diverse per cercare di comprendere il potenziale campo di applicazione dei sistemi di garanzia partecipativa.

Development and characterization of micromachined devices for separation techniques

Nowadays microfluidic is becoming an important technology in many chemical and biological processes and analysis applications. The potential to replace large-scale conventional laboratory instrumentation with miniaturized and self-contained systems, (called lab-on-a-chip (LOC) or point-of-care-testing (POCT)), offers a variety of advantages such as low reagent consumption, faster analysis speeds, and the capability of operating in a massively parallel scale in order to achieve high-throughput. Micro-electro-mechanical-systems (MEMS) technologies enable both the fabrication of miniaturized system and the possibility of developing compact and portable systems. The work described in this dissertation is towards the development of micromachined separation devices for both high-speed gas chromatography (HSGC) and gravitational field-flow fractionation (GrFFF) using MEMS technologies. Concerning the HSGC, a complete platform of three MEMS-based GC core components (injector, separation column and detector) is designed, fabricated and characterized. The microinjector consists of a set of pneumatically driven microvalves, based on a polymeric actuating membrane. Experimental results demonstrate that the microinjector is able to guarantee low dead volumes, fast actuation time, a wide operating temperature range and high chemical inertness. The microcolumn consists of an all-silicon microcolumn having a nearly circular cross-section channel. The extensive characterization has produced separation performances very close to the theoretical ideal expectations. A thermal conductivity detector (TCD) is chosen as most proper detector to be miniaturized since the volume reduction of the detector chamber results in increased mass and reduced dead volumes. The microTDC shows a good sensitivity and a very wide dynamic range. Finally a feasibility study for miniaturizing a channel suited for GrFFF is performed. The proposed GrFFF microchannel is at early stage of development, but represents a first step for the realization of a highly portable and potentially low-cost POCT device for biomedical applications.

Use of essential oils and biocontrol cultures for the improvement of shelf-life of fresh cut products

The demand of minimally processed fruits and vegetables has increased in the last years. However, their intrinsic characteristics may favor the growth of pathogens and spoilage microbiota. The negative effects on human health reported for some traditional chemical sanitizers have justified the search for substitutes to guarantee food safety and quality. In this work we have evaluate the potential of some essential oils and their components to improve the safety and the shelf life of Lamb’s lettuce (Valerianella locusta) and apples (Golden delicious). Moreover, the effects of selected lactic acid bacteria alone or in combination with essential oils or their components, on the shelf-life and safety as well as organoleptic properties of minimally processed products, were evaluated. Since the lack of knowledge of microbial cell targets of essential oils represent one of the most important limit to the use of these molecules at industrial level, another aim of this thesis was the study of the action mechanisms of essential oils and their components. The results obtained showed the beneficial effects of the natural antimicrobials as well as the selected lactic acid bacteria on minimally processed fruit and vegetable safety and shelf-life, without detrimental effects on the quality parameters. The beneficial effects obtained by the use of the selected biocontrol agents were further increased combining them with selected natural antimicrobials. The natural antimicrobial employed induced noticeable modifications of membrane fatty acid profiles and volatile compounds produced by microbial cells during the growth. The modification of the expression in genes involved in fatty acid biosynthesis suggesting that the cytoplasmic membrane of microbial cells is one of the major cellular target of essential oils and their components. The comprehension of microbial stress response mechanisms can contribute to the scaling up of natural antimicrobials and bio-control agents at industrial level.

Milk and dairy products: evaluation of bioactive components by analytical techniques

Milk and dairy products are important source of bioactive compounds useful to satisfy the nutritional and physiological needs of any newborns of mammalian species and useful to guarantee adequate growth and development of infants as well as provide a complete nourishment of adults. Physico-chemical, nutritional and organoleptic properties of the main constituents and the “minor” components have a crucial role in the quality of milk and milk products. Although in the past decades dietary milk fat was often regarded as harmful for the human health, recent researches suggest that milk contains specific fatty acids with nutritional and physiological health benefits. For these reasons, a major attention is given to the quantity and quality of total fat intake. In the recent years, as a result of the new concept of multifunctional agriculture and the changing behaviours about diet, consumer demands in favor of high-quality, security and safety dairy products are increased. Moreover, milk proteins and milk-derived bioactive peptides are recognized to have a high nutritive value, several health-promoting functional activities and excellent technological properties. Accordingly, growing interest in the development of functional dairy products and preparation of infant formulae for babies who cannot be breast-fed, has been give in order to meet the specific consumer’s requests. This manuscript presents the main results obtained during my PhD research aimed to evaluate the main bioactive lipids and proteins in milk and dairy products using innovative analytical techniques. The experimental section of this manuscript is divided in two sections where are reported the main results obtained during my research activities on dairy products and human milks in order to characterize their bioactive compounds for functional food applications.

Exploring the biofilm of Streptococcus agalactiae to identify virulence factors

Streptococcus agalactiae, also known as Group B Streptococcus (GBS) is the primary colonizer of the anogenital mucosa of up to 40% of healthy women and an important cause of invasive neonatal infections worldwide. Among the 10 known capsular serotypes, GBS type III accounts for 30-76% of the cases of neonatal meningitis. Biofilms are dense aggregates of surface-adherent microorganisms embedded in an exopolysaccharide matrix. Centers for Disease Control and Prevention estimate that 65% of human bacterial infections involve biofilms (Post et al., 2004). In recent years, the ability of GBS to form biofilm attracted attention for its possible role in fitness and/or virulence. Here, a new in vitro biofilm formation protocol was developed to guarantee more stringent conditions, to better discriminate between strong-, low- and non- biofilm forming strains and reduce ambiguous data interpretation. This protocol was applied to screen the in vitro biofilm formation ability of more than 350 GBS clinical isolates from pregnant women and neonatal infections belonging to different serotype, in relation to media composition and pH. The results showed the enhancement of GBS biofilm formation in acidic condition and identified a subset of isolates belonging to serotypes III and V that forms strong biofilms in these conditions. Interestingly, the best biofilm formers belonged to the serotype III hypervirulent clone ST-17.It was also found that pH 5.0 induces down-regulation of the capsule but that this reduction is not enough by itself to ensure biofilm formation. Moreover, the ability of proteinase K to strongly inhibit biofilm formation and to disaggregate mature biofilms suggested that proteins play an essential role in promoting GBS biofilm formation and contribute to the biofilm structural stability. Finally, a set of proteins potentially expressed during the GBS in vitro biofilm formation were identified by mass spectrometry.

The Application of European Competition Law in Arbitration Proceedings

This work provides several policy proposals capable to strengthen the private enforcement of EU competition law in arbitration. It focuses on the procedural law aspects that are permeated by legal uncertainty and that have not yet fallen under the scrutiny of the law and economics debate. The policy proposals described herein are based on the functional approach to law and economics and aim to promote a more qualified decision making process by: adjudicators, private parties and lawmakers. The resulting framework of procedural rules would be a cost-effective policy tool that could sustain the European Commission’s effort to guarantee a workable level of competition in the EU internal market. This project aims to answer the following broad research question: which procedural rules can improve the efficiency of antitrust arbitration by decreasing litigation costs for private parties on the one hand, and by increasing private parties’ compliance with competition law on the other hand?Throughout this research project, such broad question has been developed into research sub-questions revolving around several key legal issues. The chosen sub-research questions result from a vacuum in the European enforcement system that leaves several key legal issues in antitrust arbitration unresolved. The legal framework proposed in this research project could prevent such a blurry scenario from impairing the EU private enforcement of competition law in arbitration. Therefore, our attention was triggered by those legal issues whose proposed solutions lead to relevant uncertainties and that are most suitable for a law and economics analysis.

Development of an innovative pyrolysis plant for the production of secondary raw materials

This project was born with the aim of developing an environmentally and financially sustainable process to dispose of end-life tires. In this perspective was devised an innovative static bed batch pilot reactor where pyrolysis can be carried out on the whole tires in order to recover energy and materials and simultaneously save the energy costs of their shredding. The innovative plant is also able to guarantee a high safety of the process thanks to the presence of a hydraulic guard. The pilot plant was used to pyrolyze new and end-life tires at temperatures from 400 to 600°C with step of 50°C in presence of steam. The main objective of this research was to evaluate the influence of the maximum process temperature on yields and chemical-physics properties of pyrolysis products. In addition, in view of a scale-up of the plant in continuous mode, the influence of the nature of several different tires as well as the effects of the aging on the final products were studied. The same pilot plant was also used to carry out pyrolysis on polymeric matrix composites in order to obtain chemical feedstocks from the resin degradation together with the recovery of the reinforcement in the form of fibers. Carbon fibers reinforced composites ad fiberglass was treated in the 450-600°C range and the products was fully characterized. A second oxidative step was performed on the pyrolysis solid residue in order to obtain the fibers in a suitable condition for a subsequent re-impregnation in order to close the composite Life Cycle in a cradle-to-cradle approach. These investigations have demonstrated that steel wires, char, carbon and glass fibers recovered in the prototypal plant as solid residues can be a viable alternative to pristine materials, making use of them to obtain new products with a commercial added value.

Design and Control of Robotic Hands

The application of dexterous robotic hands out of research laboratories has been limited by the intrinsic complexity that these devices present. This is directly reflected as an economically unreasonable cost and a low overall reliability. Within the research reported in this thesis it is shown how the problem of complexity in the design of robotic hands can be tackled, taking advantage of modern technologies (i.e. rapid prototyping), leading to innovative concepts for the design of the mechanical structure, the actuation and sensory systems. The solutions adopted drastically reduce the prototyping and production costs and increase the reliability, reducing the number of parts required and averaging their single reliability factors. In order to get guidelines for the design process, the problem of robotic grasp and manipulation by a dual arm/hand system has been reviewed. In this way, the requirements that should be fulfilled at hardware level to guarantee successful execution of the task has been highlighted. The contribution of this research from the manipulation planning side focuses on the redundancy resolution that arise in the execution of the task in a dexterous arm/hand system. In literature the problem of coordination of arm and hand during manipulation of an object has been widely analyzed in theory but often experimentally demonstrated in simplified robotic setup. Our aim is to cover the lack in the study of this topic and experimentally evaluate it in a complex system as a anthropomorphic arm hand system.

Assessment of gait spatio-temporal parameters in neurological disorders using wearable inertial sensors

Movement analysis carried out in laboratory settings is a powerful, but costly solution since it requires dedicated instrumentation, space and personnel. Recently, new technologies such as the magnetic and inertial measurement units (MIMU) are becoming widely accepted as tools for the assessment of human motion in clinical and research settings. They are relatively easy-to-use and potentially suitable for estimating gait kinematic features, including spatio-temporal parameters. The objective of this thesis regards the development and testing in clinical contexts of robust MIMUs based methods for assessing gait spatio-temporal parameters applicable across a number of different pathological gait patterns. First, considering the need of a solution the least obtrusive as possible, the validity of the single unit based approach was explored. A comparative evaluation of the performance of various methods reported in the literature for estimating gait temporal parameters using a single unit attached to the trunk first in normal gait and then in different pathological gait conditions was performed. Then, the second part of the research headed towards the development of new methods for estimating gait spatio-temporal parameters using shank worn MIMUs on different pathological subjects groups. In addition to the conventional gait parameters, new methods for estimating the changes of the direction of progression were explored. Finally, a new hardware solution and relevant methodology for estimating inter-feet distance during walking was proposed. Results of the technical validation of the proposed methods at different walking speeds and along different paths against a gold standard were reported and showed that the use of two MIMUs attached to the lower limbs associated with a robust method guarantee a much higher accuracy in determining gait spatio-temporal parameters. In conclusion, the proposed methods could be reliably applied to various abnormal gaits obtaining in some cases a comparable level of accuracy with respect to normal gait.