Made available in DSpace on 2016-08-17T14:52:53Z (GMT). No. of bitstreams: 1 Reginaldo Isaias Braga.pdf: 1510667 bytes, checksum: 681b1cdce694568db4239625f302fc05 (MD5) Previous issue date: 2004-07-02 / This thesis deals with implementation of a railway control interlocking simulator whose functional requirements can be adaptive, that is, modified, complemented or same redefined, through an approach based on Finite State Machines. Depending on its requirements, a controller of rail traffic can assume simple or critics characteristics in terms of safety or fault tolerance. The modeling based on the Finite State Machine approach provides the conditions for the adaptability of some functional requirements. This characteristic is emphasized better when we used automated tools of definition of state machines, which allow the easy integration with the remaining of the software application. A detailed discussion about safety's considerations in design of mission and safety critical systems is presented. Emphasis is given in the subjects related to the safety software. A methodology and tool (SpecTRM-RL) that implements it, derived of recent researches in safety software, is shown. These considerations are fundamental in the design and requirements analysis in railway s interlocking control systems. These kinds of systems can be classified as mission and safety critical and they are progressively migrating for relay based controllers to microprocessor-based controllers where in the whole or partly safety's requirements are implemented by software. Fault tolerance techniques either in software or hardware are fundamental in the context of this work. A selection of the most usual in systems that demand high reliability was detailed with the goal of emphasizing its potential application in the case study of a railway control-interlocking simulator. / Este trabalho trata da implementação de um simulador de controle de tráfego ferroviário cujos requisitos funcionais possam ser adaptáveis, isto é, modificados, complementados ou mesmo redefinidos, através de uma abordagem baseada em máquinas de estado finitas. Dependendo de seus requisitos, um controlador de tráfego ferroviário pode assumir características simples ou críticas em termos de segurança ou tolerância a falhas. A modelagem baseada na abordagem de máquinas de estado provê as condições para a adaptabilidade de alguns requisitos funcionais. Esta característica é melhor enfatizada quando usamos ferramentas automatizadas de definição de máquinas de estado, que permitem a fácil integração com o restante da aplicação. É apresentada uma discussão detalhada sobre as considerações de segurança que devem ser seguidas em um projeto de missão e segurança crítica, onde é dada ênfase nas questões relacionadas à segurança do software. Uma metodologia e ferramenta (SpecTRM-RL) que a implementa, derivada de pesquisas recentes em software de segurança é mostrada. Estas considerações desempenham um papel fundamental no projeto e análise de requisitos em sistemas de controle metroferroviários. Por serem estes classificados como de missão e segurança críticas e principalmente por estarem migrando gradativamente de dispositivos com lógica de controle baseada em relês para controladores microprocessados onde no todo ou em parte os requisitos de segurança são implementados por software. Também de fundamental importância no contexto deste trabalho são as técnicas de tolerância a falha tanto em hardware como em software. Uma seleção das mais usuais em sistemas que demandam elevada confiabilidade foi detalhada com objetivo de enfatizar a aplicabilidade no estudo de caso de um simulador de intertravamento ferroviário.

<p>The impact of computer programs in safety-critical systems has increased in the past decades and computer-based systems can now be found in a wide range of applications. </p><p>A new approach for developing dependable systems is documenting all design rationale that affects safety using Intent Specifications. A recent approach for developing complex systems efficiently and in an upgradeable manner is Component-Based System Engineering. In this thesis, these approaches are combined in the development and upgrade of a Remote Robot Control Unit by using the tool SpecTRM. </p><p>The case study showed that Intent Specifications and CBSE could successfully be combined. The tool SpecTRM was also studied during this work. It showed that traceability is of great importance during system upgrades. Since SpecTRM does not support formal verification of safety properties in design models, the SpecTRM-RL models were translated to Esterel code. Further analysis showed that functional verification can be efficient and useful when using the automatic model-checking tool available in Esterel Studio. This work also proposes a practical guideline for system upgrades in component-based systems, presented as the Sigma model. </p><p>The work also showed some shortcomings. First of all, the tool SpecTRM is at an early development stage and not yet mature for industrial use. Secondly, neither of the two languages SpecTRM-RL and Esterel was expressive enough for some of the numerical computations and data-exchange structures needed for navigation in the system. Finally, the verifier was not able to prove any data properties since valued signals are abstracted into pure signals during verification in Esterel Studio.</p>

The impact of computer programs in safety-critical systems has increased in the past decades and computer-based systems can now be found in a wide range of applications. A new approach for developing dependable systems is documenting all design rationale that affects safety using Intent Specifications. A recent approach for developing complex systems efficiently and in an upgradeable manner is Component-Based System Engineering. In this thesis, these approaches are combined in the development and upgrade of a Remote Robot Control Unit by using the tool SpecTRM. The case study showed that Intent Specifications and CBSE could successfully be combined. The tool SpecTRM was also studied during this work. It showed that traceability is of great importance during system upgrades. Since SpecTRM does not support formal verification of safety properties in design models, the SpecTRM-RL models were translated to Esterel code. Further analysis showed that functional verification can be efficient and useful when using the automatic model-checking tool available in Esterel Studio. This work also proposes a practical guideline for system upgrades in component-based systems, presented as the Sigma model. The work also showed some shortcomings. First of all, the tool SpecTRM is at an early development stage and not yet mature for industrial use. Secondly, neither of the two languages SpecTRM-RL and Esterel was expressive enough for some of the numerical computations and data-exchange structures needed for navigation in the system. Finally, the verifier was not able to prove any data properties since valued signals are abstracted into pure signals during verification in Esterel Studio.