The influence of neighbourhood formality status and socio-economic position on self-rated health among adult men and women: a multilevel, cross sectional, population study from Aleppo, Syria

Background There is substantial evidence from high income countries that neighbourhoods have an influence on health independent of individual characteristics. However, neighbourhood characteristics are rarely taken into account in the analysis of urban health studies from developing countries. Informal urban neighbourhoods are home to about half of the population in Aleppo, the second largest city in Syria (population>2.5 million). This study aimed to examine the influence of neighbourhood socioeconomic status (SES) and formality status on self-rated health (SRH) of adult men and women residing in formal and informal urban neighbourhoods in Aleppo. Methods The study used data from 2038 survey respondents to the Aleppo Household Survey, 2004 (age 18–65 years, 54.8% women, response rate 86%). Respondents were nested in 45 neighbourhoods. Five individual-level SES measures, namely education, employment, car ownership, item ownership and household density, were aggregated to the level of neighbourhood. Multilevel regression models were used to investigate associations. Results We did not find evidence of important SRH variation between neighbourhoods. Neighbourhood average of household item ownership was associated with a greater likelihood of reporting excellent SRH in women; odds ratio (OR) for an increase of one item on average was 2.3 (95% CI 1.3-4.4 (versus poor SRH)) and 1.7 (95% CI 1.1-2.5 (versus normal SRH)), adjusted for individual characteristics and neighbourhood formality. After controlling for individual and neighbourhood SES measures, women living in informal neighbourhoods were less likely to report poor SRH than women living in formal neighbourhoods (OR= 0.4; 95% CI (0.2- 0.8) (versus poor SRH) and OR=0.5; 95%; CI (0.3-0.9) (versus normal SRH). Conclusions Findings support evidence from high income countries that certain characteristic of neighbourhoods affect men and women in different ways. Further research from similar urban settings in developing countries is needed to understand the mechanisms by which informal neighbourhoods influence women’s health.

Formal verification and testing of software architectural models

Ensuring the correctness of software has been the major motivation in software research, constituting a Grand Challenge. Due to its impact in the final implementation, one critical aspect of software is its architectural design. By guaranteeing a correct architectural design, major and costly flaws can be caught early on in the development cycle. Software architecture design has received a lot of attention in the past years, with several methods, techniques and tools developed. However, there is still more to be done, such as providing adequate formal analysis of software architectures. On these regards, a framework to ensure system dependability from design to implementation has been developed at FIU (Florida International University). This framework is based on SAM (Software Architecture Model), an ADL (Architecture Description Language), that allows hierarchical compositions of components and connectors, defines an architectural modeling language for the behavior of components and connectors, and provides a specification language for the behavioral properties. The behavioral model of a SAM model is expressed in the form of Petri nets and the properties in first order linear temporal logic.^ This dissertation presents a formal verification and testing approach to guarantee the correctness of Software Architectures. The Software Architectures studied are expressed in SAM. For the formal verification approach, the technique applied was model checking and the model checker of choice was Spin. As part of the approach, a SAM model is formally translated to a model in the input language of Spin and verified for its correctness with respect to temporal properties. In terms of testing, a testing approach for SAM architectures was defined which includes the evaluation of test cases based on Petri net testing theory to be used in the testing process at the design level. Additionally, the information at the design level is used to derive test cases for the implementation level. Finally, a modeling and analysis tool (SAM tool) was implemented to help support the design and analysis of SAM models. The results show the applicability of the approach to testing and verification of SAM models with the aid of the SAM tool.^

Formal verification and testing of software architectural models

Ensuring the correctness of software has been the major motivation in software research, constituting a Grand Challenge. Due to its impact in the final implementation, one critical aspect of software is its architectural design. By guaranteeing a correct architectural design, major and costly flaws can be caught early on in the development cycle. Software architecture design has received a lot of attention in the past years, with several methods, techniques and tools developed. However, there is still more to be done, such as providing adequate formal analysis of software architectures. On these regards, a framework to ensure system dependability from design to implementation has been developed at FIU (Florida International University). This framework is based on SAM (Software Architecture Model), an ADL (Architecture Description Language), that allows hierarchical compositions of components and connectors, defines an architectural modeling language for the behavior of components and connectors, and provides a specification language for the behavioral properties. The behavioral model of a SAM model is expressed in the form of Petri nets and the properties in first order linear temporal logic. This dissertation presents a formal verification and testing approach to guarantee the correctness of Software Architectures. The Software Architectures studied are expressed in SAM. For the formal verification approach, the technique applied was model checking and the model checker of choice was Spin. As part of the approach, a SAM model is formally translated to a model in the input language of Spin and verified for its correctness with respect to temporal properties. In terms of testing, a testing approach for SAM architectures was defined which includes the evaluation of test cases based on Petri net testing theory to be used in the testing process at the design level. Additionally, the information at the design level is used to derive test cases for the implementation level. Finally, a modeling and analysis tool (SAM tool) was implemented to help support the design and analysis of SAM models. The results show the applicability of the approach to testing and verification of SAM models with the aid of the SAM tool.