Flexible proof reuse for software verification

Proof reuse, or analogical reasoning, involves reusing the proof of a source theorem in the proof of a target conjecture. We have developed a method for proof reuse that is based on the generalisation replay paradigm described in the literature, in which a generalisation of the source proof is replayed to construct the target proof. In this paper, we describe the novel aspects of our method, which include a technique for producing more accurate source proof generalisations (using knowledge of the target goal), as well as a flexible replay strategy that allows the user to set various parameters to control the size and the shape of the search space. Finally, we report on the results of applying this method to a case study from the realm of software verification.

Integrating formal specification and software verification and validation

It is not surprising that students are unconvinced about the benefits of formal methods if we do not show them how these methods can be integrated with other activities in the software lifecycle. In this paper, we describe an approach to integrating formal specification with more traditional verification and validation techniques in a course that teaches formal specification and specification-based testing. This is accomplished through a series of assignments on a single software component that involves specifying the component in Object-Z, validating that specification using inspection and a specification animation tool, and then testing an implementation of the specification using test cases derived from the formal specification.

Agent-based distributed software verification

Despite decades of research, the takeup of formal methods for developing provably correct software in industry remains slow. One reason for this is the high cost of proof construction, an activity that, due to the complexity of the required proofs, is typically carried out using interactive theorem provers. In this paper we propose an agent-oriented architecture for interactive theorem proving with the aim of reducing the user interactions (and thus the cost) of constructing software verification proofs. We describe a prototype implementation of our architecture and discuss its application to a small, but non-trivial case study.

Performance-based structural fire design of steel frames using conventional computer software

Fire incident in buildings is common, so the fire safety design of the framed structure is imperative, especially for the unprotected or partly protected bare steel frames. However, software for structural fire analysis is not widely available. As a result, the performance-based structural fire design is urged on the basis of using user-friendly and conventional nonlinear computer analysis programs so that engineers do not need to acquire new structural analysis software for structural fire analysis and design. The tool is desired to have the capacity of simulating the different fire scenarios and associated detrimental effects efficiently, which includes second-order P-D and P-d effects and material yielding. Also the nonlinear behaviour of large-scale structure becomes complicated when under fire, and thus its simulation relies on an efficient and effective numerical analysis to cope with intricate nonlinear effects due to fire. To this end, the present fire study utilizes a second order elastic/plastic analysis software NIDA to predict structural behaviour of bare steel framed structures at elevated temperatures. This fire study considers thermal expansion and material degradation due to heating. Degradation of material strength with increasing temperature is included by a set of temperature-stress-strain curves according to BS5950 Part 8 mainly, which implicitly allows for creep deformation. This finite element stiffness formulation of beam-column elements is derived from the fifth-order PEP element which facilitates the computer modeling by one member per element. The Newton-Raphson method is used in the nonlinear solution procedure in order to trace the nonlinear equilibrium path at specified elevated temperatures. Several numerical and experimental verifications of framed structures are presented and compared against solutions in literature. The proposed method permits engineers to adopt the performance-based structural fire analysis and design using typical second-order nonlinear structural analysis software.

A computer software package for assessing and managing risks posed by experiments with genetically modified fish and shellfish

Assessment and management of risk is needed for sustainable use of genetically modified aquatic organisms (aquatic GMOs). A computer software package for safely conducting research with genetically modified fish and shellfish is described. By answering a series of questions about the organism and the accessible aquatic ecosystem, a researcher or oversight authority can either identify specific risks or conclude that there is a specific reason for safety of the experiment. Risk assessment protocols with examples involving transgenic coho salmon, triploid grass carp and hybrid tilapia are described. In case a specific risk is identified, the user is led to consider risk management measures, involving culture methods, facilities design and operations management, to minimize the risk. Key features of the software are its user-friendly organization; easy access to explanatory text, literature citations and glossary; and automated completion of a worksheet. Documented completion of the Performance Standards can facilitate approval of a well designed experiment by oversight authorities.

Analysing audio-recorded data : using computer software applications

Conventional methods of qualitative data analysis require transcription of audio-recorded data prior to conduct of the coding and analysis process. In this paper Alison Hutchinson describes and illustrates an innovative method of data analysis that comprises the use of audio-editing software to save selected audio bytes from digital audio recordings of meetings. The use of a database to code and manage the linked audio files and generate detailed and summary reports, including reporting of code frequencies according to participant code and/or meeting, is also highlighted. The advantage of using this approach in the analysis of audio-recorded data is that the process may be undertaken in the medium in which the data were collected. Though time-consuming, this process negates the need for expensive and time intensive transcription of recorded data.