L’introduction des nouvelles technologies de l’information et de la communication dans les systèmes automatisés entraîne un accroissement de la complexité des fonctions qu’ils supportent. Cet accroissement de la complexité a un impact sur la sécurité des systèmes. En effet, leurs propriétés ne sont plus réductibles aux propriétés de leurs constituants pris isolément mais émergent d’un réseau d’interactions entre ces constituants qui peut être à l’origine de comportements néfastes et difficiles à prévoir. Notre conviction est que le développement sûr de ces systèmes doit combiner des approches pragmatiques orientées « système », qui tiennent compte du facteur d'échelle réel d'une automatisation pour appréhender le fonctionnement global du système et son architecture, avec des approches plus formelles qui permettent de s’assurer que les propriétés intrinsèques des constituants contribuent efficacement au respect des exigences « système » formulées par les utilisateurs. Le travail présenté dans ce mémoire définit donc une approche méthodologique basée sur le formalisme SysML (System Modeling Language) permettant l’identification, la formalisation et la structuration d’exigences globales relatives à un système, puis leur projection, sous forme de propriétés invariantes, sur une architecture de composants. La vérification des exigences de sécurité, repose alors, d’une part, sur un raffinement prouvé (par theroem proving) des exigences « système » permettant d’établir leur équivalence avec un ensemble de propriétés intrinsèques relatives à chacun des composants, et d’autre part, sur la vérification formelle (par model checking) de ces propriétés intrinsèques. / Introduction of new information and communication technology in automated systems leads to a growth of safety functions complexity. System properties are not limited to components properties, they issued from an interactions network that can introduces bad behaviour. Our conviction is that a safe development of such system must involve system oriented approaches in order to apprehend system global behaviour and architecture and more formal approaches allowing verifying that components properties satisfy end users system requirements We define a methodological approach based on SysML formalism (System Modelling Language) allowing global system requirements identification; formalisation and structuring in order to project these requirements on the system components architecture and so obtain local components properties. Then safety requirements verification is based in one hand on proved refinement (using theorem proving) of system requirements to components properties; and, in the other hand, on the formal verification (using model checking) of these components properties.

La vérification formelle des contrôleurs logiques a donné lieu à de nombreux travaux scientifiques cette dernière décennie. Elle permet de démontrer (obtention d'un niveau requis de sûreté de fonctionnement (SdF) des systèmes industriels, et tout particulièrement des systèmes critiques. Nos travaux portent sur la preuve des propriétés relatives à la qualité du service rendu par le système automatisé, que nous nommons des propriétés quantitatives. Par exemple, au lieu de vérifier que plusieurs produits ont effectivement été dosés avant d'enclencher un mélange puis une réaction chimique, il peut être important de prouver que la bonne quantité de ces produits a été dosée. Autre exemple, au lieu de prouver qu'un mobile s'arrête dans une position donnée, il peut être important de prouver que cet arrêt en position s'effectue avec une précision garantie. Ce sont de telles propriétés quantitatives que nous nous sommes attachés à être capables de prouver pour les systèmes à évènement discrets (SED), et plus exactement pour une sous classe des SED : les systèmes logiques. Dans ce mémoire nous explorons l'apport des automates hybrides pour la prise en compte simultanée du caractère discret du contrôleur et continu du processus. A cette fin, nous introduisons un formalisme d'automates hybrides à transitions typées et nous proposons une méthodologie de modélisation basée sur des automates modulaires génériques. La vérification est alors obtenue par le model checker PHAVer. Deux études de cas sont présentées en fin de mémoire.

L'introduction des nouvelles technologies de l'information et de la communication dans les systèmes automatisés entraîne un accroissement de la complexité des fonctions qu'ils supportent. Cet accroissement de la complexité a un impact sur la sécurité des systèmes. En effet, leurs propriétés ne sont plus réductibles aux propriétés de leurs constituants pris isolément mais émergent d'un réseau d'interactions entre ces constituants qui peut être à l'origine de comportements néfastes et difficiles à prévoir. <br />Notre conviction est que le développement sûr de ces systèmes doit combiner des approches pragmatiques orientées " système ", qui tiennent compte du facteur d'échelle réel d'une automatisation pour appréhender le fonctionnement global du système et son architecture, avec des approches plus formelles qui permettent de s'assurer que les propriétés intrinsèques des constituants contribuent efficacement au respect des exigences " système " formulées par les utilisateurs. <br />Le travail présenté dans ce mémoire définit donc une approche méthodologique basée sur le formalisme SysML (System Modeling Language) permettant l'identification, la formalisation et la structuration d'exigences globales relatives à un système, puis leur projection, sous forme de propriétés invariantes, sur une architecture de composants. La vérification des exigences de sécurité, repose alors, d'une part, sur un raffinement prouvé (par theroem proving) des exigences " système " permettant d'établir leur équivalence avec un ensemble de propriétés intrinsèques relatives à chacun des composants, et d'autre part, sur la vérification formelle (par model checking) de ces propriétés intrinsèques.

Disaster risk reduction policies and practitioners alike emphasise the importance of vulnerability reduction. However, the concept of vulnerability is highly dynamic, and research still strives to understand and capture its complexity. The purpose of this study was to improve the understanding of flood vulnerability in rural disaster-prone communities in Mozambique. To explore previous experiences of floods, I conducted semi-structured interviews with local risk committee members and community members in the lower Limpopo river basin. The findings were analysed with an analytical framework consisting of the Disaster Pressure and Release (PAR) model, drawing on political ecology and the Access model. Disaster was studied as a process revealing important factors, capabilities and strains affecting peoples’ vulnerability. This paper illustrated that rural communities in the lower Limpopo river basin are vulnerable to floods in a variety of ways. The findings presented unsafe conditions such as the fragile local economy, unsafe natural resources, strained physical resources and limited access to human and social capital. Several factors deriving from political, social and economic structures were found to influence specific forms of vulnerability expressed in relation to floods. Therefore, this paper contributes to new insights of how flood vulnerability can be described and explained in Mozambique.

Submitted by Izabel Franco (izabel-franco@ufscar.br) on 2016-10-06T18:14:46Z No. of bitstreams: 1 TeseEAMms.pdf: 1490434 bytes, checksum: e7a807666b453630ffb423774d2539b9 (MD5) / Approved for entry into archive by Marina Freitas (marinapf@ufscar.br) on 2016-10-20T13:51:46Z (GMT) No. of bitstreams: 1 TeseEAMms.pdf: 1490434 bytes, checksum: e7a807666b453630ffb423774d2539b9 (MD5) / Approved for entry into archive by Marina Freitas (marinapf@ufscar.br) on 2016-10-20T13:51:52Z (GMT) No. of bitstreams: 1 TeseEAMms.pdf: 1490434 bytes, checksum: e7a807666b453630ffb423774d2539b9 (MD5) / Made available in DSpace on 2016-10-20T13:52:00Z (GMT). No. of bitstreams: 1 TeseEAMms.pdf: 1490434 bytes, checksum: e7a807666b453630ffb423774d2539b9 (MD5) Previous issue date: 2016-03-23 / Coordenação de Aperfeiçoamento de Pessoal de Nível Superior (CAPES) / From the generalized normal distribution and concepts of the generalized autoregressive moving averages models we introduce the generalized normal-ARMA model as an alternative way to model time series exhibiting symmetry and tails that may be lighter or heavier when compared the normal distribution. We present application for proposed model using three time series in the hydrology, economy and publics policy areas. The proposed model is presented as good alternative when compared to ARMA model with normal distribution. We extended this model the case of the asymmetric time series. In this case we used the Box-Cox transformation, denoted by Box-Cox generalized normal ARMA. The particular case, when we use the logarithmic transformation is called generalized log-normal ARMA. We adjusted the models with transformation to the series on monthly average affluent streamflow of the Furnas and Sobradinho hydroelectric plants. We obtain the prediction values for the model with transformation, that are better when compared with the model without transformation. To treat time series that exhibit periodic in the correlation function we defined three extensions for periodic autoregressive model, called generalized normal periodic autoregressive model, generalized log-normal periodic autoregressive model and Box-Cox generalized normal periodic autoregressive model. We can observed that the series on monthly average affluent streamflow of the Furnas and Sobradinho hydroelectric plants have periodic correlation. We present two applications of periodic models from these series. In the models, we note that is not necessary the use of generalized normal distribution in every months, just in some the generalized normal distribution presented better results than the normal distribution. Finally, we define the generalized normal zero inflated distribution and the generalized normal zero inflated ARMA model for time series. Adopting the model for series that have zero inflation and the maximum likelihood method for estimation of parameters, we analyze the serie of the amount of rainfall in the city of São Carlos. / A partir da distribuição normal generalizada e dos conceitos do modelo autorregressivo e de médias móveis generalizado, introduzimos o modelo normal generalizada- ARMA, como alternativa para modelar séries temporais, que exibem simetria e caudas mais leves ou mais pesadas quando comparadas com a distribuição normal. Apresentamos aplicações do modelo proposto, usando três séries temporais, das áreas de hidrologia, políticas públicas e economia. O modelo proposto se apresentou como uma boa alternativa ao modelo ARMA com distribuição normal. Estendemos o modelo para o caso de séries que apresentam assimetria. Neste caso, utilizamos a transformação de Box-Cox, denotado por Box-Cox normal generalizada-ARMA. O caso particular quando utilizamos a transformação logarítmica é chamado de log-normal generalizada-ARMA. Ajustamos os modelos com transformação à séries de vazões das usinas hidrelétricas de Furnas e Sobradinho. Calculamos predições, que para o modelo com transformação, foram melhores, quando comparado ao modelo sem transformação. Com o objetivo de tratar séries que apresentam periodicidade na função de correlação, definimos três extensões do modelo autorregressivo periódico, chamando-os de modelo normal generalizada autorregressivo periódico, modelo log-normal generalizada autorregressivo periódico e modelo Box-Cox normal generalizada autorregressivo periódico. Constatamos que as séries de vazões das usinas hidrelétricas de Furnas e Sobradinho apresentam correlação periódica. Apresentamos duas aplicações dos modelos periódicos propostos usando estas séries. Nos ajustes dos modelos, notamos que não há necessidade da utilização da distribuição normal generalizada em todos os meses, mas em alguns a distribuição normal generalizada se sobressaiu em relação a distribuição normal. Por último, definimos a distribuição normal generalizada zero inflacionada e o modelo para séries temporais normal generalizada zero inflacionada-ARMA. Adotando o método de máxima verossimilhança e o modelo para séries que apresentam inflação de zeros, analisamos a série da quantidade de precipitação pluviométrica da cidade de São Carlos.