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.

Mathematical modelling of the solidification of liquid tin with electromagnetic stirring

It is well known that during alloy solidification, convection currents close to the so-lidification front have an influence on the structure of dendrites, the local solute concentration, the pattern of solid segregation, and eventually the microstructure of the casting and hence its mechanical properties. Controlled stirring of the melt in continuous casting or in ingot solidification is thought to have a beneficial effect. Free convection currents occur naturally due to temperature differences in the melt and for any given configuration, their strength is a function of the degree of superheat present. A more controlled forced convection current can be induced using electro-magnetic stirring. The authors have applied their Control-Volume based MHD method [1, 2] to the problem of tin solidification in an annular crucible with a water-cooled inner wall and a resistance heated outer one, for both free and forced convection situations and for various degrees of superheat. This problem was studied experimentally by Vives and Perry [3] who obtained temperature measurements, front positions and maps of electro-magnetic body force for a range of superheat values. The results of the mathematical model are compared critically against the experimental ones, in order to validate the model and also to demonstrate the usefulness of the coupled solution technique followed, as a predictive tool and a design aid. Figs 6, refs 19.

A reified temporal logic

This paper presents a reified temporal logic for representing and reasoning about temporal and non-temporal relationships between non-temporal assertions. A clear syntax and semantics for the logic is formally provided. Three types of predicates, temporal predicates, non-temporal predicates and meta-predicates, are introduced. Terms of the proposed language are partitioned into three types, temporal terms, non-temporal terms and propositional terms. Reified propositions consist of formulae with each predicate being either a temporal predicate or a meta-predicate. Meta-predicates may take both temporal terms and propositional terms together as arguments or take propositional terms alone. A standard formula of the classical first-order language with each predicate being a non-temporal predicate taking only non-temporal terms as arguments is reified as just a propositional term. A general time ontology has been provided which can be specialized to a variety of existing temporal systems. The new logic allows one to predicate and quantify over propositional terms while according a special status of time; for example, assertions such as ‘effects cannot precede their causes’ is ensured in the logic, and some problematic temporal aspects including the delay time between events and their effects can be conveniently expressed. Applications of the logic are presented including the characterization of the negation of properties and their contextual sentences, and the expression of temporal relations between actions and effects.

Guest Editorial. Special Issue: Temporal logic in engineering

Logic-based models are thriving within artificial intelligence. A great number of new logics have been defined, and their theory investigated. Epistemic logics introduce modal operators for knowledge or belief; deontic logics are about norms, and introduce operators of deontic necessity and possibility (i.e., obligation or prohibition). And then we have a much investigated class—temporal logics—to whose application to engineering this special issue is devoted. This kind of formalism deserves increased widespread recognition and application in engineering, a domain where other kinds of temporal models (e.g., Petri nets) are by now a fairly standard part of the modelling toolbox.

Using mathematical models to predict the development of aircraft cabin fires

Computer based mathematical models describing aircraft fire have a role to play in the design and development of safer aircraft, in the implementation of safer and more rigorous certification criteria and in post mortuum accident investigation. As the cost involved in performing large-scale fire experiments for the next generation 'Ultra High Capacity Aircraft' (UHCA) are expected to be prohibitively high, the development and use of these modelling tools may become essential if these aircraft are to prove a safe and viable reality. By describing the present capabilities and limitations of aircraft fire models, this paper will examine the future development of these models in the areas of large scale applications through parallel computing, combustion modelling and extinguishment modelling.

Performance evaluation of a distributed algorithm for an inverse heat conduction problem

Numerical solutions of realistic 2-D and 3-D inverse problems may require a very large amount of computation. A two-level concept on parallelism is often used to solve such problems. The primary level uses the problem partitioning concept which is a decomposition based on the mathematical/physical problem. The secondary level utilizes the widely used data partitioning concept. A theoretical performance model is built based on the two-level parallelism. The observed performance results obtained from a network of general purpose Sun Sparc stations are compared with the theoretical values. Restrictions of the theoretical model are also discussed.

Computer Museum, School of Computing and Mathematical Sciences, University of Greenwich

Computer equipment, once viewed as leading edge, is quickly condemned as obsolete and banished to basement store rooms or rubbish bins. The magpie instincts of some of the academics and technicians at the University of Greenwich, London, preserved some such relics in cluttered offices and garages to the dismay of colleagues and partners. When the University moved into its new campus in the historic buildings of the Old Royal Naval College in the center of Greenwich, corridor space in King William Court provided an opportunity to display some of this equipment so that students could see these objects and gain a more vivid appreciation of their subject's history.

Demonstration thermo-electric and MHD mathematical models of a 500 kA A1 electrolysis cell

In the present study, a 3D full cell quarter thermo-electric model of a 500kA demonstration cell has been developed and solved. In parallel, a non-linear wave MHD model of the same 500 kA demonstration cell has been developed and solved. A preliminary study of the impact of the interactions between the cell thermo-electric and MHD models will be presented.

Mathematical modelling: a laser soldering process for an optoelectronics butterfly package

For sensitive optoelectronic components, traditional soldering techniques cannot be used because of their inherent sensitivity to thermal stresses. One such component is the Optoelectronic Butterfly Package which houses a laser diode chip aligned to a fibre-optic cable. Even sub-micron misalignment of the fibre optic and laser diode chip can significantly reduce the performance of the device. The high cost of each unit requires that the number of damaged components, via the laser soldering process, are kept to a minimum. Mathematical modelling is undertaken to better understand the laser soldering process and to optimize operational parameters such as solder paste volume, copper pad dimensions, laser solder times for each joint, laser intensity and absorption coefficient. Validation of the model against experimental data will be completed, and will lead to an optimization of the assembly process, through an iterative modelling cycle. This will ultimately reduce costs, improve the process development time and increase consistency in the laser soldering process.

Mathematical modelling of the behaviour of granular material in a computational fluid dynamics framework using micro-mechanical models

In this paper, a Computational Fluid Dynamics framework is presented for the modelling of key processes which involve granular material (i.e. segregation, degradation, caking). Appropriate physical models and sophisticated algorithms have been developed for the correct representation of the different material components in a granular mixture. The various processes, which arise from the micromechanical properties of the different mixture species can be obtained and parametrised in a DEM / experimental framework, thus enabling the continuum theory to correctly account for the micromechanical properties of a granular system. The present study establishes the link between the micromechanics and continuum theory and demonstrates the model capabilities in simulations of processes which are of great importance to the process engineering industry and involve granular materials in complex geometries.

Identification and doing without it, V: A formal mathematical analysis for a case of mix-up of individuals, and of recovery from failure to attain identification

Identification, when sought, is not necessarily obtained. Operational guidance that is normatively acceptable may be necessary for such cases. We proceed to formalize and illustrate modes of exchanges of individual identity, and provide procedures of recovery strategies in specific prescriptions from an ancient body of law for such situations when, for given types of purposes, individuals of some relevant kind had become intermixed and were undistinguishable. Rules were devised, in a variety of domains, for coping with situations that occur if and when the goal of identification was frustrated. We propose or discuss mathematical representations of such recovery procedures.

[Review] M. Feistauer, J. Felcman, I. Straskbraba, Mathematical and Computational Methods for Compressible Flow, Oxford Science Publication, Oxford, ISBN 0198505884, 2004 (535pp.)

The growth of computer power allows the solution of complex problems related to compressible flow, which is an important class of problems in modern day CFD. Over the last 15 years or so, many review works on CFD have been published. This book concerns both mathematical and numerical methods for compressible flow. In particular, it provides a clear cut introduction as well as in depth treatment of modern numerical methods in CFD. This book is organised in two parts. The first part consists of Chapters 1 and 2, and is mainly devoted to theoretical discussions and results. Chapter 1 concerns fundamental physical concepts and theoretical results in gas dynamics. Chapter 2 describes the basic mathematical theory of compressible flow using the inviscid Euler equations and the viscous Navier–Stokes equations. Existence and uniqueness results are also included. The second part consists of modern numerical methods for the Euler and Navier–Stokes equations. Chapter 3 is devoted entirely to the finite volume method for the numerical solution of the Euler equations and covers fundamental concepts such as order of numerical schemes, stability and high-order schemes. The finite volume method is illustrated for 1-D as well as multidimensional Euler equations. Chapter 4 covers the theory of the finite element method and its application to compressible flow. A section is devoted to the combined finite volume–finite element method, and its background theory is also included. Throughout the book numerous examples have been included to demonstrate the numerical methods. The book provides a good insight into the numerical schemes, theoretical analysis, and validation of test problems. It is a very useful reference for applied mathematicians, numerical analysts, and practice engineers. It is also an important reference for postgraduate researchers in the field of scientific computing and CFD.

A mathematical description of the acoustic coupling of the mass/spring model

This paper describes hybrid mathematical model which couples the mechanics of the mass/spring model to the acoustic wave propagation model for use in generating the acoustic signal emitted by complex structures of paper fibres under strain. A discussion of the coupling method is presented including remarks on the errors encountered intrinsic to the discretisation scheme. The numerical results of a vibrating rubber band and a vibrating paper fibre are compared to their experimental counterparts. The fundamental frequencies of the acoustic signals are compared showing a close agreement between the experimental and numerical results

A sound and complete reified temporal logic

There are mainly two known approaches to the representation of temporal information in Computer Science: modal logic approaches (including tense logics and hybrid temporal logics) and predicate logic approaches (including temporal argument methods and reified temporal logics). On one hand, while tense logics, hybrid temporal logics and temporal argument methods enjoy formal theoretical foundations, their expressiveness has been criticised as not power enough for representing general temporal knowledge; on the other hand, although current reified temporal logics provide greater expressive power, most of them lack of complete and sound axiomatic theories. In this paper, we propose a new reified temporal logic with a clear syntax and semantics in terms of a sound and complete axiomatic formalism which retains all the expressive power of the approach of temporal reification.