Certificação de Composições de Serviços Web Semânticos
Serviços Web, Serviços Web Semânticos
Esta tese apresenta um m ́etodo de certificac ̧ ̃ao de composi ̧co ̃es de servi ̧cos web semˆanticos, o qual visa assegurar estaticamente sua corretitude funcional. O m ́etodo de certifica ̧ca ̃o consiste em duas dimenso ̃es de verifica ̧ca ̃o, denominadas base e funcional. A dimensa ̃o base ́e centrada na verifica ̧ca ̃o da corretitude da aplica ̧c ̃ao dos servi ̧cos web semaˆnticos na composi ̧ca ̃o, i.e., visa certificar que as invocac ̧ ̃oes de servic ̧o especificadas na composic ̧ ̃ao esta ̃o em conformidade com as respectivas defini ̧co ̃es dos servic ̧os. A certifica ̧ca ̃o desta dimensa ̃o explora a compatibilidade semˆantica entre os argumentos dados na invoca ̧c ̃ao e os parˆametros formais do servi ̧co web semˆantico. A dimens ̃ao funcional visa certificar que a composi ̧ca ̃o cumpre uma dada especifica ̧c ̃ao expressa na forma de pr ́e- e po ́s-condi ̧co ̃es. Esta dimens ̃ao ́e formalizada atrav ́es de um c ́alculo baseado na l ́ogica de Hoare. Especi- fica ̧co ̃es de corretitude parciais envolvendo composi ̧co ̃es de servi ̧cos web semaˆnticos podem ser derivadas a partir do sistema dedutivo proposto. Este trabalho caracteriza-se tamb ́em por explorar o emprego de um fragmento da lo ́gica descritiva, i.e., ALC, para expressar as especifica ̧co ̃es de corretitude parciais. Como forma de operacionalizar o m ́etodo de certifica ̧ca ̃o, foi desenvolvido um ambiente de suporte para a definic ̧ ̃ao das composic ̧ ̃oes de servi ̧cos web semaˆnticos, assim como os mecanismos necess ́arios para realizar a cer- tifica ̧ca ̃o. O m ́etodo de certifica ̧ca ̃o foi avaliado experimentalmente atrav ́es da aplica ̧ca ̃o em trˆes provas de conceito diferentes. As provas de conceito desenvolvidas possibilitaram avaliar de forma ampla o m ́etodo de certifica ̧ca ̃o proposto.