60ª Reunião Anual da SBPC

INTRODUÇÃO:

Os sistemas embarcados estão cada vez mais presentes no dia a dia das pessoas. De acordo com uma projeção da empresa Nokia, em meados de 2010, quatro bilhões de pessoas possuirão um telefone celular. Sistemas embarcados são caracterizados, essencialmente, por oferecerem serviços de computação como atividade meio. Citam-se como exemplos telefones celulares, fornos de microondas, tocadores de DVD e de arquivos MP3. Sistemas embarcados são também caracterizados por sua forte limitação de recursos, tais como tamanho máximo de memória de programa ocupada e consumo de energia, juntamente com um curto tempo para a finalização da produção e o lançamento do produto mercado. Para lidar com a complexidade dessas aplicações e atender a todos os requisitos dos produtos, garantindo a qualidade esperada dentro de um curto período de tempo, faz-se necessário aumentar o nível de abstração do projeto e verificar formalmente as propriedades do mesmo. Nesse sentido, este trabalho propõe a geração automática de código para aplicações embarcadas a partir de modelos Alloy e apresenta os algoritmos e as regras de transformação dos modelos para a linguagem Java. Essa abordagem alia automação no desenvolvimento de software à confiabilidade da verificação formal. Escolheu-se o Alloy como linguagem formal devido à sua sintaxe muito parecida com linguagens orientadas a objetos, reduzindo assim o tempo necessário para o seu aprendizado.

METODOLOGIA:

O compilador de modelos Alloy para código Java foi codificada também em Java, com o auxílio das ferramentas CUP e JFlex para a geração automática do parser e do scanner. Atualmente, a ferramenta é composta por em torno de cinco mil linhas de código. As classes e os atributos são extraídos a partir das signatures e suas relações. Signatures que possuem campos são traduzidas para classes que encapsulam os campos como atributos; já as vazias são traduzidas para o tipo String em Java. Como em Alloy não há estruturas de dados, faz-se necessário a criação delas em Java. A metodologia disponibiliza as estruturas Vector, ArrayList, LinkedList, HashSet, TreeSet, HashMap, Hashtable, LinkedHashMap e AbstractCollection. Os métodos são extraídos a partir dos predicados e das funções em Alloy. Métodos extraídos a partir de predicados são tipados como void; já os extraídos de funções são tipados de acordo com o tipo de retorno declarado no modelo Alloy. A inferência da classe que encapsula um dado método é realizada através da lista de parâmetros formais do mesmo. Fez-se necessário codificar as operações do Alloy em Java, com o intuito de garantir que o código gerado descreva o comportamento descrito no modelo Alloy. Todas as estruturas de dados geradas ou estendem a classe abstrata AbstractCollection ou implementam a interface Map. A máquina de estados da aplicação é sintetizada automaticamente a partir da especificação Alloy, tendo como modelo de computação escolhido o reativo.

RESULTADOS:

Modelaram-se três aplicações em Alloy e se aplicou o tradutor de código com as regras de tradução descritas na metodologia. A agenda de endereços e a máquina de vendas são aplicações mistas, possuindo elementos data-flow, a qual faz uso intenso de estruturas de dados; já o controle de um elevador é totalmente control-flow. Observa-se que as aplicações as quais fazem algum uso de estruturas de dados são bastante beneficiadas pela geração automática de código, tendo em consideração o número de linhas de código gerado. Isso se deve ao fato dessas estruturas, inexistentes no modelo Alloy, serem imprescindíveis para tornar o código gerado executável. Esse fato se evidencia ao considerar que o modelo Alloy da agenda de endereços faz menor uso de construções Alloy que o da máquina de vendas, mas mesmo assim o código Java gerado é maior – a agenda de endereços sequer faz uso de herança e polimorfismo. A quantidade de métodos Java gerada é superior à quantidade de predicados Alloy existente para uma mesma aplicação, devido ao fato que aplicações data-flow possuírem mais atributos encapsulando os dados (necessitando de métodos get e set), além de um comportamento mais elaborado sobre esses dados. Na aplicação totalmente control-flow o único comportamento existente é o da máquina de estados, possuindo somente o método main. Ressalta-se também que o código Java gerado para as três aplicações não apresentou erros, o que demonstra a consistência das regras de tradução e dos algoritmos desenvolvidos.

CONCLUSÕES:

Este trabalho apresentou uma metodologia e uma ferramenta para geração automática de código Java a partir de modelos Alloy, tendo como domínio aplicações embarcadas. Esta abordagem possui a vantagem de ser baseada em um método formal simples, relacional, com sintaxe baseada em orientação a objetos. Além disso, contribui potencialmente para a redução do tempo para o lançamento do produto no qual a aplicação modelada e gerada automaticamente faz parte, pois não há a necessidade de codificá-la e testá-la, obtendo maior qualidade em um tempo mais reduzido. Também se analisou quantitativamente o código gerado para aplicações control-flow e mistas, demonstrando o bom resultado e o potencial da abordagem aqui proposta. Como trabalhos futuros, citam-se a tradução dos fatos dos modelos Alloy e a modelagem de uma aplicação maior, comparando-a qualitativamente com a respectiva modelagem em UML e a escrita manual do código Java através de métricas de software para o domínio de embarcados. Sem a tradução dos fatos, as restrições do modelo Alloy devem ser modeladas juntamente com o comportamento, tornando menos flexível a modelagem das propriedades da aplicação.

Instituição de fomento: PIBIC/CNPq/UFRGS

Trabalho de Iniciação Científica

Palavras-chave: Verificação Formal, Sistemas Embarcados, Geração Automática de Código

E-mail para contato: rrferreira@inf.ufrgs.br