JCML: A specification language for the runtime verification of Java Card programs

COSTA, Umberto Souza; MOREIRA, Anamaria Martins; MUSICANTE, Matin A.; SOUZA NETO, Plácido A. JCML: A specification language for the runtime verification of Java Card programs. Science of Computer Programming. [S.l]: [s.n], 2010.

Specification and Runtime Verification of Java Card Programs

COSTA, Umberto Souza da; MOREIRA, Anamaria Martins; MUSICANTE, Martin A. Specification and Runtime Verification of Java Card Programs. Electronic Notes in Theoretical Computer Science. [S.l:s.n], 2009.

Atividade bioinseticida e mecanismo de ação de vicilinas de sementes Erythrina velutina sobre moscas-das frutas Ceratitis capitata

The fruit fly Ceratitis capitata is considered the most destructive pest of the world fruitculture. Many pest management practices, mainly based on agrochemicals, have been developed to allow the world-wide commerce of fruit. Solutions to decrease the use of synthetic insecticides in agriculture are based on the development of new target-specific compounds which cause less damage to the environment, especially vegetal proteins with insecticidal effects. The aim of this work was to evaluate the deleterious effect of a purified vicilin of E. velutina (EvV) seeds to C. capitata larvae and adult insects and to investigate the mechanisms involved in these effects. EvV was purified, characterized and its deleterious effect was tested in bioassay systems. EvV mechanism of action was determined by immunodetection techniques and fluorescence localization in chitin structures that are present in C. capitata digestory system. EvV is a glycoprotein with affinity to chitin. Its molecular weight, of 216,57 kDa, was determined by gel filtration chromatography in FPLC system. Using SDS-PAGE, it was possible to observe EvV dissociation in two main subunits of 54,8 and 50,8 kDa. When it was submitted to eletrophoresis in native conditions, EvV presented only one band of acid characteristic. The WD50 and LD50 values found in the bioassays were 0,13% and 0,14% (w/w), respectively for the larvae. EvV deleterious effects were related to the binding to chitin structures presented in peritrophic membrane and gut epithelial cells, associated with its low digestibility in C. capitata digestive tract. The results described herein are the first demonstration of the larvicidal effects of plant protein on C. capitata larvae. EvV may be part of the pest management programs, in the toxic bait composition, or an alternative in plant improvement program

Formal verification of PLC programs using the B Method

PLCs (acronym for Programmable Logic Controllers) perform control operations, receiving information from the environment, processing it and modifying this same environment according to the results produced. They are commonly used in industry in several applications, from mass transport to petroleum industry. As the complexity of these applications increase, and as various are safety critical, a necessity for ensuring that they are reliable arouses. Testing and simulation are the de-facto methods used in the industry to do so, but they can leave flaws undiscovered. Formal methods can provide more confidence in an application s safety, once they permit their mathematical verification. We make use of the B Method, which has been successfully applied in the formal verification of industrial systems, is supported by several tools and can handle decomposition, refinement, and verification of correctness according to the specification. The method we developed and present in this work automatically generates B models from PLC programs and verify them in terms of safety constraints, manually derived from the system requirements. The scope of our method is the PLC programming languages presented in the IEC 61131-3 standard, although we are also able to verify programs not fully compliant with the standard. Our approach aims to ease the integration of formal methods in the industry through the abbreviation of the effort to perform formal verification in PLCs