BSmart: desenvolvimento rigoroso de aplicações Java Card com base no método formal B

AUTOR(ES)

Bruno Emerson Gurgel Gomes

DATA DE PUBLICAÇÃO

2007

RESUMO

A tecnologia Java Card permite o desenvolvimento e execução de pequenas aplicações embutidas em smart cards. Uma aplicação Java Card é composta por um cliente, externo ao cartão, e por uma aplicação contida no cartão que implementa os serviços disponíveis ao cliente por meio de uma Application Programming Interface (API). Usualmente, essas aplicações manipulam e armazenam informações importantes, tais como valores monetários ou dados confidenciais do seu portador. Sendo assim, faz-se necessário adotar um maior rigor no processo de desenvolvimento de uma aplicação smart card, visando melhorar a sua qualidade e confiabilidade. O emprego de métodos formais como parte desse processo é um meio de se alcançar esses requisitos de qualidade. O método formal B e um dentre os diversos métodos formais para a especificação de sistemas. O desenvolvimento em B tem início com a especificação funcional do sistema, continua com a aplicação opcional de refinamentos à especificação e, a partir do último nível de refinamento, é possível a geração de código para alguma linguagem de programação. O formalismo B conta com bom suporte de ferramentas e a sua aplicação a Java Card mostra-se bastante adequada, uma vez que a especificação e desenvolvimento de APIs e o ponto forte de B. O método BSmart aqui proposto visa promover o desenvolvimento rigoroso de aplicações Java Card a partir da geração de código da aplicação com base em refinamentos da sua especificação formal descrita na notação B. O processo de desenvolvimento descrito no método é apoiado pela ferramenta BSmart, a qual constitui-se por alguns programas que automatizam cada etapa do método; e por uma biblioteca de módulos B e classes Java Card que modelam tipos primitivos, classes essenciais da API Java Card e estruturas de dados reutilizáveis

ASSUNTO(S)

método b b method geração de código. java card métodos formais code generation formal methods, sistemas de computacao java card

Documentos Relacionados

• Desenvolvimento rigoroso com uml-rt
• Uma implantação de criptografia de curvas elipticas no Java Card
• Desenvolvimento de sistemas TINA utilizando a linguagem de especificação formal SDL com geração automatica de codigo Java
• Uso de AMF para interação entre Java e Action Script no desenvolvimento de aplicações RIA.
• Orientação exterior de um par estereoscópico Ikonos II com base no modelo não-rigoroso DLT