| Resumo: |
Os factores humanos são responsáveis por uma grande percentagem de falhas em sistemas informatizados e essa percentagem tende a aumentar à medida que os métodos de desenvolvimento de software melhoram. Parece haver consenso em considerar que 60-90% de todas as falhas se devem a acções erradas levadas a cabo por humanos. Model checking tornou-se uma técnica de verificação útil tanto para hardware como para software. A tentativa de aplicar model checking à verificação de interacções humano-computador complexas era logicamente o passo seguinte. No entanto, os sistemas interactivos colocam um conjunto de desafios que as ferramentas tradicionais não conseguem endereçar de forma apropriada. Na última década a aplicabilidade de ferramentas de raciocínio automatizado à análise de questões de usabilidade a partir de modelos de sistemas interactivos tem sido investigada. Neste contexto o PI desenvolveu um protótipo (i2smv) que suporta um processo semi-automático de análise de questões comportamentais da interacção. Desenvolver um entendimento de como a tecnologia de verificação pode ajudar na avaliação de usabilidade não é suficiente. É também necessário suportar adequadamente o processo de verificação. Uma possibilidade é construir camadas em cima de ferramentas de verificação existentes que auxiliem no processo de raciocínio sobre questões relacionadas com usabilidade e tornem a ferramenta de utilização mais simples. Este projecto tem como objectivo o desenvolvimento do i2smv para uma ferramenta de modelação e análise mais útil. Isto possibilitará que ele funcione como uma plataforma de teste para técnicas de verificação formal aplicadas a sistemas interactivos. A ferramenta a criar chamar-se-á IVY (Interactors VerifYier). A ferramenta será modelar e espera-se que consista nos seguintes componentes: um editor de modelos, um editor de propriedades, um compilador, um visualizador de traços de comportamento e um componente de engenharia reversa. O passo de verificação será  |
Resumo
Os factores humanos são responsáveis por uma grande percentagem de falhas em sistemas informatizados e essa percentagem tende a aumentar à medida que os métodos de desenvolvimento de software melhoram. Parece haver consenso em considerar que 60-90% de todas as falhas se devem a acções erradas levadas a cabo por humanos. Model checking tornou-se uma técnica de verificação útil tanto para hardware como para software. A tentativa de aplicar model checking à verificação de interacções humano-computador complexas era logicamente o passo seguinte. No entanto, os sistemas interactivos colocam um conjunto de desafios que as ferramentas tradicionais não conseguem endereçar de forma apropriada. Na última década a aplicabilidade de ferramentas de raciocínio automatizado à análise de questões de usabilidade a partir de modelos de sistemas interactivos tem sido investigada. Neste contexto o PI desenvolveu um protótipo (i2smv) que suporta um processo semi-automático de análise de questões comportamentais da interacção. Desenvolver um entendimento de como a tecnologia de verificação pode ajudar na avaliação de usabilidade não é suficiente. É também necessário suportar adequadamente o processo de verificação. Uma possibilidade é construir camadas em cima de ferramentas de verificação existentes que auxiliem no processo de raciocínio sobre questões relacionadas com usabilidade e tornem a ferramenta de utilização mais simples. Este projecto tem como objectivo o desenvolvimento do i2smv para uma ferramenta de modelação e análise mais útil. Isto possibilitará que ele funcione como uma plataforma de teste para técnicas de verificação formal aplicadas a sistemas interactivos. A ferramenta a criar chamar-se-á IVY (Interactors VerifYier). A ferramenta será modelar e espera-se que consista nos seguintes componentes: um editor de modelos, um editor de propriedades, um compilador, um visualizador de traços de comportamento e um componente de engenharia reversa. O passo de verificação será realizado externamente pelo SMV. |