Título: Verificação de Sistemas de Tempo Real com Autômatos Temporizados: Teoria e Prática Resumo: Nesta palestra vamos apresentar, informalmente, Autômatos Temporizados e seu uso em verificação automática de Sistemas de Tempo Real. A palestra está divida em três partes. Na parte inicial, cobriremos a teoria básica de autômatos temporizados e verificação para permitir, na segunda parte, a apresentação da ferramenta UPPAAL, com algum exemplo de modelagem e verificação de sistema. Na terceira parte veremos alguns aspectos mais teóricos, mas não menos interessantes, sobre o que pode e não pode ser feito com autômatos temporizados. Veremos que se admitimos não-determinismo nos autômatos, dizer simplesmente se um autômato modela um sistema que exibe todos os possíveis comportamentos -- a universalidade -- se torna um problema "altamente indecidível". Veremos o que isso significa.