KitSmart: Uma biblioteca de componentes para o desenvolvimento rigoroso de aplicações Java Card com o método B

The development of smart card applications requires a high level of reliability. Formal methods provide means for this reliability to be achieved. The BSmart method and tool contribute to the development of smart card applications with the support of the B method, generating Java Card code from B specifications. For the development with BSmart to be effectively rigorous without overloading the user it is important to have a library of reusable components built in B. The goal of KitSmart is to provide this support. A first research about the composition of this library was a graduation work from Universidade Federal do Rio Grande do Norte, made by Thiago Dutra in 2006. This first version of the kit resulted in a specification of Java Card primitive types byte, short and boolean in B and the creation of reusable components for application development. This work provides an improvement of KitSmart with the addition of API Java Card specification made in B and a guide for the creation of new components. The API Java Card in B, besides being available to be used for development of applications, is also useful as a documentation of each API class. The reusable components correspond to modules to manipulate specific structures, such as date and time. These structures are not available for B or Java Card. These components for Java Card are generated from specifications formally verified in B. The guide contains quick reference on how to specify some structures and how some situations were adapted from object-orientation to the B Method. This work was evaluated through a case study made through the BSmart tool, that makes use of the KitSmart library. In this case study, it is possible to see the contribution of the components in a B specification. This kit should be useful for B method users and Java Card application developers

The influence of visual inter-hemispheric connections on spiking, assembly and LFP activities, and their phase relationship during figure-ground stimulation

Desde os descobrimentos pioneiros de Hubel e Wiesel acumulou-se uma vasta literatura descrevendo as respostas neuronais do córtex visual primário (V1) a diferentes estímulos visuais. Estes estímulos consistem principalmente em barras em movimento, pontos ou grades, que são úteis para explorar as respostas dentro do campo receptivo clássico (CRF do inglês classical receptive field) a características básicas dos estímulos visuais como a orientação, direção de movimento, contraste, entre outras. Entretanto, nas últimas duas décadas, tornou-se cada vez mais evidente que a atividade de neurônios em V1 pode ser modulada por estímulos fora do CRF. Desta forma, áreas visuais primárias poderiam estar envolvidas em funções visuais mais complexas como, por exemplo, a separação de um objeto ou figura do seu fundo (segregação figura-fundo) e assume-se que as conexões intrínsecas de longo alcance em V1, assim como as conexões de áreas visuais superiores, estão ativamente envolvidas neste processo. Sua possível função foi inferida a partir da análise das variações das respostas induzidas por um estímulo localizado fora do CRF de neurônios individuais. Mesmo sendo muito provável que estas conexões tenham também um impacto tanto na atividade conjunta de neurônios envolvidos no processamento da figura quanto no potencial de campo, estas questões permanecem pouco estudadas. Visando examinar a modulação do contexto visual nessas atividades, coletamos potenciais de ação e potenciais de campo em paralelo de até 48 eletrodos implantados na área visual primária de gatos anestesiados. Estimulamos com grades compostas e cenas naturais, focando-nos na atividade de neurônios cujo CRF estava situado na figura. Da mesma forma, visando examinar a influência das conexões laterais, o sinal proveniente da área visual isotópica e contralateral foi removido através da desativação reversível por resfriamento. Fizemos isso devido a: i) as conexões laterais intrínsecas não podem ser facilmente manipuladas sem afetar diretamente os sinais que estão sendo medidos, ii) as conexões inter-hemisféricas compartilham as principais características anatômicas com a rede lateral intrínseca e podem ser vistas como uma continuação funcional das mesmas entre os dois hemisférios e iii) o resfriamento desativa as conexões de forma causal e reversível, silenciando temporariamente seu sinal, permitindo conclusões diretas a respeito da sua contribuição. Nossos resultados demonstram que o mecanismo de segmentação figurafundo se reflete nas taxas de disparo de neurônios individuais, assim como na potência do potencial de campo e na relação entre sua fase e os padrões de disparo produzidos pela população. Além disso, as conexões laterais inter-hemisféricas modulam estas variáveis dependendo da estimulação feita fora do CRF. Observamos também uma influência deste circuito lateral na coerência entre potenciais de campo entre eletrodos distantes. Em conclusão, nossos resultados dão suporte à ideia de um mecanismo complexo de segmentação figura-fundo atuando desde as áreas visuais primárias em diferentes escalas de frequência. Esse mecanismo parece envolver grupos de neurônios ativos sincronicamente e dependentes da fase do potencial de campo. Nossos resultados também são compatíveis com a hipótese que conexões laterais de longo alcance também fazem parte deste mecanismo