Verificação e sintese de sistemas hibridos

• Main Author: Bonifácio, Adilson Luiz
• Other Authors: UNIVERSIDADE ESTADUAL DE CAMPINAS
• Format: Others
• Language: Portuguese
• Published: [s.n.] 2000
• Subjects: Linguagens formais; Modelagem
• Online Access: BONIFÁCIO, Adilson Luiz. Verificação e sintese de sistemas hibridos. 2000. 137p. Dissertação (mestrado) - Universidade Estadual de Campinas, Instituto de Computação, Campinas, SP. Disponível em: <http://www.repositorio.unicamp.br/handle/REPOSIP/275910>. Acesso em: 26 jul. 2018.; http://repositorio.unicamp.br/jspui/handle/REPOSIP/275910

Orientador: Arnaldo Vieira Moura === Dissertação (mestrado) - Universidade Estadual de Campinas, Instituto de Computação === Made available in DSpace on 2018-07-26T17:52:58Z (GMT). No. of bitstreams: 1 Bonifacio_AdilsonLuiz_M.pdf: 21453626 bytes, checksum: de7be74dafd77bc551c7395989d64b6f (MD5) Previous issue date: 2000 === Resumo: Sistemas distribuídos híbridos advêm da interconexão de sistemas de dinâmica contínua com sistemas de dinâmica discreta. A noção de autômatos híbridos oferece meios para a construção de especificações formais para tais sistemas. Autômatos híbridos são autômatos finitos, onde cada estado descreve um perfil dinâmico do sistema e cujas transições entre estados provocam alterações nestes perfis dinâmicos. Neste trabalho, alguns sistemas híbridos reais são modelados através de autômatos híbridos. Em seguida, os modelos construídos são verificados, usando-se das facilidades de uma ferramenta computacional. Além disso, alguns parâmetros importantes, que afetam o comportamento operacional dos modelos, têm seus valores sintetizados. Os sistemas alvo desse trabalho são segmentos de via de uma malha metroviária e um sistema de gerenciamento de tráfego aéreo. As verificações foram sempre conduzidas de maneira a garantir uma operação segura dos sistemas estudados. As sínteses realizadas contribuíram para determinar valores mais justos para os parâmetros operacionais enfocados, mantendo a segurança na operação dos sistemas alvo. === Abstract: Distributed hybrid systems result from the interplay of continuous and discrete dynamics systems. The notion of hybrid automata offers a way to formally specify such systems. A hybrid automaton is a finite state automaton, where each state is extended to contain a description for a system dynamie profile. Transitions between states model a change in the system dynamies. In this work, some real hybrid systems are modeled using the formalism of hybrid automata. Next, the models constructed are verified, using the support of a computational tool. Moreover, values are synthesized for some important parameters that affect the system operational behavior. The target systems treated here are segments of a subway mesh and an air traffice control system. The verification sessions aimed at certifying that the system operates safely. Results from the synthesis contributed to obtain tighter values for operational system parameters, while still guaranteeing its safe operation. === Mestrado === Mestre em Ciência da Computação