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

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

Does a mandibular RDP and new maxillary CD improve masticatory efficiency and quality of life in patients with a mandibular Kennedy class I arch?

Objectives To evaluate the change in masticatory efficiency and quality of life of patients treated with mandibular Kennedy class I removable partial dentures (RPDs) and maxillary complete dentures at the Department of Dentistry of the Federal University of Rio Grande do Norte. Materials and methods A total of 33 Kennedy class I patients were rehabilitated with maxillary complete dentures, and mandibular RPDs were selected for this non-randomized prospective intervention study. The patients had a mean age of 59.1 years. Masticatory efficiency was evaluated by colorimetric assay using fuchsin capsules. The measurements were conducted at baseline and 2 and 6 months after prosthesis insertion. Quality of life was evaluated using the Oral Health Impact Profile (OHIP-14) at baseline and 6 months after denture insertion. The Kolmogorov-Smirnov normality test was applied. Masticatory efficiency was evaluated by repeated measures ANOVA. Oral health-related quality of life was compared using the paired t test. Results There was no statistically significant difference in masticatory efficiency after denture insertion (p = 0.101). Significant differences were found (p = 0.010) for oral health-related quality of life. A significant improvement in psychological discomfort (p < 0.01) and psychological disability (p < 0.01) was observed. Mean difference value (95 % confidence interval) was 6.8 (3.8 to 9.7) points, reflecting a low impact of oral health on quality of life, considering the 0–56 range of variation of the OHIP-14 and a Cohen’s d of 1.13. Conclusion According to the results of the present study, rehabilitation with Kennedy class I RPDs and complete dentures did not influence masticatory efficiency but improved oral health-related quality of life. Clinical relevance The association between the patient’s quality of life and the masticatory efficiency is important for treatment predictability.