Specification, refinement and verification of concurrent systems - An integration of Object-Z and CSP

This paper presents a method of formally specifying, refining and verifying concurrent systems which uses the object-oriented state-based specification language Object-Z together with the process algebra CSP. Object-Z provides a convenient way of modelling complex data structures needed to define the component processes of such systems, and CSP enables the concise specification of process interactions. The basis of the integration is a semantics of Object-Z classes identical to that of CSP processes. This allows classes specified in Object-Z to he used directly within the CSP part of the specification. In addition to specification, we also discuss refinement and verification in this model. The common semantic basis enables a unified method of refinement to be used, based upon CSP refinement. To enable state-based techniques to be used fur the Object-Z components of a specification we develop state-based refinement relations which are sound and complete with respect to CSP refinement. In addition, a verification method for static and dynamic properties is presented. The method allows us to verify properties of the CSP system specification in terms of its component Object-Z classes by using the laws of the the CSP operators together with the logic for Object-Z.

Visual-auditory integration during speech imitation in autism

Children with autistic spectrum disorder (ASD) may have poor audio-visual integration, possibly reflecting dysfunctional 'mirror neuron' systems which have been hypothesised to be at the core of the condition. In the present study, a computer program, utilizing speech synthesizer software and a 'virtual' head (Baldi), delivered speech stimuli for identification in auditory, visual or bimodal conditions. Children with ASD were poorer than controls at recognizing stimuli in the unimodal conditions, but once performance on this measure was controlled for, no group difference was found in the bimodal condition. A group of participants with ASD were also trained to develop their speech-reading ability. Training improved visual accuracy and this also improved the children's ability to utilize visual information in their processing of speech. Overall results were compared to predictions from mathematical models based on integration and non-integration, and were most consistent with the integration model. We conclude that, whilst they are less accurate in recognizing stimuli in the unimodal condition, children with ASD show normal integration of visual and auditory speech stimuli. Given that training in recognition of visual speech was effective, children with ASD may benefit from multi-modal approaches in imitative therapy and language training. (C) 2004 Elsevier Ltd. All rights reserved.

Understanding technology integration in secondary mathematics: Theorising the role of the teacher

Previous research on computers and graphics calculators in mathematics education has examined effects on curriculum content and students’ mathematical achievement and attitudes while less attention has been given to the relationship between technology use and issues of pedagogy, in particular the impact on teachers’ professional learning in specific classroom and school environments. This observation is critical in the current context of educational policy making, where it is assumed – often incorrectly – that supplying schools with hardware and software will increase teachers’ use of technology and encourage more innovative teaching approaches. This paper reports on a research program that aimed to develop better understanding of how and under what conditions Australian secondary school mathematics teachers learn to effectively integrate technology into their practice. The research adapted Valsiner’s concepts of the Zone of Proximal Development, Zone of Free Movement and Zone of Promoted Action to devise a theoretical framework for analysing relationships between factors influencing teachers’ use of technology in mathematics classrooms. This paper illustrates how the framework may be used by analysing case studies of a novice teacher and an experienced teacher in different school settings.

The BCD transient recorder revisited: firmware for the ISA-to-USB bridging card and software for the graphical user interface

This report describes recent updates to the custom-built data-acquisition hardware operated by the Center for Hypersonics. In 2006, an ISA-to-USB bridging card was developed as part of Luke Hillyard's final-year thesis. This card allows the hardware to be connected to any recent personal computers via a (USB or RS232) serial port and it provides a number of simple text-based commands for control of the hardware. A graphical user interface program was also updated to help the experimenter manage the data acquisition functions. Sampled data is stored in text files that have been compressed with the gzip for mat. To simplify the later archiving or transport of the data, all files specific to a shot are stored in a single directory. This includes a text file for the run description, the signal configuration file and the individual sampled-data files, one for each signal that was recorded.

XSophe-Sophe-XeprView (R). A computer simulation software suite (v. 1.1.3) for the analysis of continuous wave EPR spectra

The XSophe-Sophe-XeprView((R)) computer simulation software suite enables scientists to easily determine spin Hamiltonian parameters from isotropic, randomly oriented and single crystal continuous wave electron paramagnetic resonance (CW EPR) spectra from radicals and isolated paramagnetic metal ion centers or clusters found in metalloproteins, chemical systems and materials science. XSophe provides an X-windows graphical user interface to the Sophe programme and allows: creation of multiple input files, local and remote execution of Sophe, the display of sophelog (output from Sophe) and input parameters/files. Sophe is a sophisticated computer simulation software programme employing a number of innovative technologies including; the Sydney OPera HousE (SOPHE) partition and interpolation schemes, a field segmentation algorithm, the mosaic misorientation linewidth model, parallelization and spectral optimisation. In conjunction with the SOPHE partition scheme and the field segmentation algorithm, the SOPHE interpolation scheme and the mosaic misorientation linewidth model greatly increase the speed of simulations for most spin systems. Employing brute force matrix diagonalization in the simulation of an EPR spectrum from a high spin Cr(III) complex with the spin Hamiltonian parameters g(e) = 2.00, D = 0.10 cm(-1), E/D = 0.25, A(x) = 120.0, A(y) = 120.0, A(z) = 240.0 x 10(-4) cm(-1) requires a SOPHE grid size of N = 400 (to produce a good signal to noise ratio) and takes 229.47 s. In contrast the use of either the SOPHE interpolation scheme or the mosaic misorientation linewidth model requires a SOPHE grid size of only N = 18 and takes 44.08 and 0.79 s, respectively. Results from Sophe are transferred via the Common Object Request Broker Architecture (CORBA) to XSophe and subsequently to XeprView((R)) where the simulated CW EPR spectra (1D and 2D) can be compared to the experimental spectra. Energy level diagrams, transition roadmaps and transition surfaces aid the interpretation of complicated randomly oriented CW EPR spectra and can be viewed with a web browser and an OpenInventor scene graph viewer.

Using FCD Mapper Software and Landsat Images to Assess Forest Canopy Density in Landscapes in Australia and the Philippines

Using Landsat imagery, forest canopy density (FCD) estimated with the FCD Mapper®, was correlated with predominant height (PDH, measured as the average height of the tallest 50 trees per hectare) for 20 field plots measured in native forest at Noosa Heads, south-east Queensland, Australia. A corresponding image was used to calculate FCD in Leyte Island, the Philippines and was validated on the ground for accuracy. The FCD Mapper was produced for the International Tropical Timber Organisation and estimates FCD as an index of canopy density using reflectance characteristics of Landsat Enhanced Thematic (ETM) Mapper images. The FCD Mapper is a ‘semi-expert’ computer program which uses interactive screens to allow the operator to make decisions concerning the classification of land into bare soil, grass and forest. At Noosa, a positive strong nonlinear relationship (r2 = 0.86) was found between FCD and PDH for 15 field plots with variable PDH but complete canopy closure. An additional five field plots were measured in forest with a broken canopy and the software assessed these plots as having a much lower FCD than forest with canopy closure. FCD estimates for forest and agricultural land in the island of Leyte and subsequent field validation showed that at appropriate settings, the FCD Mapper differentiated between tropical rainforest and banana or coconut plantation. These findings suggest that in forests with a closed canopy this remote sensing technique has promise for forest inventory and productivity assessment. The findings also suggest that the software has promise for discriminating between native forest with a complete canopy and forest which has a broken canopy, such as coconut or banana plantation.