Introdução a lógica temporal linear. Verificação em alloy. Case study usando o sistema alloy na verificação do programa de uma aeronave.