Concurreny based transition refinement for the verification of distributed algorithms

We suggest a new notion of behaviour preserving transition refinement based on partial order semantics. This notion is called transition refinement. We introduced transition refinement for elementary (low-level) Petri Nets earlier. For modelling and verifying complex distributed algorithms, high-level (Algebraic) Petri nets are usually used. In this paper, we define transition refinement for Algebraic Petri Nets. This notion is more powerful than transition refinement for elementary Petri nets because it corresponds to the simultaneous refinement of several transitions in an elementary Petri net. Transition refinement is particularly suitable for refinement steps that increase the degree of distribution of an algorithm, e.g. when synchronous communication is replaced by asynchronous message passing. We study how to prove that a replacement of a transition is a transition refinement.

SPINAL POSTURAL ALIGNMENT VARIANCE ACCORDING TO SEX AND AGE IN 7-AND 8-YEAR-OLD CHILDREN

Purpose: Children`s postural alignment undergoes many adjustments due to the changes in body proportions during the stages of growth. The objective of this study was to quantitatively characterize and analyze spinal postural standards in 7- and 8-year-old children to verify which of the differences found were correlated to age and sex. Methods: Two hundred thirty public school students (Amparo, Sao Paulo, Brazil) aged 7 to 8 years were divided into groups according to postural alignment, which were further subdivided by sex and age, for comparison. Digital photos of upright Subjects were analyzed to evaluate posture. Lumbar and thoracic curvature, pelvic inclination, head posture, and lateral spine deviation were measured using CorelDraw (Ottawa, Canada) software guidelines and bone landmarks. Descriptive statistics and analysis of variance data analysis were utilized to verify differences among the groups. This was a cross-sectional, descriptive study. Results: Mean values for the variables analyzed were calculated. For lumbar lordosis, 7-year-old boys showed 38.49 degrees +/- 15.32 degrees in comparison to all other groups (42.29 degrees +/- 7.13 degrees). For thoracic kyphosis, the 7-year-old children presented 28.07 degrees +/- 7.73 degrees. and the 8-year-olds 30.32 degrees +/- 7.73 degrees. Pelvic inclination presented a mean value of 15.82 degrees +/- 5.46 degrees and single lateral spine deviation mean value of 3.48 degrees +/- 2.12 degrees. Conclusion: For the sample studied, differences based on sex and age were found for some of the body segments analyzed. The values found in this study may contribute to improved physiotherapeutic treatment when associated with other aspects of the clinical assessment and symptomatology. (J Manipulative Physiol Ther 2009;32: 154-159)

Developing logic programs from specifications using stepwise refinement

In this paper we demonstrate a refinement calculus for logic programs, which is a framework for developing logic programs from specifications. The paper is written in a tutorial-style, using a running example to illustrate how the refinement calculus is used to develop logic programs. The paper also presents an overview of some of the advanced features of the calculus, including the introduction of higher-order procedures and the refinement of abstract data types.

Effect of image analysis software on neurofunctional activation during processing of emotional human faces

Functional brain imaging techniques such as functional MRI (fMRI) that allow the in vivo investigation of the human brain have been exponentially employed to address the neurophysiological substrates of emotional processing. Despite the growing number of fMRI studies in the field, when taken separately these individual imaging studies demonstrate contrasting findings and variable pictures, and are unable to definitively characterize the neural networks underlying each specific emotional condition. Different imaging packages, as well as the statistical approaches for image processing and analysis, probably have a detrimental role by increasing the heterogeneity of findings. In particular, it is unclear to what extent the observed neurofunctional response of the brain cortex during emotional processing depends on the fMRI package used in the analysis. In this pilot study, we performed a double analysis of an fMRI dataset using emotional faces. The Statistical Parametric Mapping (SPM) version 2.6 (Wellcome Department of Cognitive Neurology, London, UK) and the XBAM 3.4 (Brain Imaging Analysis Unit, Institute of Psychiatry, Kings College London, UK) programs, which use parametric and non-parametric analysis, respectively, were used to assess our results. Both packages revealed that processing of emotional faces was associated with an increased activation in the brain`s visual areas (occipital, fusiform and lingual gyri), in the cerebellum, in the parietal cortex, in the cingulate cortex (anterior and posterior cingulate), and in the dorsolateral and ventrolateral prefrontal cortex. However, blood oxygenation level-dependent (BOLD) response in the temporal regions, insula and putamen was evident in the XBAM analysis but not in the SPM analysis. Overall, SPM and XBAM analyses revealed comparable whole-group brain responses. Further Studies are needed to explore the between-group compatibility of the different imaging packages in other cognitive and emotional processing domains. (C) 2009 Elsevier Ltd. All rights reserved.