Refinement methods for software architecture design using the software architecture model

Modern software systems are often large and complicated. To better understand, develop, and manage large software systems, researchers have studied software architectures that provide the top level overall structural design of software systems for the last decade. One major research focus on software architectures is formal architecture description languages, but most existing research focuses primarily on the descriptive capability and puts less emphasis on software architecture design methods and formal analysis techniques, which are necessary to develop correct software architecture design. ^ Refinement is a general approach of adding details to a software design. A formal refinement method can further ensure certain design properties. This dissertation proposes refinement methods, including a set of formal refinement patterns and complementary verification techniques, for software architecture design using Software Architecture Model (SAM), which was developed at Florida International University. First, a general guideline for software architecture design in SAM is proposed. Second, specification construction through property-preserving refinement patterns is discussed. The refinement patterns are categorized into connector refinement, component refinement and high-level Petri nets refinement. These three levels of refinement patterns are applicable to overall system interaction, architectural components, and underlying formal language, respectively. Third, verification after modeling as a complementary technique to specification refinement is discussed. Two formal verification tools, the Stanford Temporal Prover (STeP) and the Simple Promela Interpreter (SPIN), are adopted into SAM to develop the initial models. Fourth, formalization and refinement of security issues are studied. A method for security enforcement in SAM is proposed. The Role-Based Access Control model is formalized using predicate transition nets and Z notation. The patterns of enforcing access control and auditing are proposed. Finally, modeling and refining a life insurance system is used to demonstrate how to apply the refinement patterns for software architecture design using SAM and how to integrate the access control model. ^ The results of this dissertation demonstrate that a refinement method is an effective way to develop a high assurance system. The method developed in this dissertation extends existing work on modeling software architectures using SAM and makes SAM a more usable and valuable formal tool for software architecture design. ^

Quality of life and application of the transtheoretical model to diabetes self -management behaviors in older adults with type 2 diabetes

One in five adults 65 years and older has diabetes. Coping with diabetes is a lifelong task, and much of the responsibility for managing the disease falls upon the individual. Reports of non-adherence to recommended treatments are high. Understanding the additive impact of diabetes on quality of life issues is important. The purpose of this study was to investigate the quality of life and diabetes self-management behaviors in ethnically diverse older adults with type 2 diabetes. The SF-12v2 was used to measure physical and mental health quality of life. Scores were compared to general, age sub-groups, and diabetes-specific norms. The Transtheoretical Model (TTM) was applied to assess perceived versus actual behavior for three diabetes self-management tasks: dietary management, medication management, and blood glucose self-monitoring. Dietary intake and hemoglobin A1c values were measured as outcome variables. Utilizing a cross-sectional research design, participants were recruited from Elderly Nutrition Program congregate meal sites (n = 148, mean age 75). ^ Results showed that mean scores of the SF-12v2 were significantly lower in the study sample than the general norms for physical health (p < .001), mental health (p < .01), age sub-group norms (p < .05), and diabetes-specific norms for physical health (p < .001). A multiple regression analysis found that adherence to an exercise plan was significantly associated with better physical health (p < .001). Transtheoretical Model multiple regression analyses explained 68% of the variance for % Kcal from fat, 41% for fiber, 70% for % Kcal from carbohydrate, and 7% for hemoglobin A 1c values. Significant associations were found between TTM stage of change and dietary fiber intake (p < .01). Other significant associations related to diet included gender (p < .01), ethnicity (p < .05), employment (p < .05), type of insurance (p < .05), adherence to an exercise plan (p < .05), number of doctor visits/year ( p < .01), and physical health (p < .05). Significant associations were found between hemoglobin A1c values and age ( p < .05), being non-Hispanic Black (p < .01), income (p < .01), and eye problems (p < .05). ^ The study highlights the importance of the beneficial effects of exercise on quality of life issues. Furthermore, application of the Transtheoretical Model in conjunction with an assessment of dietary intake may be valuable in helping individuals make lifestyle changes. ^