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. ^

A survey of music educator's understanding and use of advanced audio technology in their instructional methods and strategies

This study examines the correlation between how certified music educators understand audio technology and how they incorporate it in their instructional methods. Participants were classroom music teachers selected from fifty middle schools in Miami- Dade Public Schools. The study adopted a non-experimental research design in which a survey was the primary tool of investigation. The findings reveal that a majority of middle school music teachers in Miami-Dade are not familiar with advanced audiorecording software or any other digital device dedicated to the recording and processing of audio signals. Moreover, they report a lack of opportunities to develop this knowledge. Younger music teachers, however, are more open to developing up-to-date instructional methodologies. Most of the participants agreed that music instruction should be a platform for preparing students for a future in the entertainment industry. A basic knowledge of music business should be delivered to students enrolled in middle-school music courses.

Design, fabrication, and evaluation of on-chip micro-supercapacitors

Due to the increasing demand for high power and reliable miniaturized energy storage devices, the development of micro-supercapacitors or electrochemical micro-capacitors have attracted much attention in recent years. This dissertation investigates several strategies to develop on-chip micro-supercapacitors with high power and energy density. Micro-supercapacitors based on interdigitated carbon micro-electrode arrays are fabricated through carbon microelectromechanical systems (C-MEMS) technique which is based on carbonization of patterned photoresist. To improve the capacitive behavior, electrochemical activation is performed on carbon micro-electrode arrays. The developed micro-supercapacitors show specific capacitances as high as 75 mFcm-2 at a scan rate of 5 mVs -1 after electrochemical activation for 30 minutes. The capacitance loss is less than 13% after 1000 cyclic voltammetry (CV) cycles. These results indicate that electrochemically activated C-MEMS micro-electrode arrays are promising candidates for on-chip electrochemical micro-capacitor applications. The energy density of micro-supercapacitors was further improved by conformal coating of polypyrrole (PPy) on C-MEMS structures. In these types of micro-devices the three dimensional (3D) carbon microstructures serve as current collectors for high energy density PPy electrodes. The electrochemical characterizations of these micro-supercapacitors show that they can deliver a specific capacitance of about 162.07 mFcm-2 and a specific power of 1.62mWcm -2 at a 20 mVs-1 scan rate. Addressing the need for high power micro-supercapacitors, the application of graphene as electrode materials for micro-supercapacitor was also investigated. The present study suggests a novel method to fabricate graphene-based micro-supercapacitors with thin film or in-plane interdigital electrodes. The fabricated micro-supercapacitors show exceptional frequency response and power handling performance and could effectively charge and discharge at rates as high as 50 Vs-1. CV measurements show that the specific capacitance of the micro-supercapacitor based on reduced graphene oxide and carbon nanotube composites is 6.1 mFcm -2 at scan rate of 0.01Vs-1. At a very high scan rate of 50 Vs-1, a specific capacitance of 2.8 mFcm-2 (stack capacitance of 3.1 Fcm-3) is recorded. This unprecedented performance can potentially broaden the future applications of micro-supercapacitors.

Adult Learners and AIDS Artwork: Suggestions for Adult Education Practice

The purpose of this paper is to explore the ways in which the creative and purposeful use of AIDS Artwork as an educational tool may reduce stigma about HIV/AIDS and help adult learners to regulate their own prejudices about the diseases.

The design, implementation and production process of creating a viable series of Latin shows in Hollywood, Florida

The purpose of this research was to design and implement a Series of Latin Shows to be featured at the Satine Restaurant located in The Diplomat Hotel in Hollywood, Florida. Three shows were created: "Electro Tango," "Bossa Nova Jazz," and "Piel Canela Night" to help generate interest for not only the Satine Restaurant but also for the surrounding area. The artistic concept included big bands, costumes, dancers and a DJ. A production book was created and included the most important aspects of the individual shows such as budgets, costumes, and ground plans, to assure the success of each event. Careful analysis was done for the demographic area and a marketing plan was designed and implemented. The research and practical application of similar shows in the industry determined that the production of these particular shows, although costly, have a qualifiable chance to succeed in this venue.

ASIC microcontroller design of a radiation monitoring system using VHDL modeling and FPGA implementation

Three new technologies have been brought together to develop a miniaturized radiation monitoring system. The research involved (1) Investigation a new HgI$\sb2$ detector. (2) VHDL modeling. (3) FPGA implementation. (4) In-circuit Verification. The packages used included an EG&G's crystal(HgI$\sb2$) manufactured at zero gravity, the Viewlogic's VHDL and Synthesis, Xilinx's technology library, its FPGA implementation tool, and a high density device (XC4003A). The results show: (1) Reduced cycle-time between Design and Hardware implementation; (2) Unlimited Re-design and implementation using the static RAM technology; (3) Customer based design, verification, and system construction; (4) Well suited for intelligent systems. These advantages excelled conventional chip design technologies and methods in easiness, short cycle time, and price in medium sized VLSI applications. It is also expected that the density of these devices will improve radically in the near future. ^

Methods for modeling and analyzing concurrent software

Concurrent software executes multiple threads or processes to achieve high performance. However, concurrency results in a huge number of different system behaviors that are difficult to test and verify. The aim of this dissertation is to develop new methods and tools for modeling and analyzing concurrent software systems at design and code levels. This dissertation consists of several related results. First, a formal model of Mondex, an electronic purse system, is built using Petri nets from user requirements, which is formally verified using model checking. Second, Petri nets models are automatically mined from the event traces generated from scientific workflows. Third, partial order models are automatically extracted from some instrumented concurrent program execution, and potential atomicity violation bugs are automatically verified based on the partial order models using model checking. Our formal specification and verification of Mondex have contributed to the world wide effort in developing a verified software repository. Our method to mine Petri net models automatically from provenance offers a new approach to build scientific workflows. Our dynamic prediction tool, named McPatom, can predict several known bugs in real world systems including one that evades several other existing tools. McPatom is efficient and scalable as it takes advantage of the nature of atomicity violations and considers only a pair of threads and accesses to a single shared variable at one time. However, predictive tools need to consider the tradeoffs between precision and coverage. Based on McPatom, this dissertation presents two methods for improving the coverage and precision of atomicity violation predictions: 1) a post-prediction analysis method to increase coverage while ensuring precision; 2) a follow-up replaying method to further increase coverage. Both methods are implemented in a completely automatic tool.

Methods for Modeling and Analyzing Concurrent Software

Concurrent software executes multiple threads or processes to achieve high performance. However, concurrency results in a huge number of different system behaviors that are difficult to test and verify. The aim of this dissertation is to develop new methods and tools for modeling and analyzing concurrent software systems at design and code levels. This dissertation consists of several related results. First, a formal model of Mondex, an electronic purse system, is built using Petri nets from user requirements, which is formally verified using model checking. Second, Petri nets models are automatically mined from the event traces generated from scientific workflows. Third, partial order models are automatically extracted from some instrumented concurrent program execution, and potential atomicity violation bugs are automatically verified based on the partial order models using model checking. Our formal specification and verification of Mondex have contributed to the world wide effort in developing a verified software repository. Our method to mine Petri net models automatically from provenance offers a new approach to build scientific workflows. Our dynamic prediction tool, named McPatom, can predict several known bugs in real world systems including one that evades several other existing tools. McPatom is efficient and scalable as it takes advantage of the nature of atomicity violations and considers only a pair of threads and accesses to a single shared variable at one time. However, predictive tools need to consider the tradeoffs between precision and coverage. Based on McPatom, this dissertation presents two methods for improving the coverage and precision of atomicity violation predictions: 1) a post-prediction analysis method to increase coverage while ensuring precision; 2) a follow-up replaying method to further increase coverage. Both methods are implemented in a completely automatic tool.