Linear temporal logic and z refinement

Since Z, being a state-based language, describes a system in terms of its state and potential state changes, it is natural to want to describe properties of a specified system also in terms of its state. One means of doing this is to use Linear Temporal Logic (LTL) in which properties about the state of a system over time can be captured. This, however, raises the question of whether these properties are preserved under refinement. Refinement is observation preserving and the state of a specified system is regarded as internal and, hence, non-observable. In this paper, we investigate this issue by addressing the following questions. Given that a Z specification A is refined by a Z specification C, and that P is a temporal logic property which holds for A, what temporal logic property Q can we deduce holds for C? Furthermore, under what circumstances does the property Q preserve the intended meaning of the property P? The paper answers these questions for LTL, but the approach could also be applied to other temporal logics over states such as CTL and the mgr-calculus.

A formal object-oriented approach to defining consistency constraints for UML models

We discuss how integrity consistency constraints between different UML models can be precisely defined at a language level. In doing so, we introduce a formal object-oriented metamodeling approach. In the approach, integrity consistency constraints between UML models are defined in terms of invariants of the UML model elements used to define the models at the language-level. Adopting a formal approach, constraints are formally defined using Object-Z. We demonstrate how integrity consistency constraints for UML models can be precisely defined at the language-level and once completed, the formal description of the consistency constraints will be a precise reference of checking consistency of UML models as well as for tool development.

Motion analysis of right ventricular wall based on an electromechanical biventricular model

Based on our previously developed electrical heart model, an electromechanical biventricular model, which couples the electrical property and mechanical property of the heart, was constructed and the right ventricular wall motion and deformation was simulated using this model. The model was developed on the basis of composite material theory and finite element method. The excitation propagation was simulated by electrical heart model, and the resultant active forces were used to study the ventricular wall motion during systole. The simulation results show that: (1) The right ventricular free wall moves towards the septum, and at the same time, the base and middle of free wall move towards the apex, which reduce the volume of right ventricle; (2) The minimum principle strain (E3) is largest at the apex, then at the middle of free wall, and its direction is in the approximate direction of epicardial muscle fibers. These results are in good accordance with solutions obtained from MR tagging images. It suggests that such electromechanical biventricular model can be used to assess the mechanical function of two ventricles.

A concept for hip prosthesis identification using ultra wideband radar

Ultra wideband (UWB) radar has been extensively investigated both theoretically and practically for the identification buried artifacts. Ground probe radar (GPR) concentrates on the identification of lightly buried land mines, unexploded ordnance (UXO) and archeological targets. The same technology is proposed in a similar context for the rapid identification of in vivo implanted metallic prostheses. The technique is based on resonance based target identification and the paper investigates UWB scattering from a metallic hip prosthesis in free space as a first step in the identification process.

Numerical evaluation of e-fields induced by body motion near high-field MRI scanner

In modern magnetic resonance imaging (MRI), both patients and radiologists are exposed to strong, nonuniform static magnetic fields inside or outside of the scanner, in which the body movement may be able to induce electric currents in tissues which could be possibly harmful. This paper presents theoretical investigations into the spatial distribution of induced E-fields in the human model when moving at various positions around the magnet. The numerical calculations are based on an efficient, quasistatic, finite-difference scheme and an anatomically realistic, full-body, male model. 3D field profiles from an actively-shielded 4 T magnet system are used and the body model projected through the field profile with normalized velocity. The simulation shows that it is possible to induce E-fields/currents near the level of physiological significance under some circumstances and provides insight into the spatial characteristics of the induced fields. The results are easy to extrapolate to very high field strengths for the safety evaluation at a variety of field strengths and motion velocities.

An equivalent distributed magnetic current based FDTD method for the calculation of e-fields induced by gradient coils in MRI

This paper evaluates a low-frequency FDTD method applied to the problem of induced E-fields/eddy currents in the human body resulting from the pulsed magnetic field gradients in MRI. In this algorithm, a distributed equivalent magnetic current (DEMC) is proposed as the electromagnetic source and is obtained by quasistatic calculation of the empty coil's vector potential or measurements therein. This technique circumvents the discretizing of complicated gradient coil geometries into a mesh of Yee cells, and thereby enables any type of gradient coil modeling or other complex low frequency sources. The proposed method has been verified against an example with an analytical solution. Results are presented showing the spatial distribution of gradient-induced electric fields in a multilayered spherical phantom model and a complete body model.

Formalising behaviour trees with CSP

Behaviour Trees is a novel approach for requirements engineering. It advocates a graphical tree notation that is easy to use and to understand. Individual requirements axe modelled as single trees which later on are integrated into a model of the system as a whole. We develop a formal semantics for a subset of Behaviour Trees using CSP. This work, on one hand, provides tool support for Behaviour Trees. On the other hand, it builds a front-end to a subset of the CSP notation and gives CSP users a new modelling strategy which is well suited to the challenges of requirements engineering.

Viewpoint-based testing of concurrent components

The use of multiple partial viewpoints is recommended for specification. We believe they also can be useful for devising strategies for testing. In this paper, we use Object-Z to formally specify concurrent Java components from viewpoints based on the separation of application and synchronisation concerns inherent in Java monitors. We then use the Test-Template Framework on the Object-Z viewpoints to devise a strategy for testing the components. When combining the test templates for the different viewpoints we focus on the observable behaviour of the application to systematically derive a practical testing strategy. The Producer-Consumer and Readers-Writers problems are considered as case studies.

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.

Mutation-based exploration of a method for verifying concurrent Java components

Summary form only given. The Java programming language supports concurrency. Concurrent programs are harder to verify than their sequential counterparts due to their inherent nondeterminism and a number of specific concurrency problems such as interference and deadlock. In previous work, we proposed a method for verifying concurrent Java components based on a mix of code inspection, static analysis tools, and the ConAn testing tool. The method was derived from an analysis of concurrency failures in Java components, but was not applied in practice. In this paper, we explore the method by applying it to an implementation of the well-known readers-writers problem and a number of mutants of that implementation. We only apply it to a single, well-known example, and so we do not attempt to draw any general conclusions about the applicability or effectiveness of the method. However, the exploration does point out several strengths and weaknesses in the method, which enable us to fine-tune the method before we carry out a more formal evaluation on other, more realistic components.

A case study in specification and implementation testing

Achieving consistency between a specification and its implementation is an important part of software development In previous work, we have presented a method and tool support for testing a formal specification using animation and then verifying an implementation of that specification. The method is based on a testgraph, which provides a partial model of the application under test. The testgraph is used in combination with an animator to generate test sequences for testing the formal specification. The same testgraph is used during testing to execute those same sequences on the implementation and to ensure that the implementation conforms to the specification. So far, the method and its tool support have been applied to software components that can be accessed through an application programmer interface (API). In this paper, we use an industrially-based case study to discuss the problems associated with applying the method to a software system with a graphical user interface (GUI). In particular, the lack of a standardised interface, as well as controllability and observability problems, make it difficult to automate the testing of the implementation. The method can still be applied, but the amount of testing that can be carried on the implementation is limited by the manual effort involved.

Testing java interrupts and timed waits

Testing concurrent software is difficult due to problems with inherent nondeterminism. In previous work, we have presented a method and tool support for the testing of concurrent Java components. In this paper, we extend that work by presenting and discussing techniques for testing Java thread interrupts and timed waits. Testing thread interrupts is important because every Java component that calls wait must have code dealing with these interrupts. For a component that uses interrupts and timed waits to provide its basic functionality, the ability to test these features is clearly even more important. We discuss the application of the techniques and tool support to one such component, which is a nontrivial implementation of the readers-writers problem.