@MASTERSTHESIS{ 2008:232416061,
 	title = {Verifica??o de modelos uml de software embarcado com model checking},
 	year = {2008},
 	url = "http://tede.ufam.edu.br/handle/tede/2956",
 	abstract = "Os sistemas embarcados possuem ineg?vel import?ncia na sociedade atual. Eles possuem restri??es temporais (quando s?o de tempo real), de ger?ncia de consumo de energia, tamanho, peso etc que tornam o seu projeto e concep??o mais complexos do que os sistemas convencionais. Dado o grande n?mero de requisitos de todos os tipos, a alta complexidade dos softwares embarcados desenvolvidos bem como a grande possibilidade de cat?strofes significativas em caso de falha e por fim a grande press?o de mercado por produtos cada vez mais r?pido, fazem-se necess?rios m?todos que possam assegurar uma correta, r?pida por?m intuitiva especifica??o e concep??o dos projetos. Diante disso, o presente trabalho visa prover um m?todo que acrescente ao atual estado da arte. O objetivo do m?todo ent?o ? prover uma abordagem que colete uma especifica??o de software embarcado em uma nota??o semi-formal, orientada a objetos e amplamente aceita pela Ind?stria, que ? a Unified Modeling Language (UML), especificamente com seu Diagrama de Sequ?ncia, o
 qual ? apto para capturar os aspectos din?micos de um sistema e um mecanismo de tradu??o dessa nota??o para a nota??o formal SMV, apta a ser utilizada pelo model checker de mesmo nome. O objetivo do m?todo ? prover tamb?m um esquema de tradu??o dos diagramas de sequ?ncia em UML para uma nota??o formal, no caso a nota??o de Redes de Petri, o qual ? adequada para verifica??o formal, gerando sa?das de arquivos nos formatos APNN e PNML. O formato APNN ? adequado para ser usado no Model Checking Kit (MCK). Por fim, prover um esquema de tradu??o consultas de propriedade em alto n?vel para o formato
 de CTL puro adequado para ser usado no MCK e um programa em SMV e sua especifica??o 7 em CTL, formatos aptos a serem usados no model checker SMV. A verifica??o de propriedades
 ? apenas qualitativa, isto ?, que verificar? apenas propriedades de execu??o do software embarcado, em oposi??o ?s propriedades quantitativas de tempo por exemplo, comuns em softwares de tempo-real. Todas essas funcionalidades s?o realizadas por uma ferramenta, chamada Ambiente de Verifica??o Formal de Software Embarcado.",
 	publisher = {Universidade Federal do Amazonas},
 	scholl = {Programa de P?s-gradua??o em Inform?tica},
 	note = {Instituto de Computa??o}
}