Made available in DSpace on 2016-04-27T18:47:17Z (GMT). No. of bitstreams: 1 Francimar Felipa da Silva Costa.pdf: 1224855 bytes, checksum: 4a0ebf0e6de35ed4986b77f20331f4de (MD5) Previous issue date: 2015-05-26 / Coordenação de Aperfeiçoamento de Pessoal de Nível Superior / The caretaking responsibility of elderly people in need of palliative treatment at home has been increasingly assigned to their families, in which considering this scenario can experience moments of fragility; physical, social and financial problems with serious consequences to the caregiver health. The adopted methodology for this research is an exploratory-descriptive study, utilising an interdisciplinary qualitative perspective, which is based in the literacy and interpretation of an empiric dissertation of 10 voluntary caretakers, using semi-structured interview processes. The objective is to contribute with theories, based in Social Gerontology, in order to provide a better comprehension about the caretaker of the elderly in palliative care, the practical implications and effects that can affect the caretaker. The socio-demographic profile of the palliative caretakers was identified, as were the groupings, based specifically in the answers provided, such as; how to proceed in palliative care , performance limits and possibilities of performance improvement . These answers indicate us there can be no connection between everyday life events and public and social policies, being both necessarily in complementation of each other. The recommendation is to give the proper importance to the situation, implementing the use of specific public policies to help the caretaker, as it was specifically noted in some of the reports, allowing the improvement of their well being, the prevention of conflicts, stress, depression and furthermore the security necessary in some palliative care procedures. Moreover, it is also indispensable the total support of the family and the articulation in a social network, either formal or informal, contributing to a less arduous day-to-day life of the caretaker, as well as a more comfortable end of life for the elderly, alleviating pain and suffering / O ato de cuidar de idosos em cuidados paliativos, em domicílio, atualmente, é responsabilidade cada vez mais atribuída às famílias que, nesse cenário, podem vivenciar contextos de fragilidades, subjetiva, física, social e financeira, com implicações sérias, senão amargas, para a saúde do seu cuidador. A metodologia adotada nesta pesquisa é a de estudo exploratório-descritivo, em perspectiva qualitativa e abordagem interdisciplinar que, pautada na literatura e na interpretação de um empírico trazido pelos discursos de 10 cuidadores voluntários em entrevistas semiestruturadas, objetiva contribuir, sob o enfoque da Gerontologia Social, com subsídios teóricos para uma melhor compreensão sobre como procede o cuidador familiar de idoso em cuidado paliativo, e quais as implicações das práticas e efeitos que o impactam. Foi identificado o perfil sociodemográfico do cuidador familiar em situação paliativa, assim como categorias temáticas advindas de suas respostas especialmente a como procede nos cuidados paliativos , seus limites de atuação e possibilidades de melhoria em sua performance . Essas respostas nos fazem ver que não pode haver cisão entre acontecimentos da vida cotidiana e políticas público-sociais, sendo ambos necessariamente complementares; insiste-se, pois, sobre a importância de serem postas em ação as políticas públicas de cuidados específicos ao cuidador familiar em situação paliativa, a partir de suas demandas em vários registros, a fim de permitir-lhe a melhoria de seu bem-estar, a prevenção de conflitos, do estresse e depressão, além da segurança necessária para os procedimentos de cuidados paliativos. Ratifica-se ainda o imprescindível apoio da família e da articulação a uma rede social, formal ou informal, contribuindo para tornar menos árduo o dia a dia do cuidador, assim como mais confortável o do idoso em final de vida, escapando da dor e do sofrimento

A evolução de sistemas de gerenciamento de tráfego aéreo é pesquisada para suportar o crescimento na demanda por transporte aéreo. Uma alternativa para essa evolução é o aumento no grau de automação. Os sistemas automatizados precisam ser tão seguros quanto os sistemas em operação atualmente. Com o uso de técnicas de especificação e verificação formal é possível avaliar os requisitos de sistemas. Neste trabalho, é proposto um ciclo de especificação formal, que consiste em um conjunto de diretrizes para aplicação de técnicas de métodos formais em requisitos escritos em linguagem natural. O resultado esperado da aplicação deste ciclo é um conjunto de requisitos escritos em linguagem natural verificados formalmente. O ciclo é composto pelas etapas: levantamento de requisitos do sistema e classificação em padrões de especificação; mapeamento dos requisitos para as linguagens de especificação formal LTL (Linear Temporal Logic) e CTL (Computation Tree Logic); verificação formal da especificação com o verificador NuSMV; ajustes na especificação baseada nos resultados da verificação; ajustes nos requisitos baseados nos ajustes na especificação. As diretrizes propostas são definidas com a análise da verificação formal do Automated Airspace Concept (AAC), padrões de especificação e diretrizes para uso do verificador NuSMV. Os resultados esperados são obtidos na aplicação do ciclo de especificação em dois estudos de caso. A principal contribuição do trabalho é o conjunto de diretrizes para elaboração de expressões escritas em linguagem de especificação formal baseadas em requisitos escritos em linguagem natural e que podem ser verificadas formalmente. / Air traffic management systems evolution is being researched to support air transportation demand growth. An evolution alternative is system automation degree increase. Automated systems need to be as safe as current operating systems. It is possible to analyze system requirements with the application of formal specification and formal verification techniques. In this work, a specification cycle is proposed. The specification cycle is a set of guidelines to use formal method techniques on requirements written in natural language. The specification cycle application expected result is a set of formally verified requirements written in natural language. This cycle is comprised of the following stages: system requirements elicitation and specification pattern classification; requirements mapping to LTL (Linear Temporal Logic) and CTL (Computation Tree Logic) formal specification languages; specification formal verification using the NuSMV verifier; formal specification adjustment based on verification results; requirements adjustment based on formal specification adjustment. The proposed guidelines are defined with the Automated Airspace Concept (AAC) formal verification analysis, specification patterns and guidelines for the NuSMV formal verifier use. The expected results are accomplished in the specification cycle application on two study cases. The main contribution of this work is the set of guidelines applied to formulate formally verifiable expressions specified in formal specification languages based on system requirements written in natural language.

As melhores práticas de engenharia de software indicam que a atividade de verificação é fundamental para se alcançar o mínimo de qualidade na construção de um software. Nos processos de desenvolvimento baseados na UML, um dos seus focos principais é detectar inconsistências nos diagramas representativos do software. No entanto, a maioria desses processos, como o Iconix, aplica apenas técnicas informais (ex: inspeções visuais nos modelos), fazendo com que muitas vezes essa atividade seja negligenciada pelos desenvolvedores. Por outro lado, com o avanço das ferramentas automatizadas de verificação, os métodos formais, tais como o Event-B, estão atraindo cada vez mais a atenção das empresas de software. Porém, ainda é difícil convencer os desenvolvedores a adotá-los, pois não estão acostumados com os conceitos matemáticos envolvidos. Assim, este trabalho apresenta uma proposta de inclusão do Event-B no Iconix, dando origem ao BIconix, um processo de desenvolvimento orientado a objetos com suporte à verificação formal de inconsistências. Mais especificamente, esta tese aborda a tradução automática dos quatro diagramas existentes no Iconix (classes, casos de uso, robustez e sequência) para o Event-B, além de mostrar como esta formalização pode auxiliar na atividade de verificação em pontos específicos e bem definidos no processo proposto. / The best practices of software engineering indicate that the verification activity is essential to achieve some quality during the software construction. In UML-based development processes, one of its main focuses is the detection of inconsistencies in diagrams that represent the software. However, most of these processes, such as Iconix, apply only informal techniques (eg. visual model inspections), often implying the negligence of that activity by developers. Moreover, with the advance of automated verification tools, formal methods, such as Event-B, are increasingly attracting the attention of software companies. However, it is still difficult to convince developers to adopt them, because they are not acquainted with some mathematical concepts. Thus, this paper presents a proposal for the inclusion of Event-B within Iconix, giving rise to BIconix, an object-oriented development process that supports automatic inconsistencies formal verification. More specifically, this thesis addresses the translation of the four existing diagrams in Iconix (classes, use cases, robustness and sequence) to Event- B, and show how this formalization can assist the verification activity in well-defined check points of the proposed process.

Submitted by Maria Aparecida (cidazen@gmail.com) on 2017-08-21T12:14:23Z No. of bitstreams: 1 Falkner de Arêa Leão Moraes.pdf: 2601896 bytes, checksum: 0fa8b49e3f279d911a70b4f78d9cbe08 (MD5) / Made available in DSpace on 2017-08-21T12:14:23Z (GMT). No. of bitstreams: 1 Falkner de Arêa Leão Moraes.pdf: 2601896 bytes, checksum: 0fa8b49e3f279d911a70b4f78d9cbe08 (MD5) Previous issue date: 2009-02-16 / Lack of security is a constant concern in open distributed systems. Threats are present within environments insecure, uncertain and constantly changing. Due to this problem, many tools for evaluating vulnerabilities of the network as well as for their protection are being developed as techniques for encryption and software systems such as antivirus, firewall and IDS (Intrusion Detection System). Among these, there are IDS systems that are being conceived, designed and implemented, using techniques executed by agents. However, it is necessary to assure security and reliability of exchanged messages inside IDS. For this purpose, this paper proposes a security solution for IDS based on agents. The proposed solution provides a methodology and a secure mechanism for communication among agents, through information protection configuration mechanisms, authentication and authorization, key control and messages persistence using XML. The proposed solution is implemented as an extension to the IDS-NIDIA (Network Intrusion Detection System based on Intelligent Agents), whose architecture has an intelligent agent society that communicate in a cooperative way in a distributed environment. The implementation of the prototype and tests proposed in this work show the applicability of the proposed solution. / A falta de segurança é uma preocupação constante em sistemas distribuídos abertos. Ameaças estão presentes dentro de ambientes inseguros, incertos e que mudam constantemente. Devido a esses problemas, diversas ferramentas para avaliação de vulnerabilidades da rede, bem como para sua proteção, estão sendo desenvolvidas como técnicas de criptografia e softwares como antivírus, firewall e IDS (Intrusion Detection System). Dentre estas, destaca-se Sistemas IDS que estão crescentemente sendo concebidos, projetados e implementados, usando técnicas de segurança executadas por agentes. Entretanto, é necessário que a segurança e a confiabilidade das mensagens trocadas dentro de um sistema IDS sejam asseguradas. Para este fim, este trabalho propõe uma solução segura e confiável para IDS baseada em agentes. A solução propõe estabelecer um esquema de execução e comunicação segura dos agentes através de mecanismos de proteção de informações de configuração, autenticação e autorização, controle de chaves e persistência de mensagens do IDS, utilizando XML. A solução proposta é implementada como uma extensão do IDS-NIDIA (Network Intrusion Detection System based on Intelligent Agents), cuja arquitetura consiste em uma sociedade de agentes inteligentes que se comunicam de forma cooperativa em um ambiente distribuído. A implementação do protótipo e os testes apresentados neste trabalho demonstram a aplicabilidade da solução proposta.

Este trabalho descreve o formalismo das gramáticas livres de contexto adaptativas com verificação de aparência. Esses dispositivos gramaticais possuem como núcleo uma gramática livre de contexto subjacente e, como mecanismo de auto-modificação, uma ou várias funções adaptativas que determinam quais produções são aplicáveis em cada passo de uma derivação. A verificação de aparência se refere a uma forma especial de aplicar algumas produções, escolhidas pelo projetista da gramática, sem alterar a forma sentencial nessa aplicação. É provado que esse formalismo tem poder de máquina de Turing demonstrando, em forma construtiva, sua equivalência com quatro formalismos gramaticais baseados em gramáticas livres de contexto com mecanismos de controle, que tem esse poder. São desenvolvidos dois analisadorers para linguagens dependentes de contexto a partir de um desses outros quatro formalismos. Um deles, que é baseado em autômatos-pilha, opera em forma ascendente; o outro, baseado em autômatos finitos adaptativos, opera em forma descendente. / This work introduces and describes the formalism of the context-free adaptive grammar with appearance checking. Such gramatical devices have as its kernel a subjacent context-free grammar and, as mechanism of self-modification, one or several adaptive functions which determines the productions able to be applied at each step of a derivation. The appearance checking refers to a special way to apply some productions, choosen by the designer of the grammar, without changing the sentential form in this application. It is proved that this formalism has Turing Machine power, proving, by construction, its equivalence with four grammatical formalisms based on context-free grammars and with control mechanisms, with such power. Two parsers have been developed for context-dependent languages from one of these four formalisms. One of them is based on stack-automata, and operates in a bottom-up fashion.

O avanço tecnológico recente tem atraído tanto a comunidade acadêmica quanto o mercado para a investigação de novos métodos, técnicas e linguagens formais para a área de Projeto de Engenharia. A principal motivação é o atendimento à demanda para desenvolver produtos e sistemas cada vez mais completos e que satisfaçam as necessidades do usuário final. Necessidades estas que podem estar ligadas, por exemplo, à análise e reconhecimento de objetos que compõe uma imagem pela sua textura, um processo essencial na automação de uma enorme gama de aplicações como: visão robótica, monitoração industrial, sensoriamento remoto, segurança e diagnóstico médico assistido. Em vista da relevância das inúmeras aplicações envolvidas e pelo fato do domínio de aplicação ser muito próximo do contexto do desenvolvedor, é apresentada uma proposta de um processo de design baseado no Projeto Axiomático como sendo o mais indicado para esta situação. Especificamente, se espera que no estudo de caso da análise de textura haja uma convergência mais rápida para a solução - se esta existir. No estudo de caso, se desenvolve uma nova concepção de arquitetura de rede neural artificial (RNA), auto-organizável, com a estrutura espacial bidimensional da imagem de entrada preservada, tendo a extração e reconhecimento/classificação de textura em uma única fase de aprendizado. Um novo conceito para o paradigma da competição entre os neurônios também é estabelecida. O processo é original por permitir que o desenvolvedor assuma concomitantemente o papel do cliente no projeto, e especificamente por estabelecer o processo de sistematização e estruturação do raciocínio lógico do projetista para a solução do problema a ser desenvolvido e implementado em RNA. / The recent technological advance has attracted the industry and the academic community to research and propose methods, seek for new techniques, and formal languages for engineering design in order to respond to the growing demand for sophisticated product and systems that fully satisfy customers needs. It can be associated, for instance, with an application of object recognition using texture features, essential to a variety of applications domains, such as robotic vision, industrial inspection, remote sensing, security and medical image diagnosis. Considering the importance of the large number of applications mentioned before, and due to their characteristic where both application and developer domain are very close to each other, this work aims to present a design process based on ideas extracted from axiomatic design to accelerate the development for the classical approach to texture analysis. Thus, a case study is accomplished where a new conception of neural network architecture is specially designed for the following proposal: preserving the two-dimensional spatial structure of the input image, and performing texture feature extraction and classification within the same architecture. As a result, a new mechanism for neuronal competition is also developed as specific knowledge for the domain. In fact, the process proposed has some originality because it does take into account that the developer assumes also the customers role on the project, and establishes the systematization process and structure of logical reasoning of the developer in order to develop and implement the solution in neural network domain.

Orientador: Renato Eugenio da Silva Diniz / Resumo: A educação em ciências é uma prática social que vem sendo cada vez mais ampliada e desenvolvida nos chamados espaços não formais de educação. Por apresentar estratégias de ensino atrativas e interativas, a utilização desses espaços pode contribuir para uma alfabetização científica mais efetiva tanto para os alunos como também para os professores. Partindo dessa perspectiva o objetivo geral desta pesquisa foi analisar as possibilidades e limites de uma proposta de formação continuada de professores dos anos iniciais do Ensino Fundamental, que busca uma ressignificação da relação entre o ensino de Ciências em espaços não formais e a prática docente escolar. Para atender tal objetivo a pesquisa foi desenvolvida, no período de janeiro de 2016 a março de 2018, no Centro de Ciências e Planetário do Pará – CCPP, localizado na cidade de Belém no estado do Pará. Os sujeitos foram professores de Ciências que atuavam em turmas dos anos iniciais do Ensino Fundamental e os dados qualitativos foram coletados por meio da observação participante, de questionários e entrevistas. A análise dos dados coletados utilizou-se o conjunto de técnicas da Análise de Conteúdo. Através dos resultados obtidos a partir do levantamento do perfil dos professores foram realizadas ações de formação onde a proposta levou em consideração a análise crítica da realidade docente. A formação foi desenvolvida no período de julho a novembro de 2017 e o último encontro ocorreu em maio de 2018. O processo formativo ocor... (Resumo completo, clicar acesso eletrônico abaixo) / Abstract: Education in science is a social practice that has been increasingly expanded and developed in the so-called non-formal spaces of education. By presenting attractive and interactive teaching strategies, the use of these spaces can contribute to a more effective scientific literacy for both students and teachers. From this perspective, the general objective of this research was to analyze the possibilities and limits of a proposal for the continuous training of teachers from the initial years of Elementary Education, which seeks a re - signification of the relationship between science teaching in non - formal spaces and school teaching practice. In order to meet this objective, the research was carried out from January 2016 to March 2018 at the Center of Sciences and Planetarium of Pará - CCPP, located in the city of Belém in the state of Pará. Subjects were science teachers who worked in classes from the initial years of elementary school and qualitative data were collected through participant observation, questionnaires and interviews. The analysis of the collected data was used the set of techniques of Content Analysis. Through the results obtained from the survey of the profile of the teachers were carried out training actions where the proposal took into account the critical analysis of the teaching reality. A was developed in the period from July to November 2017 and the last meeting took place in May 2018. The training process took place in 5 stages: 4 face-to-face stag... (Complete abstract click electronic access below) / Doutor

[pt] Atualmente, podemos observar uma clara tendência na direção de sistemas cada vez maiores e mais complexos quanto às suas partes e formas de interconexão. Num cenário como este, torna-se imperativa a preocupação com a modelagem da estrutura, organização geral e formas de interação presentes nesses sistemas, assim como com as garantias de que certos requisitos críticos sejam atendidos. O contexto de nosso trabalho engloba disciplinas de Engenharia de Software, como Arquitetura de Software e Técnicas de Modelagem, e disciplinas mais formais como Verificação de Modelos, Lógicas Modais e Álgebras de Processos. Nosso trabalho tem inspirações nestas disciplinas mas apresenta, de fato, um cunho metodológico, localizando-se nas fronteiras da ES com Métodos Formais, onde buscamos investigar e estabelecer uma forma sistemática para utilização efetiva de métodos formais logo nas etapas iniciais do desenvo lvimento. Mais especificamente, mostramos como é possível, a partir de modelos baseados em abstrações arquiteturais, obter-se sistematicamente um modelo formal sobre o qual possamos realizar certos tipos de análise comportamental. Nossa proposta inclui um sistema notacional básico para expressar modelos arquiteturais, junto com sua semântica formal, e um protótipo construído para dar suporte a tarefas de especificação e análise formal orientadas por abstrações arquiteturais. Com isto, pretendemos abordar alguns dos aspectos essenciais de uma metodologia de desenvolvimento que integre ferramentas e técnicas formais na etapa de modelagem arquitetural. / [en] There is a trend nowadays towards bigger and more complex systems concerning their parts and interconnectivity. In such scenario, modeling structure, overall organization and interaction have become a main concern, as well as fulfillment of mission critical requirements. The scope of our work encompasses Software Engineering related subjects such as Software Architecture, Modeling Techniques and more formal disciplines like Model Checking, Modal Logics and Process Algebra. Although inspired by such techniques, there is, indeed a methodological orientation in our work, traversing the boundaries of Software Engineering with Formal Methods, through which we seek to investigate and establish a systematic way for the effective utilization of formal methods in the first steps of software development. Still, more specifically, we show how it is possible, starting from models based on architectural abstractions, to systematically produce a formal model upon which we can execute certain forms of behavior analysis. Our proposal includes a basic notational system to express architectural models along with their formal semantics and a prototype built to support specification and formal analysis tasks oriented by architectural abstractions. With this, we intend to stress some essential aspects of a development methodology which aims to integrate tools and formal techniques to software modeling.

A inferência gramatical lida com o problema de aprender um classificador capaz de reconhecer determinada construção ou característica em um conjunto qualquer de exemplos. Neste trabalho, um modelo de inferência gramatical baseado em uma variante de Programação Genética é proposto. A representação de cada indivíduo é baseada em uma lista ligada de árvores representando o conjunto de produções da gramática. A atuação dos operadores genéticos é feita de forma heurística. Além disto, dois novos operadores genéticos são apresentados. O primeiro, denominado Aprendizagem Incremental, é capaz de reconhecer, com base em exemplos, quais regras de produção estão faltando. O segundo, denominado Expansão, é capaz de prover a diversidade necessária. Em experimentos efetuados, o modelo proposto inferiu com sucesso seis gramáticas regulares e duas gramáticas livres de contexto: parênteses e palíndromos de quatro letras, tanto o comum quanto o disjunto, sendo superior a abordagens recentes. Atualmente, modelos de inferência gramatical têm sido aplicados a problemas de reconhecimento de sequências biológicas de DNA. Neste trabalho, dois problemas de identificação de padrão foram abordados: reconhecimento de promotores e splice-junction. Para o primeiro, o modelo proposto obteve resultado superior a outras abordagens. Para o segundo, o modelo proposto apresentou bons resultados. O modelo foi estendido para o uso de gramáticas fuzzy, mais especificamente, as gramáticas fuzzy fracionárias. Para tal, um método de estimação adequado dos valores da função de pertinência das produções da gramática é proposto. Os resultados obtidos na identificação de splice-junctions comprovam a utilidade do modelo de inferência gramatical fuzzy proposto. / Grammatical inference deals with the task of learning a classifier that can recognize a particular pattern in a set of examples. In this work, a new grammatical inference model based on a variant of Genetic Programming is proposed. In this approach, an individual is a list of structured trees representing their productions. Ordinary genetic operators are modified so as to bias the search and two new operators are proposed. The first one, called Incremental Learning, is able to recognize, based on examples, which productions are missing. The second, called Expansion is able to provide the diversity necessary to achieve convergence. In a suite of experiments performed, the proposed model successfully inferred six regular grammars and two context-free grammars: parentheses and palindromes with four letters, including the disjunct one. Results achieved were better than those obtained by recently published algorithms. Nowadays, grammatical inference has been applied to problems of recognition of biological sequences of DNA. In this work, two problems of this class were addressed: recognition of promoters and splice junction detection. In the former, the proposed model obtained results better than other published approaches. In the latter, the proposed model showed promising results. The model was extended to support fuzzy grammars, namely the fuzzy fractional grammars. Furthermore, an appropriate method of estimation of the values of the production's membership function is also proposed. Results obtained in the identification of splice junctions shows the utility of the fuzzy inference model proposed.

Made available in DSpace on 2014-12-17T15:47:43Z (GMT). No. of bitstreams: 1 PlacidoASN.pdf: 652214 bytes, checksum: b7912104bf8e3ec91262c75b9ef5d36b (MD5) Previous issue date: 2007-09-06 / Coordena??o de Aperfei?oamento de Pessoal de N?vel Superior / Formal methods should be used to specify and verify on-card software in Java Card applications. Furthermore, Java Card programming style requires runtime verification of all input conditions for all on-card methods, where the main goal is to preserve the data in the card. Design by contract, and in particular, the JML language, are an option for this kind of development and verification, as runtime verification is part of the Design by contract method implemented by JML. However, JML and its currently available tools for runtime verification were not designed with Java Card limitations in mind and are not Java Card compliant. In this thesis, we analyze how much of this situation is really intrinsic of Java Card limitations and how much is just a matter of a complete re-design of JML and its tools. We propose the requirements for a new language which is Java Card compliant and indicate the lines on which a compiler for this language should be built. JCML strips from JML non-Java Card aspects such as concurrency and unsupported types. This would not be enough, however, without a great effort in optimization of the verification code generated by its compiler, as this verification code must run on the card. The JCML compiler, although being much more restricted than the one for JML, is able to generate Java Card compliant verification code for some lightweight specifications. As conclusion, we present a Java Card compliant variant of JML, JCML (Java Card Modeling Language), with a preliminary version of its compiler / M?todos formais poderiam ser usados para especificar e verificar software on-card em aplica??es Java Card. O estilo de programa??o para smart cards requer verifica??o em tempo de execu??o para condi??es de entrada em todos os m?todos Java Card, onde o objetivo principal ? preservar os dados do cart?o. Projeto por Contrato, em particular, a linguagem JML, ? uma op??o para este tipo de desenvolvimento e verifica??o, pelo fato da verifica??o em tempo de execu??o ser parte da implementa??o pela JML. Contudo, JML e suas respectivas ferramentas para verifica??o em tempo de execu??o n?o foram projetadas com o foco nas limita??es Java Card, sendo, dessa forma, n?o compat?veis com Java Card. Nesta disserta??o, analisamos o quanto esta situa??o ? realmente intr?nseca ?s limita??es Java Card e, se ? poss?vel re-definir a JML e suas ferramentas. Propomos requisitos para uma nova linguagem, a qual ? compat?vel com Java Card e apresentamos como o compilador desta linguagem pode ser constru?do. JCML retira da JML aspectos n?o definidos em Java Card, como por exemplo, concorr?ncia e tipos n?o suportados. Isto pode n?o ser o bastante, contudo, sem o esfor?o em otimiza??o de c?digo de verifica??o gerado pelo compilador, n?o ? poss?vel gerar c?digo de verifica??o para rodar no cart?o. O compilador JCML, apesar de ser bem mais restrito em rela??o ao compilador JML, est? habilitado a gerar c?digo de verifica??o compat?vel com Java Card, para algumas especifica??es lightweight. Como conclus?o, apresentamos uma variante da JML compat?vel com Java Card, JCML (Java Card Modeling Language), com uma vers?o de seu compilador