Análise, Verificação, e Síntese de Segmentos de Via de uma Malha Metroviária

Abstract: The aim of this work is to apply formal specification techniques to model real-time distributed systems. The formal models are based on hybrid automata. The target systems of this work are segments of subway network. Semi-automatic tools aid in the analysis and verification of the model. The model is also used to synthesize some important parameters of the system under consideration.



Resumo: O objetivo desse trabalho é a aplicação de técnicas de especificação formal para modelar sistemas distribuídos realistas. Os modelos formais são baseados em autômatos híbridos. O sistema alvo desse trabalho são segmentos de via de uma malha metroviária. A análise e a verificação do modelo considerado, bem como a síntese de certos parâmetros importantes do modelo, são auxiliadas por ferramentas semi-automáticas. Dessa forma, obteve-se de maneira automática a validação do comportamento do sistema descrito, bem como a síntese de parâmetros críticos para a operação da malha.

1999