Gerador de protótipos de interfaces gráficas para o IVY Workbench

Universidade do Minho Escola de Engenharia Departamento de Informática João Miguel Matela Aidos Manso de Araújo Gerador de protótipos de interfaces gráficas para o IVY Workbench Dissertação January 2020 Universidade do Minho Escola de Engenharia Departamento de Informática João Miguel Matela Aidos Manso de Araújo Gerador de protótipos de interfaces gráficas para o IVY Workbench Dissertação Master dissertation Master Degree in Computer Science Dissertation supervised by José Francisco Creissac Freitas Campos Rui Miguel Silva Couto January 2020 DIREITOS DE AUTOR E CONDIÇÕES DE UTILIZAÇÃO DO TRABALHO POR TERCEIROS Este é um trabalho académico que pode ser utilizado por terceiros desde que respeitadas as regras e boas práticas internacionalmente aceites, no que concerne aos direitos de autor e direitos conexos. Assim, o presente trabalho pode ser utilizado nos termos previstos na licença abaixo indicada. Caso o utilizador necessite de permissão para poder fazer um uso do trabalho em condições não previstas no licenciamento indicado, deverá contactar o autor, através do RepositóriUM da Universidade do Minho. Licença concedida aos utilizadores deste trabalho Atribuição CC BY https://creativecommons.org/licenses/by/4.0/ i DECLARAÇÃO DE INTEGRIDADE Declaro ter atuado com integridade na elaboração do presente trabalho académico e confirmo que não recorri à prática de plágio nem a qualquer forma de utilização indevida ou falsificação de informações ou resultados em nenhuma das etapas conducente à sua elaboração. Mais declaro que conheço e que respeitei o Código de Conduta Ética da Universidade do Minho. ii GERADOR DE PROTÓTIPOS DE INTERFACES GRÁFICAS resumo A interface de um programa é um elemento importante na experiência que o utilizador tem com o software, pois constitui o principal método de interação com a lógica do programa. A existência de métodos fiáveis de verificação de sistemas de software permite o a conceção destes de acordo com a especificação e, em casos mais críticos, evitar erros com consequências graves. Estes métodos rigorosos, no entanto, contrastam com a prática mais comum no desenho de interfaces. Um dos métodos mais utilizados para o desenho e avaliação de interfaces é a prototipagem. Os protótipos permitem transmitir aspetos do design da interface e até avaliar a sua usabilidade, mas não oferecem as garantias sobre o seu funcionamento que os métodos de verificação oferecem. O IVY Workbench é uma ferramenta que suporta a modelação do comportamento de sistemas interativos e a verificação formal dos mesmos. A ferramenta contém um conjunto de plugins que suportam o processo de modelação e análise, incluindo um editor de modelos, um verificador de propriedades e um animador. Este último permite visualizar e interagir com os modelos, mas não suporta associá-los a mockups representativos das interfaces. A interação com os modelos facilita a sua validação por parte de quem os está a desenvolver. Não facilita, no entanto, a comunicação com os potenciais clientes do sistema modelado, para quem um protótipo será um meio mais eficaz de comunicação. Neste documento propõe-se uma solução para o problema acima, assente no desenvolvimento de um novo plugin capaz de suportar a construção e animação de protótipos de sistemas interativos modelados no IVY. É descrito todo o processo de desenvolvimento, desde o levantamento de requisitos, até exemplos de aplicação que permitem demonstrar as novas funcionalidades existentes. palavras-chave Interfaces com o Utilizador, Prototipagem, Modelação e análise formais iii A GENERATOR OF USER INTERFACE PROTOTYPES abstract A program’s interface is the most important element in the user’s experience with the software, because it is the primary method through which the user interacts with the program’s logic. The availability of reliable software verification methods allows its conception according to specification and, in critical cases, to avoid errors with grave consequences. These rigorous methods, however, are in contrast with the traditional approaches to user interface design. One of the most used methods for designing and evaluating interfaces is prototyping. Prototypes allow communication of design and usability aspects of a software system, but don’t offer any guarantees about their behaviour. IVY Workbench is a tool that supports modeling interactive system’s behavior and their respective formal verification. The tool contains a set of plugins that enable the modeling and analysis process, including a model editor, a trace analyzer and an animator. This last feature allows visualization and interaction with models but doesn’t support linking them with mockups that represent them. Model interaction makes it easier for developers to validate its behavior. However, it doesn’t facilitate the communication of the system’s behavior to potential clients, to which a prototype would be the most efficient communication path. In this document a solution to the above problem is presented, based on the development of a new plugin that will support the construction and animation of prototypes of interactive systems modeled in IVY. The document describes the undertaken development process, from requirements elicitation to practical examples that help demonstrate the new available features. keywords User Interfaces, Prototyping, Formal analysis and modeling iv CONTEÚDO 1 introdução 1 1.1Prototipagem 1 1.2IVY Workbench 2 1.3Objetivos 3 1.4Estrutura 3 2 requisitos para um plugin de prototipagem 5 2.1IVY Workbench 5 2.1.1Especificação 5 2.1.2Exemplo 7 2.1.3AniMAL 9 2.2CogTool 9 2.3PVSio-Web 12 2.4Discussão do CogTool e PVSio-Web 14 2.5Requisitos 14 3 formatos,programas de esboço e método de importação dos mockups 17 3.1Ferramentas de criação de mockups 17 3.1.1Exemplo Base 18 3.1.2Balsamiq Mockups 18 3.1.3Pencil Project 20 3.1.4Mockplus 21 3.1.5Análise 23 3.2Formato do Mockup 23 3.2.1Utilização de imagens raster 24 3.2.2Utilização de formatos estruturados 24 3.2.3Análise dos formatos de exportação 24 3.3SVG 26 3.3.1Bibliotecas 28 3.4Conclusão 29 4 o plugin “prototyper”31 4.1Fluxo de Trabalho 31 4.2Arquitetura 32 4.3Funcionalidades 35 v Conteúdo vi 4.4Conclusão 40 5 exemplos de aplicação 41 5.1Portão de garagem 41 5.2Bomba de infusão 44 5.3Relógio multi-funções 47 5.4Análise 52 6 conclusão 54 6.1Resumo 54 6.2Análise 55 6.3Trabalho Futuro 57 LISTA DE FIGURAS Figura 1Representação tabular da execução de um modelo descrito no IVY 3 Figura 2Arquitetura do IVY Workbench (Couto and Campos,2019)6 Figura 3Exemplo de uma sequência de ações no plugin AniMAL 10 Figura 4Interface do CogTool 11 Figura 5Arquitetura do PVSio-Web 13 Figura 6Exemplo de um modelo no PVSio-Web 13 Figura 7Caption 18 Figura 8Exemplo base replicado no Balsamiq Mockups 19 Figura 9Exemplo base replicado no Pencil 21 Figura 10 Exemplo base replicado no Mockplus 22 Figura 11 Figura de exemplo para demonstração da sintaxe SVG 27 Figura 12 Diagrama de atividades que especifica o fluxo de trabalho esperado para o uso do plugin 32 Figura 13 Estrutura do plugin 33 Figura 14 Diagrama de sequência que exemplifica as interações efetuadas ao importar um SVG 34 Figura 15 Dados de input e output que o “Prototyper” processa 35 Figura 16 Esquema representativo dos canais que o “Prototyper” subscreve e o seu fluxo de informação 36 Figura 17 Interface do plugin Prototyper 37 Figura 18 Janela popup para definir as propriedades de elementos interativos 39 Figura 19 Exemplo do realce de um elemento selecionado na tabela de elementos disponíveis 40 Figura 20 Caption 42 Figura 21 Janela de configuração dos valores do atributo com os ecrãs do mockup 43 Figura 22 Janela de animação do “Prototyper” 44 Figura 23 Protótipo da bomba de infusão criado no Pencil com as suas duas camadas 46 Figura 24 Janela de configuração de atributos com elementos textuais do protótipo 47 Figura 25 Animação da bomba de infusão em execução 48 Figura 26 Protótipo do relógio criado no Pencil com as suas duas camadas 51 vii 1.3. Objetivos 3 Figura 1: Representação tabular da execução de um modelo descrito no IVY dispõe para análise de modelos. Observe-se que a tabela contém informações sobre o valor que os atributos tomam em cada um dos estados de execução e as ações executadas. Os dados apresentados constituem informação valiosa para indivíduos versados na análise de modelos formais, mas são de pouca utilidade para outras pessoas envolvidas na conceção do sistema. Para estes últimos, um protótipo seria uma forma melhor de apresentar o comportamento da interface. Neste documento propõe-se uma solução ao problema de comunicação mencionado, acrescentando a capacidade de construção de protótipos ao IVY Workbench. 1.3 objetivos Propõe-se o desenvolvimento de uma nova funcionalidade que acrescentará capacidades de construção de protótipos ao IVY. A criação dos protótipos deverá passar pela importação de mockups do sistema descrito, gerados em ferramentas de desenho de interfaces. Esses mockups serão depois mapeados ao modelo especificado no IVY. Com o mapeamento realizado, poder-se-á iniciar a animação do mesmo, onde a execução do modelo será visualizada pelos mockups importados. Na sua essência, pode-se descrever esta nova funcionalidade como uma visualização gráfica da funcionalidade de execução do modelo descrita na secção anterior. Neste documento serão expostos todos os detalhes sobre a conceção e implementação desta nova funcionalidade no IVY. 1.4 estrutura O documento encontra-se estruturado em seis capítulos. No capítulo 2será descrito o IVY Workbench, o seu modo de funcionamento e as funcionalidades em oferta. Esta análise será acompanhada por um exemplo da linguagem de especificação dos modelos, para compreender as capacidades de representação do comportamento dos mesmos. Ainda no mesmo capítulo será realizada uma análise a ferramentas de análise de sistemas semelhantes ao IVY, com um foco no método utilizado para a representação visual dos sistemas. O objetivo passa por retirar ideias e conceitos sobre como esta representação será implementada na 1.4. Estrutura 4 nova funcionalidade. Após esta análise preliminar e uma compreensão do modo de funcionamento do IVY e das suas capacidades, serão elaborados um conjunto de requisitos funcionais para a nova funcionalidade. Estes requisitos irão direcionar o desenvolvimento da nova funcionalidade para melhor cumprir os objetivos impostos e mitigar o problema da comunicação dos modelos descritos no IVY. No capítulo 3será especificado o mockup que contem a representação gráfica do modelo, como este deverá ser estruturado, o(s) programa(s) que o utilizador deverá utilizar para a sua criação e as bibliotecas que suportarão a manipulação do mesmo. No capítulo 4procede-se à descrição da nova funcionalidade, da sua arquitetura e o seu modo de funcionamento. No capítulo 5serão expostos um conjunto de exemplos para complementar a análise da funcionalidade implementada e demonstrar as capacidades da mesma. Por último, na conclusão será realizado um resumo de todo o conteúdo exposto no documento, uma análise dos resultados obtidos e discussão de trabalho futuro. 2 REQUISITOS PARA UM PLUGIN DE PROTOTIPAGEM Nesta secção analisam-se três ferramentas relevantes para os objectivos da dissertação. Será analisada a ferramenta sobre a qual o desenvolvimento da nova funcionalidade irá incidir, o IVY Workbench. Pretende-se detalhar as funcionalidades que já existem, e as lacunas que este projeto se propõe a resolver. Serão também analisadas o CogTool e o PVSio-Web, duas ferramentas de análise de interfaces com objetivos semelhantes ao IVY, mas com abordagens diferentes tanto quanto ao tipo de análise suportado, como quanto ao modo de representação da lógica da interface. Esta análise será efetuada no contexto de recolha de requisitos. Finalmente, com os conceitos retirados da análise efectuada, serão identificados os requisitos para um plugin que permita gerar protótipos a partir dos modelos do IVY. 2.1 ivy workbench Nesta secção será detalhado o IVY, a especificação dos modelos em MAL e as funcionalidades disponíveis para a animação de modelos, mais concretamente o plugin AniMAL. 2.1.1Especificação O IVY Workbench é uma ferramenta dedicada à modelação e análise de comportamento de interfaces (Campos and Harrison,2009). Foi desenvolvida no DI da UM recorrendo ao model checker NuSMV como motor de verificação. A ferramenta está programada em Java. O objetivo da ferramenta passa pela análise do comportamento de um sistema a partir de um modelo deste. Para este propósito, recorre a MAL para descrever os modelos (Ryan et al.,1991). A linguagem MAL permite descrever: •Ações - definem as interações possíveis do sistema; •Atributos - definem as variáveis do sistema; •Axiomas - definem o comportamento do sistema com base nas ações e atributos definidos. 5 2.1. IVY Workbench 6 Figura 2: Arquitetura do IVY Workbench (Couto and Campos,2019) Os modelos podem ser validados face a propriedades da interface expressas em CTL (Clarke et al.,1983). O IVY utiliza um compilador que analisa os modelos especificados em MAL e os compila para a linguagem de entrada do model checker NuSMV (Cimatti et al.,2002), para que seja realizado o passo de verificação formal das propriedades definidas em CTL. Após a verificação, o IVY permite analisar os resultados da mesma (em caso de falha, na forma de comportamentos da interface que não obedecem à propriedade verificada), assim como modificar essas mesmas propriedades e acrescentar novas para investigar cenários adicionais de utilização. Para auxiliar na verificação dos modelos existem o visualizador de traços (Trace Analyzer) e o animador de modelos (AniMAL). O Trace Analyzer permite a análise dos resultados da verificação das propriedades. Já o AniMAL permite interagir com o modelo e criar uma sequência de ações, partindo do estado inicial do mesmo. Esta funcionalidade é útil para melhor visualizar que ações são possíveis em que estados, prevenindo assim possíveis falhas no modelo. A Figura 2apresenta a atual arquitetura do IVY. Nesta, é possível observar a estrutura modular da ferramenta. Ao nível mais baixo, o núcleo (IVY Framework) fornece as funcionalidades essenciais, como a infraestrutura da interface com o utilizador e o sistema de comunicação entre plugins e serviços. No nível intermédio existem os serviços que fornecem funcionalidades essenciais à própria aplicação. Estes são usados pelos plugins e não são expostos ao utilizador. Por último, na camada superior existem os plugins que fornecem as 2.1. IVY Workbench 7 ferramentas com que o utilizador irá interagir, como o editor de modelos, ou visualizador de propriedades. A comunicação entre os plugins e os serviços pode ser efetuada de duas formas (Couto and Campos,2019): •Sistema de mensagens, onde se implementa o padrão de publicador-subscritor. Os plugins podem criar canais, subscrever a canais existentes, publicar mensagens e receber notificações dos canais subscritos. •Sistema de memória partilhada, onde um plugin pode colocar informação na forma de um par chave-valor. Esta informação pode ser acedida por qualquer outro plugin. A nova funcionalidade será desenvolvida como um novo plugin do IVY. 2.1.2Exemplo Com a intenção de demonstrar as funcionalidades que o IVY dispõe, desenvolveu-se o exemplo de um portão de garagem, descrito na Listagem 2.1. O portão é controlado por um comando e dois sensores e pode encontrar-se num dos seguintes estados: •Aberto •Fechado •A abrir •A fechar O comando é utilizado para abrir e fechar o portão e cada um dos sensores deteta se o portão está aberto ou fechado. Caso o portão esteja a efetuar uma ação, como a abrir ou fechar, também é possível pressionar o comando para reverter a ação. A definição do modelo consiste em quatro partes: os tipos, os atributos, as ações e os axiomas. Analisando a listagem 2.1, o tipo encontra-se definido na segunda linha. Este é depois associado a atributos do modelo, e indica os valores que estes podem tomar. No modelo do portão aqui representado, na linha 6verifica-se que o atributo situacao pode tomar valores do tipo Movimento. Depois pode-se definir as ações que se podem realizar: a ação relacionada com o pressionar do comando, o Ac na linha 8, e as ações relacionadas com os sensores, Ia na linha 9eIf na linha 10. De notar a notação [vis] presente em algumas das definições para demarcar ações efetuadas pelos utilizadores e atributos presentes na interface. 2.1. IVY Workbench 8 1types 2Movimento = { a_abrir , a_fechar , aberto , fechado } 3 4interactor main 5attributes 6[ vis] situacao : Movimento 7actions 8[vis ] Ac 9Ia 10 If 11 axioms 12 [] situacao = fechado 13 situacao = fechado -> [Ac] situacao ’ = a_abrir 14 situacao = a_abrir -> [ Ac] ( situacao ’ = a_fechar ) 15 situacao = a_fechar -> [ Ac] ( situacao ’ = a_abrir ) 16 situacao = a_fechar -> [ If] ( situacao ’ = fechado ) 17 situacao = a_abrir -> [ Ia ] ( situacao ’ = aberto ) 18 per (Ia) -> situacao = a_abrir 19 per (If) -> situacao = a_fechar 20 situacao = aberto -> [ Ac] ( situacao ’ = a_fechar ) Listagem 2.1: Modelo de um portão de garagem em MAL Por último, da linha 12 até ao final encontram-se os axiomas, que definem o comportamento do sistema. A fim de melhor perceber a estrutura dos axiomas, apresenta-se um exemplo retirado da linha 15 da listagem 2.1 A declaração à esquerda da implicação (->) indica uma guarda. Se esta for verdadeira, a ação presente à direita da implicação poderá ser executada. A ação encontra-se rodeada por parêntesis retos. A expressão a seguir à ação, rodeada por parêntesis, indica qual será o estado após a execução da ação. A pelica é utilizada para referir o valor do atributo após a execução da ação. Traduzindo a expressão para linguagem corrente, se o portão estiver a fechar, ao pressionar o comando, o portão irá reverter a ação que estava a ocorrer e passará para o estado a_abrir. Observa-se também uma notação adicional na Listagem 2.1. Nas linhas 18 e19 é utilizado o operador “per“. Este operador é utilizado na definição de pré-condições para a execução de ações. Por exemplo, na linha 18, a ação Ia (correspondente ao despoletar do sensor do portão aberto) só pode ser executada se o portão estiver no estado a_abrir. Após a definição do modelo, é possível compilá-lo para a linguagem de entrada do model checker NuSMV, como especificado no início da secção. De seguida, é possível efetuar a verificação de propriedade e a análise dos resultados, recorrendo ou ao Trace Analyzer ou ao AniMAL. Na secção seguinte será detalhado o AniMAL, devido aos objetivos entre este 2.2. CogTool 9 e o plugin planeado: ambos pretendem facilitar a análise do comportamento do modelo através da sua demonstração no momento de execução. 2.1.3AniMAL O AniMAL constitui um dos vários plugins do IVY que acrescentam funcionalidades de análise e verificação aos modelos introduzidos. O nome AniMAL deriva da conjugação dos termos Animador e MAL, e indiciam o propósito que este plugin serve. Este utiliza um formato tabular para demonstrar, passo a passo, o valor que os atributos tomam na execução do modelo. O utilizador define quais as ações a executar que irão fazer progredir o estado de execução. Na Figura 3encontra-se um exemplo de uma sequência de execução possível do modelo exposto na Listagem 2.1. A sequência pode ser visualizada na tabela apresentada no lado direito da interface. A sequência de execução pode ser visualizada na tabela apresentada no lado direito da interface. Nesta tabela, cada coluna representa um estado na execução do modelo, enquanto nas linhas são representados os valores que os atributos tomam em cada estado. À esquerda encontram-se os controlos. Na secção entitulada ”ACTIONS” selecionam-se as ações que o utilizador quiser executar. Ligeiramente à direita, na secção ”STATE INFO”, apresentam-se as alterações que irão ocorrer caso a ação selecionada ocorra. No caso da Figura apresentada, a ação Ac encontra-se selecionada e o ”STATE INFO” demonstra o valor que estadoActual irá tomar caso a seleção se execute. É ainda possível ver na figura uma secção “CONSTRAINTS”, que permite controlar quais os estados considerados na execução/simulação do modelo, mas que não é relevante para a presente discussão. As representações gráficas utilizadas no AniMAL focam-se na representação dos modelos, das suas ações e atributos. Embora sejam úteis para análise, não suportam a comunicação do design da interface a não-peritos. Tal seria melhor conseguido com uma representação focada no design da interface (ou seja, com protótipos da interface). Pretende-se, agora, uma abordagem mais flexível e de mais fácil integração com o processo de conceção e desenvolvimento de sistemas interativos. Esta necessidade constitui o catalisador que impulsiona a criação de um novo plugin. Para auxiliar na fase inicial de conceção do plugin, nas secções seguintes serão analisadas ferramentas de modelação de sistemas com abordagens distintas para a representação dos mesmos. O estudo destas ferramentas irá auxiliar na recolha de requisitos. 2.2 cogtool O CogTool (John,2012) é uma ferramenta de modelação e análise de interfaces focada na análise da eficiência da interação. Para tal, incluí uma arquitectura cognitiva que pro- 2.2. CogTool 10 Figura 3: Exemplo de uma sequência de ações no plugin AniMAL cura capturar o modo como os utilizadores interagem. A ferramenta foi desenvolvida na Carnegie Mellon University pela equipa liderada por Bonnie E. John. Neste momento, a ferramenta não se encontra em desenvolvimento ativo, mas todos os materiais relacionados, incluindo o código fonte, estão disponíveis no GitHub1e num blog2criado pela investigadora mencionada. A última atualização ocorreu em 2014. Apesar disso, considera-se que os princípios e conceitos que esta aplica ainda são relevantes no contexto de visualização do comportamento de sistemas modelados. O principal objetivo da ferramenta é auxiliar no desenho de interfaces, para que efetuar tarefas comuns no programa seja intuitivo e rápido. O CogTool segue o seguinte princípio: “Tornar tarefas frequentes fáceis e tarefas menos frequentes possíveis” (John,2012, Capítulo 1.1). Para atingir este objetivo, a ferramenta aplica modelos preditivos de com1https://github.com/cogtool, visitado a 4de julho de 2019 2https://cogtool.wordpress.com/, visitado a 4de julho de 2019 2.2. CogTool 11 Figura 4: Interface do CogTool portamento humano. É possível elaborar a interface e definir as sequências de ações do utilizador paras tarefas pretendidas. O modelo cognitivo incorporado calcula, então, uma estimativa do tempo que o utilizador irá demorar a efetuar as tarefas. O modelo de previsões implementado é baseado na técnica KLM (Card et al.,1980). De forma sucinta, esta técnica tem em consideração diversos fatores relacionados com a realização de uma tarefa na interface, tais como o número de teclas a pressionar no teclado, a distância que o cursor irá percorrer e o nível de perícia do utilizador, só para listar alguns. Estes fatores são depois utilizados no cálculo do tempo que o utilizador irá demorar a completar a tarefa. A interface utiliza o conceito de storyboards ou frames, onde cada frame representa a interface num dado momento. Em cada um destes frames é possível definir uma imagem, representativa da interface a modelar, e sobrepor controlos sobre ela. A partir do momento em que os mockups e as transições entre eles estão definidos, é possível utilizá-los para demonstrar a execução de tarefas concretas (num estilo capture-replay). recorrendo ao modelo cognitivo que incorpora, a ferramenta é então capaz de calcular uma estimativa do tempo que demoraria cada uma das tarefas demonstradas. Calcula ainda uma série de indicadores 2.3. PVSio-Web 12 relacionados com a interacção, em particular relacionados com para onde o utilizador irá olhar ou o movimento das mãos. Na Figura 4observa-se uma tentativa de replicar o comportamento do exemplo do portão de garagem, descrito na secção 2.1.2. Cada storyboard representa um momento de execução do portão e os controlos para interação foram definidos para equivaler ao sensor e ao comando. No entanto, relembrando o objetivo do CogTool e o seu modo de funcionamento, nota-se que este modelo não se adequa à ferramenta. O principal objetivo do CogTool é auxiliar no desenho de interfaces de software através da análise de dados de interação. O portão de garagem não constitui um sistema de software nem se pode extrair dados de utilização deste. Note-se, no contexto desta dissertação, que o foco da análise do CogTool passa pela maneira como este efetua a representação visual do comportamento do sistema, e não pelo tipo de análises que se podem realizar dos modelos criados. Neste contexto, o uso do exemplo do portão adequa-se para retirar conclusões. Um aspeto interessante desta ferramenta é que o modelo utilizado para análise é derivado do protótipo e não o contrário. Embora essa não seja o tipo de abordagem que interessa prosseguir neste momento, o conceito de storyboards e controlos de interação indiciam uma direção que a representação gráfica dos modelos do IVY pode tomar. Cada valor que um atributo toma pode ser associado a vários mockups, representativos desses mesmos valores. 2.3 pvsio-web O PVSio-Web (Oladimeji et al.,2014) é uma ferramenta de modelação e análise formal de interfaces, com foco na construção de protótipos. Explicar o modo de funcionamento da ferramenta e dos princípios em que assenta pode ser feito com base no nome da mesma. A sigla PVS (Owre et al.,2001) significa Prototype Verification System, um demonstrador de teoremas que assenta numa lógica de ordem superior. O PVSio (Muñoz,2003) é uma extensão do PVS que facilita a utilização do avaliador de expressões (ground evaluator) do demonstrador de teoremas, adicionando um conjunto de facilidades de programação imperativa. Em particular, uma biblioteca de input/output. O PVSio-Web, utilizando o PVSio para comunicar com o PVS, suporta a construção e animação de protótipos, recorrendo ao avaliador de expressões para dinamicamente calcular o comportamento definido pelos modelos. Analisando a arquitetura da ferramenta na Figura 5, verifica-se que o PVSio-Web utiliza um cliente baseado em tecnologias Web, mais especificamente em NodeJS1, para abstrair a lógica do PVSio (Oladimeji et al.,2014, p. 3). O construtor de protótipos da interface gráfica interage com o servidor que contém os processos do PVSio e PVS através de WebSockets. Este modelo de funcionamento permite definir protótipos, importando imagens e 1https://nodejs.org/en/, visitado a 19 de outubro de 2019 3.1. Ferramentas de criação de mockups 19 Figura 8: Exemplo base replicado no Balsamiq Mockups lem a elementos de construção da interface, como botões, caixas de texto, ou figuras. Estes são selecionados através do painel superior representado na Figura 8. A moldura do dispositivo advém de uma imagem importada, pois a ferramenta não disponibilizou um widget para esta. Para representar as duas funções existentes no relógio, também se tirou proveito da funcionalidade de camadas, visível na Figura 8no painel lateral esquerdo onde se encontram as duas camadas. A porção visível do relógio no canvas de visualização encontra-se no modo de relógio, enquanto que na outra camada o relógio encontra-se no modo de cronómetro. Os botões para mudar de função encontram-se na lateral do dispositivo e são de cor vermelha. Em relação à variedade dos widgets em oferta, estes focam-se muito na construção de GUI (Graphical User Interfaces) de sistemas de software. O próprio website1salienta que 1https://balsamiq.com/, visitado a 8de outubro de 2019 3.1. Ferramentas de criação de mockups 20 um dos objetivos é a criação de mockups de baixa fidelidade, com o propósito de comunicar o design dos mesmos de forma simples e rápida. Este aspeto do programa dificulta a construção de mockups com um nível mais elevado de fidelidade com os widgets nativos. O Balsamiq Mockups também oferece opções de exportação. Os formatos suportados são: PNG,JSON e ZIP que contém ficheiros que detalham a configuração do protótipo. O Balsamiq Mockups, no seu todo, apresenta-se como uma opção interessante para a construção dos mockups. Apesar dos widgets em oferta serem principalmente direcionados para a construção de interfaces de software e de aspeto minimalista, a importação de imagens externas pode mitigar eventuais lacunas para a construção do mockup. Os formatos de exportação em oferta constituem um primeiro conjunto a considerar para importação no novo plugin. 3.1.3Pencil Project Ferramenta construída com base em tecnologias Web, recorrendo à framework Electron. O programa é open source e compatível com Windows, Linux e Mac OS. O código fonte encontra-se disponível no GitHub. Na Figura 9apresenta-se o exemplo base, definido anteriormente, replicado no Pencil. Como se pode observar no painel lateral esquerdo, a ferramenta oferece um conjunto de widgets para a construção do protótipo. Estes variam, desde formas básicas como texto, formas retangulares e circulares a elementos visuais associados a sistemas específicos como Android, iOS e Windows. Também há a opção de importar widgets adicionais na forma de coleções que podem ser instaladas através da internet (do repositório disponibilizado pela ferramenta), localmente, ou criadas pelo utilizador, utilizando a API disponibilizada (Evolus,2012), algo não possível no Balsamiq Mockups. Na Figura 9apresenta-se o exemplo base do relógio, replicado no Pencil, no modo de cronómetro. O processo de construção do dispositivo foi semelhante ao exposto para o Balsamiq Mockups. Foram utilizados diversos widgets para compor os elementos do relógio. Destaca-se o uso de uma coleção externa, transferida da internet, para descrever o aspeto do dispositivo em si. Esta coleção continha ícones do design “Material” da Google (Google,2019). Neste caso não houve necessidade, mas também há a opção de importação de imagens externas. Os dois modos do relógio também foram replicados utilizando camadas. As camadas são geridas na secção inferior da interface. O modo de relógio apresenta uma interface semelhante ao modo de cronómetro, sem o campo dos segundos na visualização e com a indicação “Clock”. O Pencil também oferece um conjunto de formatos de exportação. Tem os seguintes formatos disponíveis: PNG,HTML,PDF,SVG eODT. 3.1. Ferramentas de criação de mockups 21 Figura 9: Exemplo base replicado no Pencil No seu todo, o Pencil apresenta-se como uma proposta interessante para a criação dos protótipos que serão importados para o IVY. A funcionalidade de importação de coleções de widgets aumenta a flexibilidade disponível para a conceção de mockups para além do disponibilizado pelo Balsamiq Mockups. Adicionalmente, a maior oferta de formatos de exportação alarga o leque de opções para a importação no novo plugin. 3.1.4Mockplus Ferramenta orientada para o desenho de interfaces disponível para Windows, Mac e Android, neste momento não divulga em que tecnologias é que se baseia. Só dispõe de opções pagas, com uma oferta de 7dias de trial para experimentar todas as funcionalidades. A sua utilização exige também a criação de uma conta. A Figura 10 demonstra o protótipo replicado no Mockplus. As funcionalidades em oferta são semelhantes às ferramentas de prototipagem analisadas. O mockup é construído à base 3.1. Ferramentas de criação de mockups 22 Figura 10: Exemplo base replicado no Mockplus de widgets, com suporte para camadas para representar os diferentes estados do sistema. O dispositivo suporta uma forma circular na representação criada, devido ao uso do widget representativo de um relógio, considerado o mais próximo da visualização esperada. Os widgets oferecidos estão orientados para a construção de GUI de software. Existe, no entanto, mais variedade na oferta comparativamente ao Balsamiq Mockups graças à existência de uma coleção de widgets que representam items comuns (dispositivos, logótipos, ações, ...). No entanto, ao contrário das ferramentas analisadas até ao momento, não é possível importar imagens externas ou a importação de coleções de widgets externos como no Pencil. O Mockplus também tem uma seleção de formatos de exportação. Pode-se exportar para: PNG,JPEG,HTML e um executável, usado para visualizar o protótipo sem depender do Mockplus. Adicionalmente, pode-se exportar para uma vista de árvore dos componentes do protótipo. Esta vista de árvore meramente lista os componentes de forma textual, não contendo nenhuma informação sobre a sua constituição visual. O Mockplus oferece uma variedade de widgets que supera a oferta do Balsamiq Mockups. No entanto, a ausência da opção para importar imagens externas ou até definir um conjunto personalizado de widgets como o Pencil Project diminui o seu apelo, com base nos critérios definidos. Acrescentando a tudo isto o suporte à exportação de quatro formatos, sendo um deles um formato fechado do qual não se pode extrair a constituição do mockup, o executável. 3.2. Formato do Mockup 23 Pencil Project Balsamiq Mockups Mockplus Construção por widgets Utilização de Elementos Adicionais Coleções de Widgets e Imagens Imagens - Edição de Conteúdo Textual Opções de Exportação PNG, PDF, SVG, ODT e HTML PNG, JSON e ZIP PNG, JPG, HTML e árvore de componentes Tabela 1: Características das ferramentas de prototipagem 3.1.5Análise A Tabela 1resume a análise efetuada às ferramentas de construção de mockups. De todas, o Pencil é o que melhor cumpre os pontos de comparação definidos, permitindo a importação de imagens e coleções de widgets externas para complementar a oferta existente. Também oferece o maior número de formatos para exportação. A flexibilidade na construção do mockup pode ser verificada e avaliada com o uso e comparação das ferramentas. No entanto, a especificação do formato de exportação a adotar exige uma análise mais cuidada. A menção do número de formatos que cada ferramenta de esboço de mockups consegue exportar constitui uma métrica preliminar, necessariamente superficial, de análise, meramente indicativa dos formatos a partir dos quais se pode iniciar uma análise mais profunda. A definição do formato é crucial para o desenvolvimento do plugin, e irá ditar o rumo que este irá tomar durante o desenvolvimento. A escolha do formato a suportar deverá assentar no tipo de informação que este suporta, ou seja, como a informação sobre os mockups é representada. 3.2 formato do mockup Como definido na secção 2.5, os requisitos para o novo plugin especificam que o ficheiro que descreve o mockup deve estar num formato aberto (i.e. independente da plataforma onde foi criado e de livre utilização) e de fácil criação. Tal especificação levou à identificação de dois tipos de solução, e dois caminhos para o desenvolvimento desta nova funcionalidade: •Utilização de imagens raster como base para a definição dos protótipos. •Utilização de formatos estruturados como base para a definição dos protótipos. 3.2. Formato do Mockup 24 Ou seja, a diferença está entre ter o mockup representado numa imagem como PNG ou JPEG, ou em algum formato exportado por ferramentas de elaboração de mockups, nos quais é possível ter acesso à sua estrutura. 3.2.1Utilização de imagens raster A importação de imagens raster para o IVY deverá passar por escolher uma imagem representativa da interface do sistema modelado. Depois, será necessário definir os controlos sobre a imagem, representativos do comportamento definido no modelo, à semelhança do PVSio-Web ou CogTool, discutidos nas secções 2.2e2.3. A principal vantagem deste método é que a importação de imagens é uma tarefa que se realiza facilmente. Não há necessidade de analisar ou alterar o ficheiro que será importado. 3.2.2Utilização de formatos estruturados A importação de formatos estruturados possibilita a criação do protótipo com acesso aos componentes que definem o mockup. Este detalhe permitirá atribuir o comportamento do modelo a elemento/controlos do mockup importado, como botões ou elementos textuais. A um nível mais básico, esta abordagem permite replicar a representação de modelos com a importação de imagens raster. Neste cenário, certos elementos da estrutura interna do mockup seriam mapeados como áreas interativas. No entanto, o facto de se utilizar um formato estruturado possibilita casos de uso adicionais. O nível de integração mais profunda com o ficheiro que descreve o mockup importado poderá permitir uma definição mais granular do comportamento e automatização no mapeamento entre os elementos na interface e elementos no modelo. Como a utilização de formatos estruturados para a representação gráfica do modelo consegue abranger um maior número de casos de uso que a utilização de imagens raster, o desenvolvimento do plugin irá enveredar nesta direção. Para aprofundar a análise, serão detalhados os formatos exportados pelas ferramentas de esboço de mockups estudadas, de modo a reduzir os formatos em consideração para um único. 3.2.3Análise dos formatos de exportação Ao longo da descrição das ferramentas de esboço de mockups foram mencionados diversos formatos que a exportação do mockup poderá adotar. Procede-se com uma analise destes formatos e a informação contida neles. Desta análise, serão derivados um conjunto de critérios que serão utilizados para definir quais destes melhor se adequa à representação do mockup. 3.2. Formato do Mockup 25 Agregando toda a informação, os programas de prototipagem mencionados exportam os seguintes tipos de formato: •SVG; •JSON; •HTML; •PNG; •JPEG; •PDF; •ODT. Formatos como o PNG eJPEG encaixam na categoria de imagens raster, e portanto podem desde logo ser excluídos do processo de seleção. Com os formatos PDF eODT existe a possibilidade de extração de informação. Das ferramentas analisadas, apenas o Pencil consegue exportar para estes formatos. Acresce que, mesmo assim, a exportação é feita na forma de imagens raster embebidas nos ficheiros PDF ou ODT. O mesmo acontece com o HTML exportado pelo Pencil, que descreve o mockup recorrendo a imagens deste e das suas camadas. Depois, destacam-se os formatos ZIP e HTML. O primeiro é gerado pelo Balsamiq Mockups, enquanto o segundo é gerado tanto pelo Balsamiq como pelo Mockplus. O ZIP gerado pelo Balsamiq contém no interior ficheiros no formato proprietário, “bmml”, contendo texto XML e quaisquer imagens externas que o utilizador tenha importado para a conceção do mockup. O XML descreve a estrutura do mockup, com a peculiaridade que a representação gráfica dos widgets é omitida. Na prática, estes ficheiros “bmml” foram desenhados para serem importados apenas para o Balsamiq Mockups. Ao importar para a ferramenta, esta analisa o XML contido e verifica quais dos widgets internos a utilizar, na configuração especificada. Caso este formato viesse a ser utilizado pelo plugin planeado, seria necessário efetuar o mesmo processo para processar os mockups contidos nestes ficheiros. Tal exigiria implementar a biblioteca de widgets do Balsamiq Mockups (ou de aspeto e função semelhantes). Esta implementação aumentaria a complexidade do plugin, implicando aspetos semelhantes à incorporação da criação de mockups no mesmo e, acima de tudo, criaria uma dependência no Balsamiq Mockups e a eventuais alterações aos widgets em oferta em futuras iterações do programa. Todos estes elementos constituem aspetos que não cumprem os requisitos definidos para o plugin a desenvolver (especificamente os requisitos 1e2). 3.3. SVG 26 OHTML gerado pelo Mockplus exporta uma pasta com a estrutura de um projeto de uma página Web. Neste existe um index.html que pode ser aberto por qualquer navegador para visualizar o mockup com controlos interativos. Na estrutura de pastas existe um ficheiro XML denominado Main.xml, que descreve o mockup. Esta descrição consiste na menção de um conjunto de ficheiros SVG, contidos igualmente na estrutura de pastas, que no seu todo descrevem o mockup. Cada ficheiro SVG corresponde a um dos widgets utilizados na construção da interface. Apesar de ser um melhoramento em comparação com ZIP exportado pelo Balsamiq Mockups, uma das desvantagens deste formato de exportação acaba por ser a sua dependência em múltiplos ficheiros para descrever a totalidade de um só mockup. No caso do formato JSON, este só é gerado pelo Balsamiq Mockups. Este lista os widgets utilizados no mockup e algumas propriedades, como o posicionamento, tamanho e id, sem qualquer tipo de descrição gráfica destes. Assim, verificam-se os mesmos problemas levantados relativamente ao formato ZIP. Por fim, temos o formato SVG, gerado pelo Pencil. Este é exportado na forma de um único ficheiro. O SVG em si é um formato de imagens vetorial baseado em XML (Cohn et al.,2000). O ficheiro gerado pelo Pencil descreve todos os widgets como componentes, ou formas, dessa imagem vetorial. As camadas também se encontram especificadas no ficheiro. Após a análise cuidada de todos os formatos, o SVG exportado pelo Pencil é o formato que se apresenta como o candidato mais provável a ser utilizado pelo plugin, não aparentando apresentar nenhuma das desvantagens apontadas pelos outros formatos de exportação. De modo a melhor entender o formato e a maneira como a informação dos mockups é representada neste, na secção seguinte este o formato será melhor descrito. 3.3 svg OSVG (Cohn et al.,2000) é um standard desenvolvido pela W3C, com a primeira versão lançada em 2001 que continua a ser iterado até hoje, com uma nova versão a ser preparada (versão 2.0(David Dailey,2018)). Este formato foi desenvolvido para solucionar um dos principais problemas dos formatos de imagens mais comuns utilizados na internet: a escalabilidade. Tomando uma imagem no formato JPEG, por exemplo, quando se aumenta a proporção desta para além do especificado, começamos a notar a degradação da qualidade da imagem. Isto deve-se ao facto que este tipo de formatos apenas guardam um conjunto fixo de pixéis. Já com o SVG, guardam-se um conjunto fixo de formas, que depois são desenhadas pelo programa de visualização. Esta solução permite manter a definição da imagem, independentemente do seu tamanho. Claro que o SVG não substitui formatos de imagens raster, servindo ambos propósitos distintos. 3.3. SVG 27 Figura 11: Figura de exemplo para demonstração da sintaxe SVG De seguida apresenta-se um exemplo simples de uma figura criada em SVG e o seu código para demonstrar a sintaxe e características desta. 1<?xml version ="1.0 " encoding ="utf -8"?> 2<svg height =" 500 " version ="1.1 " width ="500 " xmlns =" http: // www .w3 . org /2000/ svg " > 3<g id=" layer1 " > 4<rect height =" 99.029755 " id=" rect3713 " style =" stroke - width:0 .26458332; fill: # ff2a2a " width =" 130.0238 " x=" 40.065475 " y=" 101.96429 "/ > 5<ellipse cx=" 104.69941 " cy=" 152.99106 " id=" path3715 " rx=" 100.1637 " ry=" 83.532738 " style =" fill:none ; stroke - width:5 .465; stroke: #0000 f9; stroke - opacity:1 ; stroke - miterlimit:4 ; stroke - dasharray:none "/ > 6</g> 7</svg > Listagem 3.1: Código SVG da figura de exemplo A Listagem 3.1descreve a Figura 11. O exemplo em si é de complexidade reduzida mas permite transmitir as características essências do formato. Como se verifica pela tag na linha 1, uma imagem SVG é descrita na linguagem de markup XML (Maler et al.,2004). Para utilizar as estruturas ou tags associadas ao SVG também é necessário definir o namespace do XML dentro do atributo xmlns no elemento svg, na linha 2. O elemento svg em si envolve sempre todas as estruturas utilizadas no documento e define atributos essenciais. Neste exemplo, os atributos especificados são o tamanho do canvas (width eheight) onde serão desenhadas as formas. Envolvendo a definição das formas encontra-se a tag g, nas linhas 3e6. Este é utilizada para agrupar formas, e permite separar diferentes elementos em grupos (ou camadas) distintas. No exemplo, o grupo composto pelo círculo e retângulo é denominado layer1. Por último, são definidas as formas em si que compõe a Figura 11. A tag rect na linha 3detalha o retângulo e a tag ellipse na linha 4detalha o círculo. Para declarar as propriedades das formas, são utilizados atributos nas tags associadas. Observe-se que o círculo não tem preenchimento, tendo apenas definido o traço. Para atingir este efeito há três componentes: 3.3. SVG 28 •style=“fill:none” - define o preenchimento do círculo como inexistente; •stroke-width:5.465 - define a espessura do traço do círculo; •stroke:#0000f9 - define a cor do traço do círculo com representação hexadecimal. O acesso a toda esta informação estruturada torna-se numa mais valia uma vez que pode ser extraída no planeado plugin para o IVY. Para além da definição de formas, também se podem definir animações, utilizando para o efeito linguagens de scripting como o Javascript, ou o SMIL. Nesta fase inicial não se prevê o uso desta funcionalidade mais avançada. 3.3.1Bibliotecas Oplugin será desenvolvido em Java, visto que o próprio IVY também faz uso da mesma linguagem. Nativamente, a linguagem de programação suporta a manipulação de dados XML1(necessária para identificação dos elementos no SVG) e ainda oferece a possibilidade de visualização, utilizando a biblioteca Java2D2para o efeito. No entanto, para facilitar o trabalho de desenvolvimento, decidiu-se investigar bibliotecas de manipulação de SVGs. Definiu-se a seguinte lista de funcionalidades que a biblioteca escolhida deverá fornecer. Esta encontra-se ordenana desde mais importante a menos importante: •Visualização do SVG - para apresentar os mockups na interface do programa; •Edição do SVG - poderá ser necessário para manifestar o comportamento do mockup e identificação dos elementos; •Documentação disponível - útil para expor a API em oferta e auxiliar o desenvolvimento. Batik O Batik (Foundation,2016) é uma biblioteca Java que fornece um conjunto de funcionalidades relacionadas com a visualização, manipulação e animação de SVG. Suporta um número elevado de elementos, atributos e propriedades da especificação SVG 1.1. Também vem acompanhado de bastante documentação e exemplos para ajudar na utilização de todas as funcionalidades existentes. SVG Salamander O SVG Salamander (blackears,2019) é uma biblioteca Java que, à semelhança do Batik, oferece um conjunto de funcionalidades para visualizar, manipular e animar SVG. O principal 1https://docs.oracle.com/javase/tutorial/jaxp/dom/readingXML.html, visitado em 5de julho de 2019 2https://www.oracle.com/technetwork/articles/java/svg-141884.html, visitado em 5de julho de 2019 4.3. Funcionalidades 35 Figura 15: Dados de input e output que o “Prototyper” processa Na Figura 16 identificam-se os canais a que o plugin subscreve, de onde os mesmos originam e a direção dos dados permutados. O “Prototyper” subscreve ao canal “model”, oferecido pelo IVY-core, que permite verificar se um modelo foi previamente importado para o IVY. Os outros dois canais, “nusmv” e “nusmv-out-sim”, são oferecidos pelo “Nusmvservice” e correspondem a dados de input eoutput da execução do modelo, respetivamente. O canal “nusmv” é utilizado para obter os valores dos atributos e uma listagem das ações possíveis no momento de execução e o canal “nusmv-out-sim” para enviar a ação executada pelo utilizador. Relativamente à memória partilhada, é nesta onde se pode obter os dados do modelo. O “IVY-core”, representado na Figura 16, publica os dados do modelo sempre que este for modificado ou compilado para a memória partilhada e o “Prototyper” recolhe-os. Esta troca é efetuada de forma assíncrona. O plugin assume que o modelo já foi definido anteriormente, como discutido no início desta secção, pelo que espera que estes dados já se encontrem colocados em memória partilhada. 4.3 funcionalidades A interface do novo plugin tem dois modos de funcionamento: o modo de edição e o modo de animação. O “Prototyper” inicia sempre no modo de edição. Neste é possível preparar 4.3. Funcionalidades 36 Figura 16: Esquema representativo dos canais que o “Prototyper” subscreve e o seu fluxo de informação a animação, gerindo a ligação entre o mockup e o modelo e ajustar os vários parâmetros. Depois de tudo estar configurado o modo de animação encontra-se disponível, onde é possível visualizar a interação definida. Ao selecionar o “Prototyper” dos vários separadores existentes no IVY, na parte superior da interface da Figura 17, a GUI do plugin será apresentada. A interface está dividida em três áreas principais, a partir das quais se pode aceder às funcionalidades disponibilizadas. A maior área, à esquerda, corresponde ao canvas de visualização do SVG importado. No topo encontram-se os controlos principais. Estes controlos incluem botões e dropdowns e são responsáveis por variadas funções: •Importar um ficheiro SVG; •Alternar entre os ficheiros SVG existentes (se houver mais do que um importado); •Alternar entre as camadas do SVG selecionado; •Eliminar SVG importado do plugin; •Configurar a associação entre elementos do SVG e atributos do modelo do IVY; •Apresentar informação sobre todos os elementos e as suas configurações; •Iniciar a animação. É possível importar mais do que um SVG representativo do protótipo, sendo que estes são selecionáveis pelo primeiro dropdown visível na Figura 17. Para alternar entre as camadas de cada SVG utiliza-se o segundo dropdown. 4.3. Funcionalidades 37 Figura 17: Interface do plugin Prototyper 4.3. Funcionalidades 38 A área à direita do canvas de visualização contém dois separadores, e em cada um destes existe uma tabela. Estas tabelas são denominadas “Available Elements” e “Active Elements”. A primeira tabela mencionada lista todos os elementos textuais e interativos identificados no mockup. Já a tabela dos elementos ativos lista os elementos configurados pelo utilizador. Quando se seleciona o separador dos elementos ativos também aparecem dois botões (demonstrados na Figura 17) que permitem remover as configurações realizadas pelo utilizador de um elemento selecionado da tabela ou de todos os elementos. O “Prototyper” cria a lista de todos os elementos interativos e textuais possíveis que existam dentro do SVG do protótipo no momento da importação. A identificação dos elementos que entram nesta lista é efetuada de forma diferente. Os SVG exportados pelo Pencil contêm neles uma identificação do tipo de forma. Por exemplo, caso o utilizador tenha utilizado os widgets de botões com estilo Android para construir o protótipo, estes encontrar-se-ão devidamente identificados no SVG. Esta informação é utilizada para identificar os elementos interativos que se podem associar a ações do modelo. Elementos interativos podem ser associados a ações do modelo e são reconhecidos pelo tipo. De um modo geral, só os widgets identificados como botões ou checkboxes é que são selecionados. Elementos textuais podem ser associados aos valores de um dado atributo do modelo e, à semelhança dos elementos interativos, também são reconhecidos pelo tipo. Qualquer elemento textual, como labels ou caixas de texto será selecionado. Qualquer dos dois tipos de elementos podem ser configurados de duas maneiras: duplo clicando na entrada da tabela dos elementos disponíveis (“Available Elements”) ou seleccionando-os diretamente no canvas de visualização. Quando se selecionam elementos interativos, a janela representada na Figura 18 aparecerá. Nesta pode-se definir a ação do modelo a associar ao elemento selecionado e o tipo de trigger para executar a ação no modo de animação. Há dois tipos de trigger: •Clique do rato - a ação será executada no modo de animação ao clicar no elemento; •Pressionar uma tecla no teclado - a ação será executada no modo de animação ao pressionar uma tecla especificada pelo utilizador. A janela de configuração dos elementos textuais pode ser visualizada na Figura 24 na página 47, no segundo exemplo de aplicação. Nesta janela aparece uma dropdown com a lista dos atributos do modelo ainda não configurados e uma visualização dos valores que o atributo atualmente selecionado pode tomar, para auxiliar o utilizador na seleção. Para distinguir entre elementos interativos e elementos textuais, a tabela dos elementos ativos contém uma segunda coluna, intitulada “Type”, que indica se o elemento foi associado a uma ação ou a um atributo (esta coluna pode ser vista na Figura 17). Quando se seleciona um dos elementos de qualquer uma das tabelas, o mesmo é realçado no canvas de visualização para auxiliar o utilizador (este efeito pode ser visto na Figura 19). Quando um 4.3. Funcionalidades 39 Figura 18: Janela popup para definir as propriedades de elementos interativos elemento é configurado, este é movido da tabela de elementos disponíveis (“Available Elements”) para a tabela dos elementos ativos (“Active Elements”). De forma idêntica, quando a configuração de um elemento é eliminada este é movido da tabela dos elementos ativos para a tabela dos elementos disponíveis. A configuração da associação entre protótipo e atributos do modelo efetua-se de duas maneiras distintas, mas complementares: •Associando atributos a elementos textuais no SVG (como já foi mencionado); •Associando os valores tomados por um atributo e a camadas específicas dos ficheiros SVG importados. A associação dos valores dos atributos aos SVG e as suas camadas significa que cada valor que o atributo possa tomar fica associado a uma camada de um SVG específico. Com os exemplos descritos no capítulo seguinte, esta funcionalidade será exemplificada. Para configurar esta associação, o utilizador pressiona o botão entitulado “Setup Screen(s)” nos controlos superiores, visíveis na Figura 17. Ao selecionar este botão, a janela apresentada na Figura 21 na página 43, relativa ao primeiro exemplo de aplicação, irá aparecer. Nesta é possível selecionar o atributo cujos valores se pretendem associar aos ecrãs do SVG. Adicionalmente, todos os valores tomados são listados com dropdowns para os associar cada um a uma camada de um SVG específica. Outra funcionalidade igualmente importante no Prototyper é a possibilidade de guardar o protótipo e as associações realizadas. Esta funcionalidade alivia o trabalho necessário quando o modelo do sistema tem uma elevada complexidade, pois permite reiniciar o trabalho sem ter de realizar as mesmas associações sempre que se abra o plugin. Para guardar ou importar as configurações realizadas basta aceder ao menu do “Prototyper” na barra de menus do IVY. O ficheiro que contém a configuração contém a extensão “.pcf”, que significa “Prototyper Configuration File”. Este equivale um ficheiro ZIP que alberga os 4.4. Conclusão 40 Figura 19: Exemplo do realce de um elemento selecionado na tabela de elementos disponíveis ficheiros SVG importados e um ficheiro de texto JSON, que explicita todas as configurações efetuadas. 4.4 conclusão Neste capítulo foi detalhado o plugin “Prototyper”, o fluxo de trabalho esperado, a sua arquitetura e o seu modo de funcionamento. Estas descrições permitiram compreender a forma como o plugin interage com o IVY, como o seu fluxo de trabalho encaixa no IVY e os diferentes modos para configurar o protótipo. Para complementar a descrição das funcionalidades do “Prototyper”, no capítulo seguinte serão apresentados três casos de estudo: o portão de uma garagem, uma bomba de infusão médica e um relógio digital. Estes exemplos irão permitir uma melhor compreensão das capacidades de prototipagem em oferta e do modo de animação. 5 EXEMPLOS DE APLICAÇÃO Neste capítulo apresentam-se três exemplos de aplicação, que irão utilizar as funcionalidades do “Prototyper” descritas até este ponto. Cada exemplo apresentado terá um maior nível de complexidade que o anterior. No final pretende-se que as funcionalidades de construção de protótipos sejam esclarecidas. 5.1 portão de garagem O primeiro exemplo que se irá expor descreve um portão de uma garagem controlado por um comando. O exemplo propriamente dito é relativamente simples, mas servirá para ilustrar, quer que a solução proposta não está limitada a interfaces no sentido tradicional, quer o tratamento de múltiplas camadas no SVG. Os detalhes do exemplo e o próprio modelo descrito em MAL já foram descritos na secção 2.1.2. Resumidamente, o estado do portão é modelado por um atributo “situacao” que pode estar em um de quatro estados: a abrir, a fechar, aberto e fechado. O botão do comando é modelado pela acção “Ac”, existindo ainda sensores que sinalizam quando o portão fica completamente aberto ou completamente fechado, modelados pelas acções “Ia” e “If”, respetivamente. O modelo pode ser consultado na Listagem 2.1, apresentado na página 8. Aqui, o foco passará pela descrição do mockup criado no Pencil, em suporte à criação do protótipo no IVY, do mapeamento entre este mockup e o modelo, efetuado no “Prototyper”, e do modo de animação. Na Figura 20 encontram-se ilustrados os mockups, criados no Pencil, correspondentes aos vários estados em que o modelo se pode encontrar, representados por A, B, C e D. O portão no estado A tem um tamanho superior para melhor visualizar os detalhes do protótipo, que contém os mesmos controlos no resto dos estados. A imagem maior, A, representa o portão fechado. Os botões pretos representam os sensores que são utilizados para indicar quando o portão fica completamente fechado ou completamente aberto. O botão vermelho representa o controlo remoto que o utilizador usa para abrir ou fechar o portão. Os restantes mockups possuem os mesmos botões. O mockup, B representa o portão a abrir, o portão C aberto e o portão D a fechar. 41 5.1. Portão de garagem 42 Figura 20: Protótipo do portão de garagem criado no Pencil com os seus estados representados por A, B, C, e D1 Após finalizar o protótipo no Pencil, este foi exportado para o formato SVG e importado para o plugin. Para obter o protótipo é necessário configurar as ligações entre o atributo e as ações do modelo e os elementos relevantes do protótipo. As ligações entre as ações e o SVG foram efetuadas da seguinte maneira: •Ac - a ação representativa do botão do comando fica associada ao botão vermelho no protótipo e este será acionado com o clique do rato; •If - a ação que representa o sensor a detetar que o portão está fechado fica associada ao botão preto esquerdo no protótipo que é acionado com o clique do rato; •Ia - a ação que representa o sensor a detetar que o portão está aberto fica associada ao botão preto direito no protótipo que é acionado com o clique do rato; O valores que o estado pode tomar serão ligados às camadas do protótipo: •a_abrir - camada B 1Imagens do portão retiradas de: https://www.canstockphoto.com.br/porta-garagem-esbo%C3%A7o-abertos25407780.html 5.1. Portão de garagem 43 Figura 21: Janela de configuração dos valores do atributo com os ecrãs do mockup •a_fechar - camada D •aberto - camada C •fechado - camada A Este é um exemplo de configuração simples, exigindo apenas o mapeamento das ações em elementos do SVG e dos valores do atributo às camadas do mesmo. Na Figura 21 apresenta-se a configuração efetuada. Note-se que os valores dos SVG elayers de cada valor do atributo correspondem aos nomes dados às camadas do SVG no Pencil na elaboração do mockup. Respetivamente, a layer “Gate Opening” corresponde ao estado B da Figura 20, “Gate Closing” ao estado D, “Gate Open” ao estado C e “Gate Closed” ao estado A. Na Figura 22 demonstra-se a interface da janela de animação com o protótipo do portão. À semelhança da interface principal do plugin, a secção à esquerda da interface apresenta o protótipo na camada SVG que foi configurada a aparecer no dado momento de execução. Como o estadoActual assume o valor de “aberto”, visualiza-se o protótipo na camada C. Os elementos do protótipos associados a ações podem ser interagidos diretamente no canvas. Como todos os elementos foram configurados para serem acionados com um clique do rato, clicar nos elementos no canvas irá resultar na execução de uma ação. Caso fossem configurados para acionarem com uma tecla especifica do teclado, o pressionar da mesma resultaria na execução da ação especificada. O painel lateral direito encontra-se dividido em duas secções. A secção superior demonstra as ações que se podem executar no estado atual. A secção inferior apresenta os atributos e o valor que tomam no momento de execução. Estes painéis auxiliam o utilizador com informação adicional e, no caso da secção que lista as ações, também se pode clicar duas vezes numa ação para progredir a animação. Sendo este um exemplo de complexidade reduzida, as animações consistem na transição entre ecrãs. 5.2. Bomba de infusão 44 Figura 22: Janela de animação do “Prototyper” A seguir apresenta-se um exemplo mais complexo que lida com a manipulação de conteúdo dentro do protótipo. 5.2 bomba de infusão Apresenta-se agora um exemplo de utilização do plugin para obtenção de um protótipo de uma bomba de infusão. Trata-se de um dispositivo responsável pela injeção intravenosa de fluídos em pacientes (por exemplo, medicamentos ou contrastes endovenosos para realização de exames). Considere-se que existe já um modelo da bomba de infusão em causa (ver Listagem 5.1). Por uma questão de facilidade de apresentação no contexto da dissertação, o modelo captura simplesmente a manipulação da quantidade de fluído a ser injetado. O modelo tem especificados atributos, ações e axiomas. Nas linhas 8e9estão declarados dois atributos: •on - do tipo boolean, pode ter o valor de verdadeiro ou falso. Este atributo é utilizado para indicar se a bomba de infusão se encontra ligada, ou não. •value - pode ter um valor numérico, no intervalo de 0a25. Este atributo guarda a quantidade de fluído a ser infundido pela bomba de infusão quando está ligada, sendo esta quantidade numa unidade de medida não especificada. Na linha 11 são apresentadas as ações do modelo: 5.3. Relógio multi-funções 51 Figura 26: Protótipo do relógio criado no Pencil com as suas duas camadas do relógio. O botão vermelho é meramente cosmético, pois no modelo não é definido que o dispositivo se possa desligar. Um detalhe relevante do protótipo é o facto dos campos das horas, minutos e segundos corresponderem a áreas de texto distintas, para se poder associar individualmente cada um destes aos atributos correspondentes. O atributo do modelo dispmode ficou associado aos ecrãs do protótipo. Destaca-se também a atribuição do tick, onde se definiu o trigger como o pressionar da tecla “U”. Com as ligações entre o protótipo e o modelo configuradas, pode-se executar a animação. Na Figura 27 demonstra-se um exemplo de execução. A animação inicia no modo de relógio, como especificado no modelo. Pressionando a tecla “U” cinco vezes, os minutos são incrementados por cinco. De seguida, alterna-se para o modo de cronómetro. Este inicia a zero. Como o cronómetro mede os segundos, para passar um minuto é necessário executar a ação tick sessenta vezes, resultando tal na imagem à direita. Ao alternar de volta para o relógio, o contador do cronómetro reinicia para zero e verifica-se que o relógio incrementou uma unidade no campo dos minutos, face à representação anterior. Um efeito curioso na representação dos valores é que a casa das décimas não é visível quando os números são de tamanho unitário. Tal deve-se ao facto de os valores representados no protótipo serem uma réplica dos valores do modelo na altura da execução, sem qualquer tipo de processamento para acrescentar o zero nas décimas no caso dos números unitários. Esta questão representa uma mera peculiaridade estética que não retira da informação que se pode retirar da animação do protótipo. Mas a possibilidade de ter widgets para representar números, em que fosse possível formar os números, podia ser incluída no trabalho futuro, Este caso de estudo é o mais complexo dos três apresentados e é o que melhor abrange todas as funcionalidades do plugin. Há associações de elementos interativos a ações com os 5.4. Análise 52 Figura 27: Exemplo de uma sequência de animação do relógio dois triggers disponíveis (clique do rato e pressionar de uma tecla) e associação de atributos a ecrãs do protótipo a elementos textuais do mesmo. 5.4 análise Com os exemplos de aplicação descritos foi possível demonstrar o uso do “Prototyper” em casos de uso reais, com graus de complexidade variáveis. A análise dos modos como as ligações entre os componentes do modelo descrito no IVY com os elementos interativos e textuais do mockup se efetuam ilustra as capacidades e limitações que existem na definição e representação do protótipo. Sendo possível a construção de protótipos com modelos de IVY complexos, o foco passa para o modo como o comportamento dos mesmos se pode definir. A transição entre ecrãs e alteração de componentes textuais no mockup satisfazem a necessidade de representação gráfica dos modelos, mas correspondem a maneiras básicas de a implementar. Tomando 5.4. Análise 53 como exemplo a bomba de infusão, foi necessário definir duas camadas para o mockup para representar os estados de desligado e ligado. A única diferença entre estes era a cor do ecrã e a ausência, ou não, do valor textual indicativo da quantidade de líquido a infundir. Considerando as capacidades do formato que descreve o mockup, o SVG, deve-se considerar acrescentar a futuras iterações do plugin mais maneiras de representar os atributos. 6 CONCLUSÃO No início deste projeto foi identificada uma lacuna na comunicação do comportamento dos modelos especificados no IVY Workbench a utilizadores fora do domínio da análise formal de interfaces. Para mitigar este problema, foi desenvolvido um novo plugin, que permite a representação gráfica dos modelos e do seu comportamento, através de protótipos. Neste documento foi descrito o plugin desenvolvido, bem como a sua concepção e desenvolvimento. O trabalho realizado deu ainda origem a um artigo aceite na conferência ICGI 2019 (International Conference on Graphics and Interaction) (Araújo et al.,2019). 6.1 resumo O documento iniciou-se com uma descrição do próprio IVY Workbench para contextualizar a necessidade de representação dos sistemas modelados face às funcionalidades em oferta. Deu-se especial atenção ao AniMAL, que permite ao utilizador decidir os passos a tomar durante a execução. Este conceito assemelha-se ao modo de execução esperado da funcionalidade planeada para o novo plugin de prototipagem. No entanto, este apresentará uma vista sobre o modelo mais próxima do que será a interface final. Para recolher requisitos para o novo plugin e perceber de que maneira é que a interação entre o modelo e a sua representação gráfica se iria manifestar, foram analisadas ferramentas de modelação de sistemas concorrentes ao IVY com uma componente gráfica. Esta análise permitiu distinguir dois métodos para representar os componentes dos modelos e a elaboração de um conjunto de requisitos funcionais. A nova funcionalidade deveria permitir a importação de um ou mais ficheiros descritivos do mockup do sistema, modelação e análise de sistemas interactivos, tal como o IVY, mas em que a componente de representação gráfica da interface assume um papel relevante. Foram analisadas duas ferramentas: o CogTool e o PVSio-web, para fins de levantamento de requisitos. A especificação dos requisitos instigou a necessidade de detalhar os programas que poderão ser usados para desenhar o mockup, o tipo de formato que o iria descrever e que 54 6.2. Análise 55 bibliotecas se utizariam para a importação e manipulação do ficheiro. Conclui-se que a ferramenta Pencil Project oferecia maior flexibilidade na conceção dos mockups e o formato SVG exportado foi considerado como o mais adequado para descrevê-los por apresentar um formato normalizado que pode ser gerado ou lido por outros programas, graças à sua especificação aberta e disponível a todos. Com os requisitos e a estrutura do mockup definidos, prosseguiu-se para uma descrição do próprio plugin, entitulado “Prototyper”, da sua arquitetura e das funcionalidades implementadas na versão final. O código foi estruturado de modo a haver uma separação clara entre a lógica da interface e a lógica de fundo, sendo esta última responsável pelo processamento dos SVGs importados e dados relacionados. Por último, foram apresentados 3casos de estudo: um portão de uma garagem, uma bomba de infusão médica e um relógio digital multi-funções. Os exemplos permitiram melhor demonstrar as funcionalidades em oferta do “Prototyper” e como a animação dos protótipos configurados se podia manifestar. 6.2 análise Após uma análise de todo o trabalho efetuado e descrito neste documento, considera-se que o produto final cumpre os objetivos inicialmente definidos. A representação gráfica do comportamento dos modelos possibilita a comunicação da especificação destes a pessoas não peritas em técnicas de modelação e análise formais. Os protótipos criados permitem a análise do comportamento do sistema por mais pessoas e, consequentemente, a obtenção de mais feedback. Este feedback permite iterar sobre os designs existentes e atingir o design final do sistema mais rapidamente. Detalham-se, agora, os requisitos inicialmente definidos, com uma explicação sobre como foram implementados: •Requisito 1O plugin deverá suportar a importação de um ou mais ficheiros que descrevam o protótipo da interface desejada. O “Prototyper” suporta a importação de múltiplos ficheiros SVG, como descrito na secção 4.3. Adicionalmente, o SVG permite a definição de camadas num só ficheiro, incorporando a capacidade de representar os múltiplos estados do sistema num só ficheiro. •Requisito 2O ficheiro a importar deve estar num formato aberto de livre utilização. O “Prototyper” suporta a importação de ficheiros SVG. O SVG é um formato de imagens vetorial baseado em XML. Descreve gráficos a duas dimensões, incluindo formas geométricas, texto e gradientes. É um formato aberto desenvolvido pela W3C, pelo que cumpre o requisito descrito. 6.2. Análise 56 Um detalhe que deve ser esclarecido é que, apesar do plugin suportar a importação de ficheiros SVG, depende da estrutura gerada pelo Pencil. Significa isto que algumas funcionalidades essenciais, como a identificação das áreas interativas, não estão garantidas com SVG gerados por outros programas. Esta limitação é algo contrária às intenções do requisito descrito, mas planeia-se em futuras revisões do plugin melhorar o suporte de ficheiros SVG genéricos. •Requisito 3Deverá ser possível a identificação/especificação de áreas de interatividade dentro do mockup importado; O “Prototyper”, no momento da importação do SVG, identifica as áreas interativas que o utilizador pode configurar. O plugin identifica certas formas no ficheiro que podem ser associadas a elementos de interface, como botões ou checkboxes. Neste momento não há suporte para a definição destas áreas manualmente por parte do utilizador, sendo esta uma funcionalidade a adicionar em trabalho futuro. •Requisito 4Deverá ser possível mapear essas mesmas áreas para atributos e ações do modelo; O “Prototyper” suporta dois tipos de áreas, interativas e textuais, que podem ser associadas a ações e atributos do modelo, respetivamente. Esta funcionalidade é descrita na secção 4.3e nos exemplos de aplicação apresentados no capítulo 5. •Requisito 5O plugin deverá suportar vários tipos de interações com os elementos interativos do protótipo; É possível definir dois tipos de trigger para as áreas interativas: clique do rato ou pressionar de uma tecla. •Requisito 6Deverá ser possível animar o protótipo para visualizar o comportamento do sistema modelado; Após efetuar o mapeamento entre o protótipo e o modelo descrito no IVY, é possível iniciar a animação. •Requisito 7Deverá ser possível guardar o estado do animador e posteriormente restaurá-lo e resumir o trabalho. O “Prototyper” oferece a opção de guardar e restaurar o trabalho efetuado. Utiliza um ficheiro com a extensão “.pcf” que alberga informação sobre os SVG importados e o mapeamento efetuado. 6.3. Trabalho Futuro 57 Um aspeto que pode ser questionado é o limitado leque de opções, no que toca à configuração do protótipo. Neste momento, apenas se podem definir dois tipos de trigger para as ações associadas: clicar com o rato, ou premir uma tecla; e dois modos de mapear os atributos do modelo para o protótipo: associá-los a camadas dos ficheiros SVG, para definir que camada deve ser apresentada em cada momento, ou a elementos textuais de uma dada camada, para que o seus valores sejam representados nestes. No entanto, ficaram lançadas as bases para a evolução da abordagem para possibilidades de configuração mais avançadas. Das duas ferramentas inicialmente analisadas, o PVSio-web é aquela cujas características mais se aproximam das do IVY. Poder-se-ia efetuar a comparação do “Prototyper” com o PVSio-Web e a sua forma de definir e interagir com os protótipos, através das áreas definidas numa imagem raster do sistema. No entanto, argumenta-se que mais que replicar ou competir com as funcionalidade de outra ferramenta, o trabalho focou-se em adicionar uma funcionalidade inexistente ao IVY. O “Prototyper”, como está implementado, encontrase aberto à adição de funcionalidades que permitirão novos métodos de definir a animação do protótipo. A escolha do formato SVG possibilita a futura integração de funcionalidades mais avançadas que este suporta, como a especificação de animações e scripting. 6.3 trabalho futuro Como já foi mencionada na secção anterior, o trabalho futuro irá focar-se em adicionar às funcionalidades base do “Prototyper” descritas neste documento. Estas poderão incluir: a adição de novas formas de visualização dos valores dos atributos (alteração da cor dos elementos, parâmetros de visibilidade, ...), suporte para widgets que permitirão a identificação dos tipos de elementos no SVG do mockup e a automatização do mapeamento destes com atributos e ações do modelo, e suporte para animações descritas no próprio SVG. Adicionalmente, pretende-se suportar o SVG de uma forma mais genérica para remover a dependência da estrutura com que o Pencil Project exporta, e melhor cumprir os requisitos definidos. Estas futuras adições ao plugin deverão permitir uma especificação mais rica do protótipo, facilidade de uso da funcionalidade e uma capacidade de comunicação do comportamento dos sistemas melhorada para facilitar a comunicação a um maior número de pessoas do design do mesmo. BIBLIOGRAFIA J. Araújo, R. Couto, and J.C. Campos. Gerador de protótipos de interfaces gráficas para o IVY workbench. In ICGI 2019 – International Conference on Graphics and Interaction. IEEE, 2019. aceite para publicação. blackears. Svg salamander, 2019. URL https://github.com/blackears/svgSalamander. J. C. Campos and M. D. Harrison. Interaction engineering using the ivy tool. In ACM Symposium on Engineering Interactive Computing Systems (EICS 2009), pages 35–44, New York, NY, USA, 2009. ACM. doi: 10.1145/1570433.1570442. J.C. Campos. High assurance interactive computing systems. In J. Ziegler, J. C. Campos, and L. Nigay, editors, HCI Engineering: Charting the Way towards Methods and Tools for Advanced Interactive Systems, pages 39–42,2014. José C. Campos and Michael D. Harrison. Model checking interactor specifications. Automated Software Engineering,8(3):275–310, Aug 2001. ISSN 1573-7535. doi: 10.1023/A: 1011265604021. URL https://doi.org/10.1023/A:1011265604021. Stuart K. Card, Thomas P. Moran, and Allen Newell. The keystroke-level model for user performance time with interactive systems. Commun. ACM,23(7):396–410, July 1980. ISSN 0001-0782. doi: 10.1145/358886.358895. URL http://doi.acm.org/10.1145/358886. 358895. Alessandro Cimatti, Edmund Clarke, Enrico Giunchiglia, Fausto Giunchiglia, Marco Pistore, Marco Roveri, Roberto Sebastiani, and Armando Tacchella. Nusmv 2: An opensource tool for symbolic model checking. In Ed Brinksma and Kim Guldstrand Larsen, editors, Computer Aided Verification, pages 359–364, Berlin, Heidelberg, 2002. Springer Berlin Heidelberg. ISBN 978-3-540-45657-5. E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic verification of finite state concurrent systems using temporal logic specifications: A practical approach. In Conference Record of the Annual ACM Symposium on Principles of Programming Languages, pages 117–126. ACM, 12 1983. ISBN 0897910907. Richard M. Cohn, David Dodds, Andrew Donoho, David A. Duce, J. Paul O. Evans, Jon Ferraiolo, S. Furman, Peter Graffagnino, Rick Graham, Lofton Henderson, Alan Hester, Bob Hopgood, Christophe Jolif, K. Faith Lawrence, Chris Lilley, Philip Andrew Mansfield, 58 Bibliografia 59 Kevin McCluskey, Tuan Minh Nguyen, Troy Sandal, Peter Santangeli, Haroon I. Sheikh, Robert Stevahn, and Shenxue Zhou. Scalable vector graphics svg 1.0specification. 2000. R. Couto and J.C. Campos. IVY 2a model-based analysis tool. In The 11th ACM SIGCHI Symposium on Engineering Interactive Computing Systems - EICS 2019, pages 5:1–5:6. ACM, 2019. doi: 10.1145/3319499.3328228. Jarek Foksa Daniel Holbert Paul LeBeau Robert Longson Henri Manson Ms2ger Kari Pihkala Philip Rogers David Zbarsky David Dailey, Eric Eastwood. Scalable vector graphics (svg) 2,2018. URL https://www.w3.org/TR/2018/CR-SVG2-20181004/. Evolus. Collection properties, 2012. URL https://pencil.evolus.vn/wiki/devguide/ Tutorial/Collection_properties.html. The Apache Software Foundation. Apache batik svg toolkit, 2016. URL https:// xmlgraphics.apache.org/batik/. Google. Material icons guide, 2019. URL https://google.github.io/ material-design-icons/. Bonnie E. John. CogTool User Guide. IBM T. J. Watson Research Center, 19 Skyline Drive, Hawthorne NY 10532,2edition, 5 2012. Kmseteam. File:suuntoambit2.jpg, 2013. URL https://commons. wikimedia.org/wiki/File:SuuntoAmbit2.JPG. Licença: CC BY-SA 3.0 (https://creativecommons.org/licenses/by-sa/3.0). Glenn E. Krasner and Stephen T. Pope. A cookbook for using the model-view controller user interface paradigm in smalltalk-80.J. Object Oriented Program.,1(3):26–49, August 1988. ISSN 0896-8438. URL http://dl.acm.org/citation.cfm?id=50757.50759. Object Refinery Limited. About jfreesvg, 2019. URL http://www.jfree.org/jfreesvg/. Eve Maler, Jean Paoli, C. M. Sperberg-McQueen, François Yergeau, and Tim Bray. Extensible markup language (XML) 1.0(third edition). first edition of a recommendation, W3C, February 2004. http://www.w3.org/TR/2004/REC-xml-20040204. César A. Muñoz. Rapid prototyping in PVS. Technical Report NASA/CR-2003-212418 / NIA Report No. 2003-03,2003. Patrick Oladimeji, Paolo Masci, Paul Curzon, and Harold Thimbleby. PVSio-web: a tool for rapid prototyping device user interfaces in PVS. Electronic Communications of the EASST,69,2014. doi: 10.14279/tuj.eceasst.69.963. URL http://dx.doi.org/10.14279/ tuj.eceasst.69.963. Bibliografia 60 S. Owre, N. Shankar, J. M. Rushby, and D. W. J. Stringer-Calver. PVS System Guide. SRI International, 333 Ravenswood Avenue, Menlo Park, CA, 94025,2edition, 11 2001. M. Ryan, J. Fiadeiro, and T. Maibaum. Sharing actions and attributes in modal action logic. In Theoretical Aspects of Computer Software, volume 526 of LNCS, pages 569–593. Springer, 1991. doi: 10.1007/3-540-54415-1_65.