Especificação Abstrata do Núcleo de um Sistema Operacional e sua formalização na linguagem Z - Barreto, Luciano; Andrade, Aline; Duran, Adolfo; Lima, Caíque; Lima, Ademilson (Anais do Workshop de Sistemas Operacionais (WSO); 2010: Anais do VII Workshop de Sistemas Operacionais, 2010)
A especificação formal e verificação do núcleo de um sistema operacional constitui um dos mini desafios propostos pela comunidade de métodos formais no contexto dos Grandes Desafios em verificação de software (Grand Challenges) proposto por Tony Hoare. Este artigo apresenta uma proposta de kernel simples e correto (ainda que preliminar) especificada em Z, que simplifica a compreensão e verificação de componentes do sistema operacional.