Family and group cognitive behavior therapy: Evaluation of treatment outcome and treatment specificity

This dissertation examined the efficacy of family cognitive behavior treatment (FCBT) and group cognitive behavior treatment (GBCT) for reducing anxiety disorders in children and adolescents using several approaches: clinical significant change, equivalence testing, and analyses of variance. It also examined treatment specificity in terms of targeting family/parents (in FCBT) and peers/group (in GCBT) contextual variables using two main approaches: analyses of variance and structural equation modeling (SEM). The sample consisted of 143 children and their parents who presented to the Child Anxiety and Phobia Program housed within the Child and Family Psychosocial Research Center at Florida International University. Diagnostic interviews and questionnaires were administered to assess youth anxiety. Questionnaires were administered to assess child and parent views of family/parents and peers/group contextual variables. In terms of clinical significant change, results indicated that 84.6% of youth in FCBT and 71.2% of youth in GBCT no longer met diagnostic criteria for their primary/targeted anxiety disorder. In addition, results from analyses of variance indicated that FCBT and GCBT were both efficacious in reducing anxiety disorders in youth across both child and parent ratings. Results using both analyses of variance and structural equation modeling also indicated that there was no meaningful treatment specificity between FCBT and GCBT in terms of either family/parents or peers/group contextual variables. That is, child social skills improved in GCBT in which these skills were targeted and in FCBT in which these skills were not targeted; parenting skills improved in FCBT in which these skills were targeted and in GCBT in which these skills were not targeted. Clinical implications and future research recommendations are discussed.

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.