Measuring the comprehensibility of Z specifications

The effects of natural language comments, meaningful variable names, and structure on the comprehensibility of Z specifications are investigated through a designed experiment conducted with a range of undergraduate and post-graduate student subjects. The times taken on three assessment questions are analysed and related to the abilities of the students as indicated by their total score, with the result that stronger students need less time than weaker students to complete the assessment. Individual question scores, and total score, are then analysed and the influence of comments, naming, structure and level of student's class are determined. In the whole experimental group, only meaningful naming significantly enhances comprehension. In contrast, for those obtaining the best score of 3/3 the only significant factor is commenting. Finally, the subjects' ratings of the five specifications used in the study in terms of their perceived comprehensibility have been analysed. Comments, naming and structure are again found to be of importance in the group when analysed as a whole, but in the sub-group of best performing subjects only the comments had an effect on perceived comprehensibility.

Evaluating the effectiveness of Z: The claims made about CICS and where we go from here

There have been few genuine success stories about industrial use of formal methods. Perhaps the best known and most celebrated is the use of Z by IBM (in collaboration with Oxford University's Programming Research Group) during the development of CICS/ESA (version 3.1). This work was rewarded with the prestigious Queen's Award for Technological Achievement in 1992 and is especially notable for two reasons: 1) because it is a commercial, rather than safety- or security-critical, system and 2) because the claims made about the effectiveness of Z are quantitative as well as qualitative. The most widely publicized claims are: less than half the normal number of customer-reported errors and a 9% savings in the total development costs of the release. This paper provides an independent assessment of the effectiveness of using Z on CICS based on the set of public domain documents. Using this evidence, we believe that the case study was important and valuable, but that the quantitative claims have not been substantiated. The intellectual arguments and rationale for formal methods are attractive, but their widespread commercial use is ultimately dependent upon more convincing quantitative demonstrations of effectiveness. Despite the pioneering efforts of IBM and PRG, there is still a need for rigorous, measurement-based case studies to assess when and how the methods are most effective. We describe how future similar case studies could be improved so that the results are more rigorous and conclusive.

A multilevel algorithm for force-directed graph drawing

We describe a heuristic method for drawing graphs which uses a multilevel technique combined with a force-directed placement algorithm. The multilevel process groups vertices to form clusters, uses the clusters to define a new graph and is repeated until the graph size falls below some threshold. The coarsest graph is then given an initial layout and the layout is successively refined on all the graphs starting with the coarsest and ending with the original. In this way the multilevel algorithm both accelerates and gives a more global quality to the force- directed placement. The algorithm can compute both 2 & 3 dimensional layouts and we demonstrate it on a number of examples ranging from 500 to 225,000 vertices. It is also very fast and can compute a 2D layout of a sparse graph in around 30 seconds for a 10,000 vertex graph to around 10 minutes for the largest graph. This is an order of magnitude faster than recent implementations of force-directed placement algorithms.

No-flow underfill flip chip assembly–an experimental and modeling analysis

In the flip-chip assembly process, no-flow underfill materials have a particular advantage over traditional underfill: the application and curing of the former can be undertaken before and during the reflow process. This advantage can be exploited to increase the flip-chip manufacturing throughput. However, adopting a no-flow underfill process may introduce reliability issues such as underfill entrapment, delamination at interfaces between underfill and other materials, and lower solder joint fatigue life. This paper presents an analysis on the assembly and the reliability of flip-chips with no-flow underfill. The methodology adopted in the work is a combination of experimental and computer-modeling methods. Two types of no-flow underfill materials have been used for the flip chips. The samples have been inspected with X-ray and scanning acoustic microscope inspection systems to find voids and other defects. Eleven samples for each type of underfill material have been subjected to thermal shock test and the number of cycles to failure for these flip chips have been found. In the computer modeling part of the work, a comprehensive parametric study has provided details on the relationship between the material properties and reliability, and on how underfill entrapment may affect the thermal–mechanical fatigue life of flip chips with no-flow underfill.

An improved approximation algorithm for the two-machine open shop scheduling problem with family setup times

We consider the problem of scheduling families of jobs in a two-machine open shop so as to minimize the makespan. The jobs of each family can be partitioned into batches and a family setup time on each machine is required before the first job is processed, and when a machine switches from processing a job of some family to a job of another family. For this NP-hard problem the literature contains (5/4)-approximation algorithms that cannot be improved on using the class of group technology algorithms in which each family is kept as a single batch. We demonstrate that there is no advantage in splitting a family more than once. We present an algorithm that splits one family at most once on a machine and delivers a worst-case performance ratio of 6/5.