Mathematical notation in formal specification: Too difficult for the masses? [Correspondence]

The phrase “not much mathematics required” can imply a variety of skill levels. When this phrase is applied to computer scientists, software engineers, and clients in the area of formal specification, the word “much” can be widely misinterpreted with disastrous consequences. A small experiment in reading specifications revealed that students already trained in discrete mathematics and the specification notation performed very poorly; much worse than could reasonably be expected if formal methods proponents are to be believed.

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.

Aircraft accident statistics and knowledge database: analyzing passenger behavior in aviation accidents

The Aircraft Accident Statistics and Knowledge (AASK) database is a repository of passenger accounts from survivable aviation accidents/incidents compiled from interview data collected by agencies such as the US NTSB. Its main purpose is to store observational and anecdotal data from the actual interviews of the occupants involved in aircraft accidents. The database has wide application to aviation safety analysis, being a source of factual data regarding the evacuation process. It also plays a significant role in the development of the airEXODUS aircraft evacuation model, where insight into how people actually behave during evacuation from survivable aircraft crashes is required. This paper describes the latest version of the database (Version 4.0) and includes some analysis of passenger behavior during actual accidents/incidents.

An analysis of the passenger to cabin crew ratio and exit reliability based on past survivable aviation accidents

A hotly debated issue in the area of aviation safety is the number of cabin crew members required to evacuate an aircraft in the event of an emergency. Most countries regulate the minimum number required for the safe operation of an aircraft, but these rulings are based on little if any scientific evidence. Another issue of concern is the failure rate of exits and slides. This paper examines these issues using the latest version of Aircraft Accident Statistics and Knowledge database AASK V4.0, which contains information from 105 survivable crashes and more than 2,000 survivors, including accounts from 155 cabin crew members.