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

Java Card technology allows the development and execution of small applications embedded in smart cards. A Java Card application is composed of an external card client and of an application in the card that implements the services available to the client by means of an Application Programming Interface (API). Usually, these applications manipulate and store important information, such as cash and confidential data of their owners. Thus, it is necessary to adopt rigor on developing a smart card application to improve its quality and trustworthiness. The use of formal methods on the development of these applications is a way to reach these quality requirements. The B method is one of the many formal methods for system specification. The development in B starts with the functional specification of the system, continues with the application of some optional refinements to the specification and, from the last level of refinement, it is possible to generate code for some programming language. The B formalism has a good tool support and its application to Java Card is adequate since the specification and development of APIs is one of the major applications of B. The BSmart method proposed here aims to promote the rigorous development of Java Card applications up to the generation of its code, based on the refinement of its formal specification described in the B notation. This development is supported by the BSmart tool, that is composed of some programs that automate each stage of the method; and by a library of B modules and Java Card classes that model primitive types, essential Java Card API classes and reusable data structures

Geração automática de testes a partir de descrições de linguagens

Some programs may have their entry data specified by formalized context-free grammars. This formalization facilitates the use of tools in the systematization and the rise of the quality of their test process. This category of programs, compilers have been the first to use this kind of tool for the automation of their tests. In this work we present an approach for definition of tests from the formal description of the entries of the program. The generation of the sentences is performed by taking into account syntactic aspects defined by the specification of the entries, the grammar. For optimization, their coverage criteria are used to limit the quantity of tests without diminishing their quality. Our approach uses these criteria to drive generation to produce sentences that satisfy a specific coverage criterion. The approach presented is based on the use of Lua language, relying heavily on its resources of coroutines and dynamic construction of functions. With these resources, we propose a simple and compact implementation that can be optimized and controlled in different ways, in order to seek satisfaction the different implemented coverage criteria. To make the use of our tool simpler, the EBNF notation for the specification of the entries was adopted. Its parser was specified in the tool Meta-Environment for rapid prototyping

Postoperative renal function evaluation, through RIFLE criteria, of elderly patients who underwent femur fracture surgery under spinal anesthesia

Introduction. The postoperative acute renal failure (ARF) incidence in different kinds of surgery has rarely been studied. Age, cardiac dysfunction, previous renal dysfunction, intraoperative hypoperfusion, and use of nephrotoxic medications are mentioned as risk factors for ARF at the postoperative period. The postoperative ARF definition was based on the creatinine increase by the RIFLE classification (R = risk, I = injury, F = failure, L = loss, E = end stage), which corresponds to a 1.5 creatinine increase, two to three times, respectively, above the basal value. This study aimed to evaluate the postoperative ARF incidence in elderly patients who underwent femur fracture surgery under subarachnoid anesthesia and stratify it by the RIFLE criteria. Methods. Ninety patients older than 65 years under spinal anesthesia with fixed dosage of 15 mg of 0.5% isobaric bupivacaine associated with morphine 50 g were studied. Immediate postoperative creatinine was considered basal and compared with maximal creatinine evaluated at 24, 48, and 72 postoperative hours. Results. The mean age of the patients was 80.27 years. ARF incidence was 24.44% and stratified this way: R = 21.11% and I = 3.33%. Conclusions. In conclusion, the postoperative ARF incidence after femur fracture surgery in patients over 65 years was 24.44%. By analyzing the stratification based on the RIFLE classification, the incidence was categorized as Risk (R) = 21.11% and Injury (I) = 3.33%.

Beta: uma ferramenta para geração de testes de unidade a partir de especificações B

Formal methods and software testing are tools to obtain and control software quality. When used together, they provide mechanisms for software specification, verification and error detection. Even though formal methods allow software to be mathematically verified, they are not enough to assure that a system is free of faults, thus, software testing techniques are necessary to complement the process of verification and validation of a system. Model Based Testing techniques allow tests to be generated from other software artifacts such as specifications and abstract models. Using formal specifications as basis for test creation, we can generate better quality tests, because these specifications are usually precise and free of ambiguity. Fernanda Souza (2009) proposed a method to define test cases from B Method specifications. This method used information from the machine s invariant and the operation s precondition to define positive and negative test cases for an operation, using equivalent class partitioning and boundary value analysis based techniques. However, the method proposed in 2009 was not automated and had conceptual deficiencies like, for instance, it did not fit in a well defined coverage criteria classification. We started our work with a case study that applied the method in an example of B specification from the industry. Based in this case study we ve obtained subsidies to improve it. In our work we evolved the proposed method, rewriting it and adding characteristics to make it compatible with a test classification used by the community. We also improved the method to support specifications structured in different components, to use information from the operation s behavior on the test case generation process and to use new coverage criterias. Besides, we have implemented a tool to automate the method and we have submitted it to more complex case studies

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

Geração de testes a partir de gramáticas: áreas de aplicação

The work proposed by Cleverton Hentz (2010) presented an approach to define tests from the formal description of a program s input. Since some programs, such as compilers, may have their inputs formalized through grammars, it is common to use context-free grammars to specify the set of its valid entries. In the original work the author developed a tool that automatically generates tests for compilers. In the present work we identify types of problems in various areas where grammars are used to describe them , for example, to specify software configurations, which are potential situations to use LGen. In addition, we conducted case studies with grammars of different domains and from these studies it was possible to evaluate the behavior and performance of LGen during the generation of sentences, evaluating aspects such as execution time, number of generated sentences and satisfaction of coverage criteria available in LGen

Verificação formal automatizada para sistemas de raciocínio procedural (PRS) utilizando redes de petri coloridas (RPC)

Este trabalho apresenta uma técnica de verificação formal de Sistemas de Raciocínio Procedural, PRS (Procedural Reasoning System), uma linguagem de programação que utiliza a abordagem do raciocínio procedural. Esta técnica baseia-se na utilização de regras de conversão entre programas PRS e Redes de Petri Coloridas (RPC). Para isso, são apresentadas regras de conversão de um sub-conjunto bem expressivo da maioria da sintaxe utilizada na linguagem PRS para RPC. A fim de proceder fia verificação formal do programa PRS especificado, uma vez que se disponha da rede de Petri equivalente ao programa PRS, utilizamos o formalismo das RPCs (verificação das propriedades estruturais e comportamentais) para analisarmos formalmente o programa PRS equivalente. Utilizamos uma ferramenta computacional disponível para desenhar, simular e analisar as redes de Petri coloridas geradas. Uma vez que disponhamos das regras de conversão PRS-RPC, podemos ser levados a querer fazer esta conversão de maneira estritamente manual. No entanto, a probabilidade de introdução de erros na conversão é grande, fazendo com que o esforço necessário para garantirmos a corretude da conversão manual seja da mesma ordem de grandeza que a eliminação de eventuais erros diretamente no programa PRS original. Assim, a conversão automatizada é de suma importância para evitar que a conversão manual nos leve a erros indesejáveis, podendo invalidar todo o processo de conversão. A principal contribuição deste trabalho de pesquisa diz respeito ao desenvolvimento de uma técnica de verificação formal automatizada que consiste basicamente em duas etapas distintas, embora inter-relacionadas. A primeira fase diz respeito fias regras de conversão de PRS para RPC. A segunda fase é concernente ao desenvolvimento de um conversor para fazer a transformação de maneira automatizada dos programas PRS para as RPCs. A conversão automática é possível, porque todas as regras de conversão apresentadas seguem leis de formação genéricas, passíveis de serem incluídas em algoritmos

Motile sperm organelle morphology examination is stricter than Tygerberg criteria

The present study aimed to evaluate the correlation between the motile sperm organelle morphology examination (MSOME) and a well-known sperm morphology classification (Tygerberg criteria). For MSOME, spermatozoa were analysed at x8400 magnification by inverted microscope equipped with Nomarski differential interference contrast optics, Uplan Apo x 100 oil/1.35 objective lens and variable zoom lens. By Tygerberg criteria, the semen underwent morphological evaluation as described in the literature. Regression analysis demonstrated significant positive correlation between percentage of normal sperm forms by Tygerberg criteria and by MSOME (r = 0.83, P < 0.0001). However, the incidence of normal spermatozoa by Tygerberg criteria (9.4%) was significantly higher (P < 0.0001) than under MSOME (3.3%). Despite the highly positive correlation, MSOME is a much stricter criterion of sperm morphology classification, since it identifies vacuoles and chromatin abnormalities that are not evaluated with the same precision by the analysis of Tygerberg criteria. MSOME should be included among the routine criteria for semen analysis. In addition, MSOME should be used for selection of spermatozoa for intracytoplasmic sperm injection based on the already published literature, as this is a good selection tool.

Critical analysis of the international classification of headache disorders diagnostic criteria (ICHD I-1988) and (ICHD II-2004), for migraine in children and adolescents

The present study analyzed the (ICHD I-1988) and ( ICHD II-2004) diagnostic criteria in children and adolescents. Our population consisted of 496 patients of the Headache Outpatient Ward for Children and Adolescents retrospectively studied from 1992 to 2002. Individuals were classified according to three diagnostic groups: Intuitive Clinical Diagnosis ( Gold Standard), ICHD I-1988 and ICHD II-2004. They were statistically compared using the variables: Sensitivity ( S), Specificity (Sp), Positive Predictive Value (PPV), Negative Predictive Value (NPV). When ICHD I-1988 was used, the sensitivity of migraine without and with aura was 21% and 27%, respectively, whereas in ICHD II-2004 it changed to 53% and 71% without affecting specificity. As a conclusion, the current classification criteria ( ICHD II-2004) showed greater sensitivity and high specificity for migraine than ICHD I-1988, although it improved migraine diagnosis in children and adolescents, the sensitivity remains poor.

Metabolic syndrome in overweight children from the city of Botucatu - São Paulo State - Brazil: agreement among six diagnostic criteria

Coordenação de Aperfeiçoamento de Pessoal de Nível Superior (CAPES)

EULAR/PRINTO/PRES criteria for Henoch-Schonlein purpura, childhood polyarteritis nodosa, childhood Wegener granulomatosis and childhood Takayasu arteritis: Ankara 2008. Part I: Overall methodology and clinical characterisation

Objectives To report methodology and overall clinical, laboratory and radiographic characteristics for Henoch-Schonlein purpura (HSP), childhood polyarteritis nodosa (c-PAN), c-Wegener granulomatosis (c-WG) and c-Takayasu arteritis (c-TA) classification criteria.Methods The preliminary Vienna 2005 consensus conference, which proposed preliminary criteria for paediatric vasculitides, was followed by a EULAR/PRINTO/PRES-supported validation project divided into three main steps. Step 1: retrospective/prospective web-data collection for HSP, c-PAN, c-WG and c-TA, with age at diagnosis <= 18 years. Step 2: blinded classification by consensus panel of a subgroup of 280 cases (128 difficult cases, 152 randomly selected) enabling expert diagnostic verification. Step 3: Ankara 2008 Consensus Conference and statistical evaluation (sensitivity, specificity, area under the curve, kappa-agreement) using as 'gold standard' the final consensus classification or original treating physician diagnosis.Results A total of 1183/1398 (85%) samples collected were available for analysis: 827 HSP, 150 c-PAN, 60 c-WG, 87 c-TA and 59 c-other. Prevalence, signs/symptoms, laboratory, biopsy and imaging reports were consistent with the clinical picture of the four c-vasculitides. A representative subgroup of 280 patients was blinded to the treating physician diagnosis and classified by a consensus panel, with kappa-agreement of 0.96 for HSP (95% CI 0.84 to 1), 0.88 for c-WG (95% CI 0.76 to 0.99), 0.84 for c-TA (95% CI 0.73 to 0.96) and 0.73 for c-PAN (95% CI 0.62 to 0.84), with an overall. of 0.79 (95% CI 0.73 to 0.84).Conclusion EULAR/PRINTO/PRES propose validated classification criteria for HSP, c-PAN, c-WG and c-TA, with substantial/almost perfect agreement with the final consensus classification or original treating physician diagnosis.

Preliminary Criteria for Global Flares in Childhood-Onset Systemic Lupus Erythematosus

Objective. To develop widely acceptable preliminary criteria of global flare for childhood-onset systemic lupus erythematosus (cSLE).Methods. Pediatric rheumatologists (n = 138) rated a total of 358 unique patient profiles with information about the cSLE flare descriptors from 2 consecutive visits: patient global assessment of well-being, physician global assessment of disease activity (MD-global), health-related quality of life, anti-double-stranded DNA antibodies, disease activity index scores, protein: creatinine (P:C) ratio, complement levels, and erythrocyte sedimentation rate (ESR). Based on 2,996 rater responses about the course of cSLE (baseline versus followup), the accuracy (sensitivity, specificity, and area under the receiver operating characteristic curve) of candidate flare criteria was assessed. An international consensus conference was held to rank these candidate flare criteria as per the American College of Rheumatology recommendations for the development and validation of criteria sets.Results. The highest-ranked candidate criteria considered absolute changes (Delta) of the Systemic Lupus Erythematosus Disease Activity Index (SLEDAI) or British Isles Lupus Assessment Group (BILAG), MD-global, P:C ratio, and ESR; flare scores can be calculated (0.5 x Delta SLEDAI + 0.45 x Delta P:C ratio + 0.5 x Delta MD-global + 0.02 x Delta ESR), where values of >= 1.04 are reflective of a flare. Similarly, BILAG-based flare scores (0.4 x Delta BILAG + Delta 0.65 x Delta P:C ratio + 0.5 + Delta MD-global + 0.02 x Delta ESR) of >= 1.15 were diagnostic of a flare. Flare scores increased with flare severity.Conclusion. Consensus has been reached on preliminary criteria for global flares in cSLE. Further validation studies are needed to confirm the usefulness of the cSLE flare criteria in research and for clinical care.

Multi-criteria spatial decision analysis for demarcation of greenway: A case study of the city of Rio Claro, São Paulo, Brazil

Concern regarding hydrological resources has been a theme of growing importance in Brazil, associating the development of new management policies and maintenance of natural areas related to rivers. An efficient way to maintain natural areas around rivers has been the development of greenways, and some cites have already adopted specific legislation in this respect. Following this growing evolution in the treatment of hydrological resources, this study was carried out to demarcate a greenway along the Corumbatai River in the state of São Paulo, Using multi-criteria analysis in a GIS environment. First, thematic maps were elaborated based on Landsat 7 satellite, aerial photographs and digital topographic base, Supported by field activities. With the use of multi-criteria analysis, for which ad hoe consultations were conducted to attribute weights to the thematic maps, a suitability map was elaborated for the allocation of the greenway. Sites that should be included in the greenway were also selected, such as areas appropriate for leisure activities, and ecologically important areas. Based on the suitability map, a pathway analysis was done, connecting the relevant points of interest, thus generating a greenway that runs along the Corumbatai River, with the aim of contributing to the conservation of this important hydrological resource. (c) 2007 Elsevier B.V. All rights reserved.