Made available in DSpace on 2014-06-12T16:01:34Z (GMT). No. of bitstreams: 3 arquivo9570_1.pdf: 10214948 bytes, checksum: aa7a02b3d9f070abe8df0da8ecba3f1e (MD5) arquivo9570_2.pdf: 4029275 bytes, checksum: cc861547d5c8c1dffe8ed95c7bd9f40a (MD5) license.txt: 1748 bytes, checksum: 8a4605be74aa9ea9d79846c1fba20a33 (MD5) Previous issue date: 2003 / A fim de viabilizar maior interação entre profissionais da área de saúde, foram propostos protocolos de comunicação, dentre os quais destacamos: HL7, DICOYI, CORBAMed e GEHR. Decidimos especificar formalmente um subconjunto de um sistema de prontuário eletrônico, baseado no modelo G EHR, pois existe um interesse real nesta formalização, pela comunidade do projeto GEHR. As vantagens da formalização são óbvias: descobrir e corrigir erros nas fases iniciais da construção de software, especificar sistemas consistentes e livres de ambiguidades, obter implementações que comprovadamente cor­ respondem as especificações, enfim, aumentar a confiabilidade e a robustez do software e reduzir custos de desenvolvimento e evolução. Definimos urna estratégia adequada a especificação e analise de tais sistemas. Adotamos o uso integrado de UYIL-RT (extensão de UML para tempo real) e a linguagem formal CSP-OZ. Estas linguagens permitem uma expressão natural do modelo orientado a objetos do GEHR e o uso combinado destas notações oferece as vantagens do formalismo (csP-oz) como apelo prático da notação gráfica (L"ML-RT). Além disso, já existe uma técnica de verificação de modelos em CSP-OZ, utilizando a ferramenta FDR, que permite a verificação automática de algumas propriedades do sistema como, por exemplo, ausência de deadlock e livelock. Constatamos que a técnica de verificação de modelos em CSP-OZ não trata os aspectos de orientação a objetos como herança, a qual e essencial para especificação do GEHR. Para sanar este problema, definimos um padrão de projeto, em CSP, que incorpora as principais características de orientação a objetos, tais como classes, subclasses, criação e remoção dinâmica de objetos. Este padrão, juntamente com a técnica de verificação de modelos desenvolvida para CSP-OZ, permite a analise de especificação considerando herança. No padrão proposto, objetos são representados como processos. A criação de objetos e realizada através de urna função que recebe urna tupla representando o estado do objeto e retorna o processo correspondente. A remoção de um objeto e implementada por eventos que, via sincronização, coordenam a terminação do processo que representa o objeto. A principal contribuição do trabalho e o padrão de projeto e a sua utilização na especificação formal de um subconjunto do sistema de prontuário eletr6nico baseado em GEHR. Além do padrão de projeto, sugerimos duas outras abordagens em CSP, que mostram alternativas para modelar herança. A contribuição da especificação formal do GEHR dirige-se a produção de software complexo e real com alta qualidade. Os profissionais de saúde podem ter acesso a um subconjunto do sistema de prontuário sem ambiguidades e livre de erros. Um dos objetivos futuros e a formalização completa deste sistema