Formal modeling and analysis techniques for high level Petri nets

Petri Nets are a formal, graphical and executable modeling technique for the specification and analysis of concurrent and distributed systems and have been widely applied in computer science and many other engineering disciplines. Low level Petri nets are simple and useful for modeling control flows but not powerful enough to define data and system functionality. High level Petri nets (HLPNs) have been developed to support data and functionality definitions, such as using complex structured data as tokens and algebraic expressions as transition formulas. Compared to low level Petri nets, HLPNs result in compact system models that are easier to be understood. Therefore, HLPNs are more useful in modeling complex systems. ^ There are two issues in using HLPNs—modeling and analysis. Modeling concerns the abstracting and representing the systems under consideration using HLPNs, and analysis deals with effective ways study the behaviors and properties of the resulting HLPN models. In this dissertation, several modeling and analysis techniques for HLPNs are studied, which are integrated into a framework that is supported by a tool. ^ For modeling, this framework integrates two formal languages: a type of HLPNs called Predicate Transition Net (PrT Net) is used to model a system's behavior and a first-order linear time temporal logic (FOLTL) to specify the system's properties. The main contribution of this dissertation with regard to modeling is to develop a software tool to support the formal modeling capabilities in this framework. ^ For analysis, this framework combines three complementary techniques, simulation, explicit state model checking and bounded model checking (BMC). Simulation is a straightforward and speedy method, but only covers some execution paths in a HLPN model. Explicit state model checking covers all the execution paths but suffers from the state explosion problem. BMC is a tradeoff as it provides a certain level of coverage while more efficient than explicit state model checking. The main contribution of this dissertation with regard to analysis is adapting BMC to analyze HLPN models and integrating the three complementary analysis techniques in a software tool to support the formal analysis capabilities in this framework. ^ The SAMTools developed for this framework in this dissertation integrates three tools: PIPE+ for HLPNs behavioral modeling and simulation, SAMAT for hierarchical structural modeling and property specification, and PIPE+Verifier for behavioral verification.^

Formal Modeling and Analysis Techniques for High Level Petri Nets

Petri Nets are a formal, graphical and executable modeling technique for the specification and analysis of concurrent and distributed systems and have been widely applied in computer science and many other engineering disciplines. Low level Petri nets are simple and useful for modeling control flows but not powerful enough to define data and system functionality. High level Petri nets (HLPNs) have been developed to support data and functionality definitions, such as using complex structured data as tokens and algebraic expressions as transition formulas. Compared to low level Petri nets, HLPNs result in compact system models that are easier to be understood. Therefore, HLPNs are more useful in modeling complex systems. There are two issues in using HLPNs - modeling and analysis. Modeling concerns the abstracting and representing the systems under consideration using HLPNs, and analysis deals with effective ways study the behaviors and properties of the resulting HLPN models. In this dissertation, several modeling and analysis techniques for HLPNs are studied, which are integrated into a framework that is supported by a tool. For modeling, this framework integrates two formal languages: a type of HLPNs called Predicate Transition Net (PrT Net) is used to model a system's behavior and a first-order linear time temporal logic (FOLTL) to specify the system's properties. The main contribution of this dissertation with regard to modeling is to develop a software tool to support the formal modeling capabilities in this framework. For analysis, this framework combines three complementary techniques, simulation, explicit state model checking and bounded model checking (BMC). Simulation is a straightforward and speedy method, but only covers some execution paths in a HLPN model. Explicit state model checking covers all the execution paths but suffers from the state explosion problem. BMC is a tradeoff as it provides a certain level of coverage while more efficient than explicit state model checking. The main contribution of this dissertation with regard to analysis is adapting BMC to analyze HLPN models and integrating the three complementary analysis techniques in a software tool to support the formal analysis capabilities in this framework. The SAMTools developed for this framework in this dissertation integrates three tools: PIPE+ for HLPNs behavioral modeling and simulation, SAMAT for hierarchical structural modeling and property specification, and PIPE+Verifier for behavioral verification.

Using structural equation modeling to assess two theoretical models that explain dropout

This study evaluated the relative fit of both Finn's (1989) Participation-Identification and Wehlage, Rutter, Smith, Lesko and Fernandez's (1989) School Membership models of high school completion to a sample of 4,597 eighth graders taken from the National Educational Longitudinal Study of 1988, (NELS:88), utilizing structural equation modeling techniques. This study found support for the importance of educational engagement as a factor in understanding academic achievement. The Participation-Identification model was particularly well fitting when applied to the sample of high school completers, dropouts (both overall and White dropouts) and African-American students. This study also confirmed the contribution of school environmental factors (i.e., size, diversity of economic and ethnic status among students) and family resources (i.e., availability of learning resources in the home and parent educational level) to students' educational engagement. Based on these findings, school social workers will need to be more attentive to utilizing macro-level interventions (i.e., community organization, interagency coordination) to achieve the organizational restructuring needed to address future challenges. The support found for the Participation-Identification model supports a shift in school social workers' attention from reactive attempts to improve the affective-interpersonal lives of students to proactive attention to their academic lives. The model concentrates school social work practices on the central mission of schools, which is educational engagement. School social workers guided by this model would be encouraged to seek changes in school policies and organization that would facilitate educational engagement. ^

Use of structural equation modeling to examine the association between breast cancer risk perception and repeat screening mammography among United States women

Breast cancer is the second leading cause of cancer death in United States women, estimated to be diagnosed in 1 out of 8 women in their lifetime. Screening mammography detects breast cancer in its pre-clinical stages when treatment strategies have the greatest chance of success, and is currently the only population-wide prevention method proven to reduce the morbidity and mortality associated with breast cancer. Research has shown that the majority of women are not screened annually, with estimates ranging front 6% - 30% of eligible women receiving all available annual mammograms over a 5-year or greater time frame. Health behavior theorists believe that perception of risk/susceptibility to a disease influences preventive health behavior, in this case, screening mammography The purpose of this dissertation is to examine the association between breast cancer risk perception and repeat screening mammography using a structural equation modeling (SEM) framework. A series of SEM multivariate regressions were conducted using self-reported, nationally representative data from the 2005 National Health Interview Survey. Interaction contrasts were tested to measure the potential moderating effects of variables which have been shown to be predictive of mammography use (physician recommendation, economic barriers, structural barriers, race/ethnicity) on the association between breast cancer risk perception and repeat mammography, while controlling for the covariates of age, income, region, nativity, and educational level. Of the variables tested for moderation, results of the SEM analyses identify physician recommendation as the only moderator of the relationship between risk perception and repeat mammography, thus the potentially most effective point of intervention to increase mammography screening, and decrease the morbidity and mortality associated with breast cancer. These findings expand the role of the physician from recommendation to one of attenuating the effect of risk perception and increasing repeat screening. The long range application of the research is the use of the SEM methodology to identify specific points of intervention most likely to increase preventive behavior in population-wide research, allowing for the most effective use of intervention funds.^

Simulating everglades national park hydrology and phosphorus transport under existing and future scenarios using numerical modeling

The Florida Everglades has a long history of anthropogenic changes which have impacted the quantity and quality of water entering the system. Since the construction of Tamiami Trail in the 1920's, overland flow to the Florida Everglades has decreased significantly, impacting ecosystems from the wetlands to the estuary. The MIKE Marsh Model of Everglades National Park (M3ENP) is a numerical model, which simulates Everglades National Park (ENP) hydrology using MIKE SHE/MIKE 11software. This model has been developed to determine the parameters that effect Everglades hydrology and understand the impact of specific flow changes on the hydrology of the system. ^ As part of the effort to return flows to the historical levels, several changes to the existing water management infrastructure have been implemented or are in the design phase. Bridge construction scenarios were programed into the M3ENP model to review the effect of these structural changes and evaluate the potential impacts on water levels and hydroperiods in the receiving Northeast Shark Slough ecosystem. These scenarios have shown critical water level increases in an area which has been in decline due to low water levels. Results from this work may help guide future decisions for restoration designs. ^ Excess phosphorus entering Everglades National Park in South Florida may promote the growth of more phosphorus-opportunistic species and alter the food chain from the bottom up. Two phosphorus transport methods were developed into the M3ENP hydrodynamic model to determine the factors affecting phosphorus transport and the impact of bridge construction on water quality. Results showed that while phosphorus concentrations in surface waters decreased overall, some areas within ENP interior may experience an increase in phosphorus loading which the addition of bridges to Tamiami Trail. Finally, phosphorus data and modeled water level data was used to evaluate the spectral response of Everglades vegetation to increasing phosphorus availability using Landsat imagery.^

Modeling of a Heat-Induced Buckling of Plates Using the Mesh-free Method

In the process of engineering design of structural shapes, the flat plate analysis results can be generalized to predict behaviors of complete structural shapes. In this case, the purpose of this project is to analyze a thin flat plate under conductive heat transfer and to simulate the temperature distribution, thermal stresses, total displacements, and buckling deformations. The current approach in these cases has been using the Finite Element Method (FEM), whose basis is the construction of a conforming mesh. In contrast, this project uses the mesh-free Scan Solve Method. This method eliminates the meshing limitation using a non-conforming mesh. I implemented this modeling process developing numerical algorithms and software tools to model thermally induced buckling. In addition, convergence analysis was achieved, and the results were compared with FEM. In conclusion, the results demonstrate that the method gives similar solutions to FEM in quality, but it is computationally less time consuming.

Simulating Everglades National Park hydrology and phosphorus transport under existing and future scenarios using numerical modeling

The Florida Everglades has a long history of anthropogenic changes which have impacted the quantity and quality of water entering the system. Since the construction of Tamiami Trail in the 1920's, overland flow to the Florida Everglades has decreased significantly, impacting ecosystems from the wetlands to the estuary. The MIKE Marsh Model of Everglades National Park (M3ENP) is a numerical model, which simulates Everglades National Park (ENP) hydrology using MIKE SHE/MIKE 11software. This model has been developed to determine the parameters that effect Everglades hydrology and understand the impact of specific flow changes on the hydrology of the system. As part of the effort to return flows to the historical levels, several changes to the existing water management infrastructure have been implemented or are in the design phase. Bridge construction scenarios were programed into the M3ENP model to review the effect of these structural changes and evaluate the potential impacts on water levels and hydroperiods in the receiving Northeast Shark Slough ecosystem. These scenarios have shown critical water level increases in an area which has been in decline due to low water levels. Results from this work may help guide future decisions for restoration designs. Excess phosphorus entering Everglades National Park in South Florida may promote the growth of more phosphorus-opportunistic species and alter the food chain from the bottom up. Two phosphorus transport methods were developed into the M3ENP hydrodynamic model to determine the factors affecting phosphorus transport and the impact of bridge construction on water quality. Results showed that while phosphorus concentrations in surface waters decreased overall, some areas within ENP interior may experience an increase in phosphorus loading which the addition of bridges to Tamiami Trail. Finally, phosphorus data and modeled water level data was used to evaluate the spectral response of Everglades vegetation to increasing phosphorus availability using Landsat imagery.

Structural Health Monitoring Inside Concrete and Grout Using the Wireless Identification and Sensing Platform (WISP)

This research investigates the implementation of battery-less RFID sensing platforms inside lossy media, such as, concrete and grout. Both concrete and novel grouts can be used for nuclear plant decommissioning as part of the U.S. Department of Energy’s (DOE’s) cleanup projects. Our research examines the following: (1) material characterization, (2) analytical modeling of transmission and propagation losses inside lossy media, (3) maximum operational range of RFID wireless sensors embedded inside concrete and grout, and (4) best positioning of antennas for achieving longer communication range between RFID antennas and wireless sensors. Our research uses the battery-less Wireless Identification and Sensing Platform (WISP) which can be used to monitor temperature, and humidity inside complex materials. By using a commercial Agilent open-ended coaxial probe (HP8570B), the measurements of the dielectric permittivity of concrete and grout are performed. Subsequently, the measured complex permittivity is used to formulate analytical Debye models. Also, the transmission and propagation losses of a uniform plane wave inside grout are calculated. Our results show that wireless sensors will perform better in concrete than grout. In addition, the maximum axial and radial ranges for WISP are experimentally determined. Our work illustrates the feasibility of battery-less wireless sensors that are embedded inside concrete and grout. Also, our work provides information that can be used to optimize the power management, sampling rate, and antenna design of such sensors.