Measurement of single spin asymmetry and fifth structure function for the p( e&ar; ,e'K +)Λ reaction with CEBAF Large Acceptance Spectrometer (CLAS)

The single spin asymmetry, ALT ′, and the polarized structure function, σ LT′, for the p( e&ar; , e′K +)Λ reaction in the resonance region have been measured and extracted using the CEBAF Large Acceptance Spectrometer (CLAS) at Jefferson Lab. Data were taken at an electron beam energy of 2.567 GeV. The large acceptance of CLAS allows for full azimuthal angle coverage over a large range of center-of-mass scattering angles. Results were obtained that span a range in Q 2 from 0.5 to 1.3 GeV2 and W from threshold up to 2.1 GeV and were compared to existing theoretical calculations. The polarized structure function is sensitive to the interferences between various resonant amplitudes, as well as to resonant and non-resonant amplitudes. This measurement is essential for understanding the structure of nucleons and searching for previously undetected nucleon excited states (resonances) predicted by quark models. The W dependence of the σ LT′ in the kinematic regions dominated by s and u channel exchange (cos qcmk = −0.50, −0.167, 0.167) indicated possible resonance structures not predicted by theoretical calculations. The σLT ′ behavior around W = 1.875 GeV could be the signature of a resonance predicted by the quark models and possibly seen in photoproduction. In the very forward angles where the reaction is dominated by the t-channel, the average σLT ′ was zero. There was no indication of the interference between resonances or resonant and non-resonant amplitudes. This might be indicating the dominance of a single t-channel exchange. Study of the sensitivity of the fifth structure function data to the resonance around 1900 MeV showed that these data were highly sensitive to the various assumptions of the models for the quantum number of this resonance. This project was part of a larger CLAS program to measure cross sections and polarization observables for kaon electroproduction in the nucleon resonance region. ^

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.