Rigorous development of safety-critical systems

Nowadays, computer-based systems tend to become more complex and control increasingly critical functions affecting different areas of human activities. Failures of such systems might result in loss of human lives as well as significant damage to the environment. Therefore, their safety needs to be ensured. However, the development of safety-critical systems is not a trivial exercise. Hence, to preclude design faults and guarantee the desired behaviour, different industrial standards prescribe the use of rigorous techniques for development and verification of such systems. The more critical the system is, the more rigorous approach should be undertaken. To ensure safety of a critical computer-based system, satisfaction of the safety requirements imposed on this system should be demonstrated. This task involves a number of activities. In particular, a set of the safety requirements is usually derived by conducting various safety analysis techniques. Strong assurance that the system satisfies the safety requirements can be provided by formal methods, i.e., mathematically-based techniques. At the same time, the evidence that the system under consideration meets the imposed safety requirements might be demonstrated by constructing safety cases. However, the overall safety assurance process of critical computerbased systems remains insufficiently defined due to the following reasons. Firstly, there are semantic differences between safety requirements and formal models. Informally represented safety requirements should be translated into the underlying formal language to enable further veri cation. Secondly, the development of formal models of complex systems can be labour-intensive and time consuming. Thirdly, there are only a few well-defined methods for integration of formal verification results into safety cases. This thesis proposes an integrated approach to the rigorous development and verification of safety-critical systems that (1) facilitates elicitation of safety requirements and their incorporation into formal models, (2) simplifies formal modelling and verification by proposing specification and refinement patterns, and (3) assists in the construction of safety cases from the artefacts generated by formal reasoning. Our chosen formal framework is Event-B. It allows us to tackle the complexity of safety-critical systems as well as to structure safety requirements by applying abstraction and stepwise refinement. The Rodin platform, a tool supporting Event-B, assists in automatic model transformations and proof-based verification of the desired system properties. The proposed approach has been validated by several case studies from different application domains.

Video-based analysis of Gait pathologies

L’analyse de la marche a émergé comme l’un des domaines médicaux le plus im- portants récemment. Les systèmes à base de marqueurs sont les méthodes les plus fa- vorisées par l’évaluation du mouvement humain et l’analyse de la marche, cependant, ces systèmes nécessitent des équipements et de l’expertise spécifiques et sont lourds, coûteux et difficiles à utiliser. De nombreuses approches récentes basées sur la vision par ordinateur ont été développées pour réduire le coût des systèmes de capture de mou- vement tout en assurant un résultat de haute précision. Dans cette thèse, nous présentons notre nouveau système d’analyse de la démarche à faible coût, qui est composé de deux caméras vidéo monoculaire placées sur le côté gauche et droit d’un tapis roulant. Chaque modèle 2D de la moitié du squelette humain est reconstruit à partir de chaque vue sur la base de la segmentation dynamique de la couleur, l’analyse de la marche est alors effectuée sur ces deux modèles. La validation avec l’état de l’art basée sur la vision du système de capture de mouvement (en utilisant le Microsoft Kinect) et la réalité du ter- rain (avec des marqueurs) a été faite pour démontrer la robustesse et l’efficacité de notre système. L’erreur moyenne de l’estimation du modèle de squelette humain par rapport à la réalité du terrain entre notre méthode vs Kinect est très prometteur: les joints des angles de cuisses (6,29◦ contre 9,68◦), jambes (7,68◦ contre 11,47◦), pieds (6,14◦ contre 13,63◦), la longueur de la foulée (6.14cm rapport de 13.63cm) sont meilleurs et plus stables que ceux de la Kinect, alors que le système peut maintenir une précision assez proche de la Kinect pour les bras (7,29◦ contre 6,12◦), les bras inférieurs (8,33◦ contre 8,04◦), et le torse (8,69◦contre 6,47◦). Basé sur le modèle de squelette obtenu par chaque méthode, nous avons réalisé une étude de symétrie sur différentes articulations (coude, genou et cheville) en utilisant chaque méthode sur trois sujets différents pour voir quelle méthode permet de distinguer plus efficacement la caractéristique symétrie / asymétrie de la marche. Dans notre test, notre système a un angle de genou au maximum de 8,97◦ et 13,86◦ pour des promenades normale et asymétrique respectivement, tandis que la Kinect a donné 10,58◦et 11,94◦. Par rapport à la réalité de terrain, 7,64◦et 14,34◦, notre système a montré une plus grande précision et pouvoir discriminant entre les deux cas.

Principle-Based Parsing

During the past few years, there has been much discussion of a shift from rule-based systems to principle-based systems for natural language processing. This paper outlines the major computational advantages of principle-based parsing, its differences from the usual rule-based approach, and surveys several existing principle-based parsing systems used for handling languages as diverse as Warlpiri, English, and Spanish, as well as language translation.

Knowledge-based modelling and simulation of operational problems of microbiological origin in wastewater treatment plants

The activated sludge and anaerobic digestion processes have been modelled in widely accepted models. Nevertheless, these models still have limitations when describing operational problems of microbiological origin. The aim of this thesis is to develop a knowledge-based model to simulate risk of plant-wide operational problems of microbiological origin.For the risk model heuristic knowledge from experts and literature was implemented in a rule-based system. Using fuzzy logic, the system can infer a risk index for the main operational problems of microbiological origin (i.e. filamentous bulking, biological foaming, rising sludge and deflocculation). To show the results of the risk model, it was implemented in the Benchmark Simulation Models. This allowed to study the risk model's response in different scenarios and control strategies. The risk model has shown to be really useful providing a third criterion to evaluate control strategies apart from the economical and environmental criteria.

Supervisory systems in waste water treatment plants: sistematise their implementation

La implantació de Sistemes de Suport a la presa de Decisions (SSD) en Estacions Depuradores d'Aigües Residuals Urbanes (EDAR) facilita l'aplicació de tècniques més eficients basades en el coneixement per a la gestió del procés, assegurant la qualitat de l'aigua de sortida tot minimitzant el cost ambiental de la seva explotació. Els sistemes basats en el coneixement es caracteritzen per la seva capacitat de treballar amb dominis molt poc estructurats, i gran part de la informació rellevant de tipus qualitatiu i/o incerta. Precisament aquests són els trets característics que es poden trobar en els sistemes biològics de depuració, i en conseqüència en una EDAR. No obstant, l'elevada complexitat dels SSD fa molt costós el seu disseny, desenvolupament i aplicació en planta real, pel que resulta determinant la generació d'un protocol que faciliti la seva exportació a EDARs de tecnologia similar. L'objectiu del present treball de Tesi és precisament el desenvolupament d'un protocol que faciliti l'exportació sistemàtica de SSD i l'aprofitament del coneixement del procés prèviament adquirit. El treball es desenvolupa en base al cas d'estudi resultant de l'exportació a l'EDAR Montornès del prototipus original de SSD implementat a l'EDAR Granollers. Aquest SSD integra dos tipus de sistemes basats en el coneixement, concretament els sistemes basats en regles (els quals són programes informàtics que emulen el raonament humà i la seva capacitat de solucionar problemes utilitzant les mateixes fonts d'informació) i els sistemes de raonament basats en casos (els quals són programes informàtics basats en el coneixement que volen solucionar les situacions anormals que pateix la planta en el moment actual mitjançant el record de l'acció efectuada en una situació passada similar). El treball està estructurat en diferents capítols, en el primer dels quals, el lector s'introdueix en el món dels sistemes de suport a la decisió i en el domini de la depuració d'aigües. Seguidament es fixen els objectius i es descriuen els materials i mètodes utilitzats. A continuació es presenta el prototipus de SSD desenvolupat per la EDAR Granollers. Una vegada el prototipus ha estat presentat es descriu el primer protocol plantejat pel mateix autor de la Tesi en el seu Treball de Recerca. A continuació es presenten els resultats obtinguts en l'aplicació pràctica del protocol per generar un nou SSD, per una planta depuradora diferent, partint del prototipus. L'aplicació pràctica del protocol permet l'evolució del mateix cap a un millor pla d'exportació. Finalment, es pot concloure que el nou protocol redueix el temps necessari per realitzar el procés d'exportació, tot i que el nombre de passos necessaris ha augmentat, la qual cosa significa que el nou protocol és més sistemàtic.

Design, implementation and testing of an intelligent knowledge-based system for the supervisory control of a hot rolling mill

This paper describes the design, implementation and testing of an intelligent knowledge-based supervisory control (IKBSC) system for a hot rolling mill process. A novel architecture is used to integrate an expert system with an existing supervisory control system and a new optimization methodology for scheduling the soaking pits in which the material is heated prior to rolling. The resulting IKBSC system was applied to an aluminium hot rolling mill process to improve the shape quality of low-gauge plate and to optimise the use of the soaking pits to reduce energy consumption. The results from the trials demonstrate the advantages to be gained from the IKBSC system that integrates knowledge contained within data, plant and human resources with existing model-based systems. (c) 2005 Elsevier Ltd. All rights reserved.

Opportunities for magnetospheric research with coordinated cluster and ground-based observations

ESA’s first multi-satellite mission Cluster is unique in its concept of 4 satellites orbiting in controlled formations. This will give an unprecedented opportunity to study structure and dynamics of the magnetosphere. In this paper we discuss ways in which ground-based remote-sensing observations of the ionosphere can be used to support the multipoint in-situ satellite measurements. There are a very large number of potentially useful configurations between the satellites and any one ground-based observatory; however, the number of ideal occurrences for any one configuration is low. Many of the ground-based instruments cannot operate continuously and Cluster will take data only for a part of each orbit, depending on how much high-resolution (‘burst-mode’) data are acquired. In addition, there are a great many instrument modes and the formation, size and shape of the cluster of the four satellites to consider. These circumstances create a clear and pressing need for careful planning to ensure that the scientific return from Cluster is maximised by additional coordinated ground-based observations. For this reason, ESA established a working group to coordinate the observations on the ground with Cluster. We will give a number of examples how the combined spacecraft and ground-based observations can address outstanding questions in magnetospheric physics. An online computer tool has been prepared to allow for the planning of conjunctions and advantageous constellations between the Cluster spacecraft and individual or combined ground-based systems. During the mission a ground-based database containing index and summary data will help to identify interesting datasets and allow to select intervals for coordinated studies. We illustrate the philosophy of our approach, using a few important examples of the many possible configurations between the satellite and the ground-based instruments.

A compact low-cost electronic hardware design for actuating soft robots

A low cost, compact embedded design approach for actuating soft robots is presented. The complete fabrication procedure and mode of operation was demonstrated, and the performance of the complete system was also demonstrated by building a microcontroller based hardware system which was used to actuate a soft robot for bending motion. The actuation system including the electronic circuit board and actuation components was embedded in a 3D-printed casing to ensure a compact approach for actuating soft robots. Results show the viability of the system in actuating and controlling siliconebased soft robots to achieve bending motions. Qualitative measurements of uniaxial tensile test, bending distance and pressure were obtained. This electronic design is easy to reproduce and integrate into any specified soft robotic device requiring pneumatic actuation.

The influence of area/volume ratio on microstructure and non-Ohmic properties of SnO2-based varistor ceramic blocks

Fundação de Amparo à Pesquisa do Estado de São Paulo (FAPESP)

Polycation-Based Gene Therapy: Current Knowledge and New Perspectives

At present, gene transfection insufficient efficiency is a major drawback of non-viral gene therapy. The 2 main types of delivery systems deployed in gene therapy are based on viral or non-viral gene carriers. Several non-viral modalities can transfer foreign genetic material into the human body. To do so, polycation-based gene delivery methods must achieve sufficient efficiency in the transportation of therapeutic genes across various extracellular and intracellular barriers. These barriers include interactions with blood components, vascular endothelial cells and uptake by the reticuloendothelial system. Furthermore, the degradation of therapeutic DNA by serum nucleases is a potential obstacle for functional delivery to target cells. Cationic polymers constitute one of the most promising approaches to the use of viral vectors for gene therapy. A better understanding of the mechanisms by which DNA can escape from endosomes and traffic to enter the nucleus has triggered new strategies of synthesis and has revitalized research into new polycation-based systems. The objective of this review is to address the state of the art in gene therapy with synthetic and natural polycations and the latest advances to improve gene transfer efficiency in cells.

Microstructure and electrical properties of (Ta, Co, Pr) doped TiO2 based electroceramics

The addition of different dopants affects the densification, mean grain size and electrical properties of TiO2-based varistor ceramics. This paper discusses the microstructural and electrical properties of (Ta, Co, Pr) doped TiO2 systems, demonstrating that some of these systems display electrical properties that allow for their use as low voltage varistor. Dopants such as Ta2O5 play a special role in the formation of barriers at the grain boundary and in the nonlinear behavior in TiO2-based systems. The higher values of nonlinear coefficient and breakdown electric field were obtained in the system just doped with Ta2O5 and CoO.

Low-voltage varistor based on (Sn,Ti)O-2 ceramics

A description is given of the nonohmic behavior obtained in (SnxTi1-x)O-2-based systems. A matrix founded on (SnxTi1-x)O-2-based systems doped with Nb2O5 leads to a low-voltage varistor system with nonlinear coefficient values of similar to9. The presence of the back-to-back Schottky-type barrier is observed based on the voltage dependence of the capacitance. When doped with CoO, the (SnxTi1-x)O(2)(.)based system presents higher nonlinear coefficient values (>30) than does the SnO2-based varistor system.

Recent research developments in SnO2-based varistors

This paper discusses some advances in research conducted on SnO2-based electroceramics. The addition of different dopants, as well as several thermal treatments in oxidizing and inert atmospheres, were found to influence the microstructure and electrical properties of SnO2-based varistor ceramics. Measurements taken by impedance spectroscopy revealed variations in the height and width of the potential barrier resulting from the atmosphere in which thermal treatments were performed. High nonlinear coefficient values, which are characteristic of high-voltage and commercial ZnO varistors, were obtained for these SnO2-based systems. All the systems developed here have potentially promising varistor applications. (C) 2004 Elsevier B.V. All rights reserved.

Knowledge-based risk management: Survey on Brazilian software development enterprises

A risks management, carried on in an effective way, leads the software development to success and may influence on the organization. The knowledge takes part of such a process as a way to help taking decisions. This research aimed to analyze the use of Knowledge Management techniques to the Risk Management in software projects development and the possible influence on the enterprise revenue. It had, as its main studying subject, Brazilian incubated and graduated software developing enterprises. The chosen research method was the Survey type. Multivariate statistical methods were used for the treatment and analysis of the obtained results, this way identifying the most significant factors, that is, enterprise's achievement constraining factors and those outcome achievement ones. Among the latter we highlight the knowledge methodology, the time of existence of the enterprise, the amount of employees and the knowledge externalization. The results encourage contributing actions to the increasing of financial revenue. © 2013 Springer-Verlag.