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.

Dynamic modeling and analysis of single-stage boost inverters under normal and abnormal conditions

Inverters play key roles in connecting sustainable energy (SE) sources to the local loads and the ac grid. Although there has been a rapid expansion in the use of renewable sources in recent years, fundamental research, on the design of inverters that are specialized for use in these systems, is still needed. Recent advances in power electronics have led to proposing new topologies and switching patterns for single-stage power conversion, which are appropriate for SE sources and energy storage devices. The current source inverter (CSI) topology, along with a newly proposed switching pattern, is capable of converting the low dc voltage to the line ac in only one stage. Simple implementation and high reliability, together with the potential advantages of higher efficiency and lower cost, turns the so-called, single-stage boost inverter (SSBI), into a viable competitor to the existing SE-based power conversion technologies.^ The dynamic model is one of the most essential requirements for performance analysis and control design of any engineering system. Thus, in order to have satisfactory operation, it is necessary to derive a dynamic model for the SSBI system. However, because of the switching behavior and nonlinear elements involved, analysis of the SSBI is a complicated task.^ This research applies the state-space averaging technique to the SSBI to develop the state-space-averaged model of the SSBI under stand-alone and grid-connected modes of operation. Then, a small-signal model is derived by means of the perturbation and linearization method. An experimental hardware set-up, including a laboratory-scaled prototype SSBI, is built and the validity of the obtained models is verified through simulation and experiments. Finally, an eigenvalue sensitivity analysis is performed to investigate the stability and dynamic behavior of the SSBI system over a typical range of operation. ^

Docking and simulation study of the enantiospecificity of chiral epoxidation reactions catalyzed by chloroperoxidase

Chloroperoxidase (CPO), a 298-residue glycosylated protein from the fungus Caldariomyces fumago, is probably the most versatile heme enzyme yet discovered. Interest in CPO as a catalyst is based on its power to produce enantiomerically enriched products. Recent research has focused its attention on the ability of CPO to epoxidize alkenes in high regioselectivity and enantioselectivity as an efficient and environmentally benign alternative to traditional synthetic routes. There has been little work on the nature of ligand binding, which probably controls the regio- and enantiospecifity of CPO. Consequently it is here that we focus our work. We report docking calculations and computer simulations aimed at predicting the enantiospecificity of CPO-catalyzed epoxidation of three model substrates. On the basis of this work candidate mutations to improve the efficiency of CPO are predicted. In order to accomplish these aims, a simulated annealing and molecular dynamics protocol is developed to sample potentially reactive substrate/CPO complexes.

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

A methodology for formally modeling and analyzing software architecture of mobile agent systems

A methodology for formally modeling and analyzing software architecture of mobile agent systems provides a solid basis to develop high quality mobile agent systems, and the methodology is helpful to study other distributed and concurrent systems as well. However, it is a challenge to provide the methodology because of the agent mobility in mobile agent systems.^ The methodology was defined from two essential parts of software architecture: a formalism to define the architectural models and an analysis method to formally verify system properties. The formalism is two-layer Predicate/Transition (PrT) nets extended with dynamic channels, and the analysis method is a hierarchical approach to verify models on different levels. The two-layer modeling formalism smoothly transforms physical models of mobile agent systems into their architectural models. Dynamic channels facilitate the synchronous communication between nets, and they naturally capture the dynamic architecture configuration and agent mobility of mobile agent systems. Component properties are verified based on transformed individual components, system properties are checked in a simplified system model, and interaction properties are analyzed on models composing from involved nets. Based on the formalism and the analysis method, this researcher formally modeled and analyzed a software architecture of mobile agent systems, and designed an architectural model of a medical information processing system based on mobile agents. The model checking tool SPIN was used to verify system properties such as reachability, concurrency and safety of the medical information processing system. ^ From successful modeling and analyzing the software architecture of mobile agent systems, the conclusion is that PrT nets extended with channels are a powerful tool to model mobile agent systems, and the hierarchical analysis method provides a rigorous foundation for the modeling tool. The hierarchical analysis method not only reduces the complexity of the analysis, but also expands the application scope of model checking techniques. The results of formally modeling and analyzing the software architecture of the medical information processing system show that model checking is an effective and an efficient way to verify software architecture. Moreover, this system shows a high level of flexibility, efficiency and low cost of mobile agent technologies. ^

Organic matter dynamics in the Florida coastal Everglades: A molecular marker and isotopic approach

Everglades National Park (ENP) is about to undergo the world's largest wetland restoration with the aim of improving the quality, timing and distribution of water flow. The changes in water flow are hypothesized to alter the nutrient fluxes and organic matter (OM) dynamics within ENP, especially in the estuarine areas. This study used a multi-proxy approach of molecular markers and stable δ 13C isotope measurements, to determine the present day OM dynamics in ENP. ^ OM dynamics in wetland soils/sediments have proved to be difficult to understand using traditional geochemical approaches. These are often inadequate to describe the multitude of OM sources (e.g. higher land plant, emergent vegetation, submerged vegetation) to the soils/sediments and the complex diagenetic processes that can alter the OM characteristics. A multi-proxy approach, however, that incorporates both molecular level and bulk parameter information is ideal to comprehend complex OM dynamics in aquatic environments. Therefore, biomass-specific molecular markers or proxies can be useful in tracing the sources and processing of OM. This approach was used to examine the OM dynamics in the two major drainage basins, Shark River Slough and Taylor River Slough, of ENP. Freshwater to marine transects were sampled in both systems for soils/sediments and suspended particulate organic matter (SPOM) to be characterized through bulk OM analyses, lipid biomarker determinations (e.g. sterols, fatty acids, hydrocarbons and triterpenoids) and compound-specific stable carbon isotope (δ 13C) determinations. ^ One key accomplishment of the research was the assessment of a molecular marker proxy (Paq) to distinguish between emergent/higher plant vegetation from submerged vegetation within ENP. This proxy proved to be quite useful at tracing OM inputs to the soils/sediments of ENP. A second key accomplishment was the development of a 3-way model using vegetation specific molecular markers. This novel, descriptive model was successfully applied to the estuarine areas of Taylor and Shark River sloughs, providing clear evidence of mixing of freshwater, estuarine and marine derived OM in these areas. In addition, diagenetic transformations of OM in these estuaries were found to be quite different between Taylor and Shark Rivers, and are likely a result of OM quality and hydrological differences. ^

Molecular markers and human history: A tale of two haplogroup systems

To chronicle demographic movement across African Asian corridors, a variety of molecular (sequence analysis, restriction mapping and denaturing high performance liquid chromatography etc.) and statistical (correspondence analysis, AMOVA, calculation of diversity indices and phylogenetic inference, etc.) techniques were employed to assess the phylogeographic patterns of mtDNA control region and Y chromosomal variation among 14 sub-Saharan, North African and Middle Eastern populations. The patterns of genetic diversity revealed evidence of multiple migrations across several African Asian passageways as well within the African continent itself. The two-part analysis uncovered several interesting results which include the following: (1) a north (Egypt and Middle East Asia) to south (sub-Saharan Africa) partitioning of both mtDNA and Y chromosomal haplogroup diversity, (2) a genetic diversity gradient in sub-Saharan Africa from east to west, (3) evidence in favor of the Levantine Corridor over the Horn of Africa as the major genetic conduit since the Last Glacial Maximum, (4) a substantially higher mtDNA versus Y chromosomal sub-Saharan component in the Middle East collections, (5) a higher representation of East versus West African mtDNA haplotypes in the Arabian Peninsula populations versus no such bias in the Levant groups and lastly, (6) genetic remnants of the Bantu demographic expansion in sub-Saharan Africa. ^

The construction and optimization of an ion mobility spectrometer for the analysis of explosives and drugs

Today, over 15,000 Ion Mobility Spectrometry (IMS) analyzers are employed at worldwide security checkpoints to detect explosives and illicit drugs. Current portal IMS instruments and other electronic nose technologies detect explosives and drugs by analyzing samples containing the headspace air and loose particles residing on a surface. Canines can outperform these systems at sampling and detecting the low vapor pressure explosives and drugs, such as RDX, PETN, cocaine, and MDMA, because these biological detectors target the volatile signature compounds available in the headspace rather than the non-volatile parent compounds of explosives and drugs.^ In this dissertation research volatile signature compounds available in the headspace over explosive and drug samples were detected using SPME as a headspace sampling tool coupled to an IMS analyzer. A Genetic Algorithm (GA) technique was developed to optimize the operating conditions of a commercial IMS (GE Itemizer 2), leading to the successful detection of plastic explosives (Detasheet, Semtex H, and C-4) and illicit drugs (cocaine, MDMA, and marijuana). Short sampling times (between 10 sec to 5 min) were adequate to extract and preconcentrate sufficient analytes (> 20 ng) representing the volatile signatures in the headspace of a 15 mL glass vial or a quart-sized can containing ≤ 1 g of the bulk explosive or drug.^ Furthermore, a research grade IMS with flexibility for changing operating conditions and physical configurations was designed and fabricated to accommodate future research into different analytes or physical configurations. The design and construction of the FIU-IMS were facilitated by computer modeling and simulation of ion’s behavior within an IMS. The simulation method developed uses SIMION/SDS and was evaluated with experimental data collected using a commercial IMS (PCP Phemto Chem 110). The FIU-IMS instrument has comparable performance to the GE Itemizer 2 (average resolving power of 14, resolution of 3 between two drugs and two explosives, and LODs range from 0.7 to 9 ng). ^ The results from this dissertation further advance the concept of targeting volatile components to presumptively detect the presence of concealed bulk explosives and drugs by SPME-IMS, and the new FIU-IMS provides a flexible platform for future IMS research projects.^

A nested Petri net framework for modeling and analyzing multi-agent systems

In the past two decades, multi-agent systems (MAS) have emerged as a new paradigm for conceptualizing large and complex distributed software systems. A multi-agent system view provides a natural abstraction for both the structure and the behavior of modern-day software systems. Although there were many conceptual frameworks for using multi-agent systems, there was no well established and widely accepted method for modeling multi-agent systems. This dissertation research addressed the representation and analysis of multi-agent systems based on model-oriented formal methods. The objective was to provide a systematic approach for studying MAS at an early stage of system development to ensure the quality of design. ^ Given that there was no well-defined formal model directly supporting agent-oriented modeling, this study was centered on three main topics: (1) adapting a well-known formal model, predicate transition nets (PrT nets), to support MAS modeling; (2) formulating a modeling methodology to ease the construction of formal MAS models; and (3) developing a technique to support machine analysis of formal MAS models using model checking technology. PrT nets were extended to include the notions of dynamic structure, agent communication and coordination to support agent-oriented modeling. An aspect-oriented technique was developed to address the modularity of agent models and compositionality of incremental analysis. A set of translation rules were defined to systematically translate formal MAS models to concrete models that can be verified through the model checker SPIN (Simple Promela Interpreter). ^ This dissertation presents the framework developed for modeling and analyzing MAS, including a well-defined process model based on nested PrT nets, and a comprehensive methodology to guide the construction and analysis of formal MAS models.^

Integrated Ecological Modeling and Decision Analysis Within the Everglades Landscape

Planning for complex ecosystem restoration projects involves integrating ecological modeling with analysis of performance trade-offs among restoration alternatives. The authors used the Everglades Landscape Model and Multi-Criteria Decision Analysis to explore the effect of simulated ecosystem performance, risk preferences, and criteria weights on the ranking of three alternatives to restoring overland sheet flow in the Everglades. The ecological model outputs included both hydrologic and water quality criteria. Results were scored in the decision analysis framework, highlighting the trade-offs between hydrologic restoration and water quality constraints. Given equal weighting of performance measures, the alternative with more homogenous sheet flow was preferred over other alternatives, despite evidence of some localized eutrophication risk.

Sediment and soil organic matter source assessment as revealed by the molecular distribution and carbon isotopic composition of n-alkanes

The assessment of organic matter (OM) sources in sediments and soils is a key to better understand the biogeochemical cycling of carbon in aquatic environments. While traditional molecular marker-based methods have provided such information for typical two end member (allochthonous/terrestrial vs. autochthonous/microbial)-dominated systems, more detailed, biomass-specific assessments are needed for ecosystems with complex OM inputs such as tropical and sub-tropical wetlands and estuaries where aquatic macrophytes and macroalgae may play an important role as OM sources. The aim of this study was to assess the utility of a combined approach using compound specific stable carbon isotope analysis and an n-alkane based proxy (Paq) to differentiate submerged and emergent/terrestrial vegetation OM inputs to soils/sediments from a sub-tropical wetland and estuarine system, the Florida Coastal Everglades. Results show that Paq values (0.13–0.51) for the emergent/terrestrial plants were generally lower than those for freshwater/marine submerged vegetation (0.45–1.00) and that compound specific δ13C values for the n-alkanes (C23 to C31) were distinctively different for terrestrial/emergent and freshwater/marine submerged plants. While crossplots of the Paq and n-alkane stable isotope values for the C23n-alkane suggest that OM inputs are controlled by vegetation changes along the freshwater to marine transect, further resolution regarding OM input changes along this landscape was obtained through principal component analysis (PCA), successfully grouping the study sites according to the OM source strengths. The data show the potential for this n-alkane based multi-proxy approach as a means of assessing OM inputs to complex ecosystems.

Tool cutting force modeling and wear estimation of micro -end-milling operations

The applications of micro-end-milling operations have increased recently. A Micro-End-Milling Operation Guide and Research Tool (MOGART) package has been developed for the study and monitoring of micro-end-milling operations. It includes an analytical cutting force model, neural network based data mapping and forecasting processes, and genetic algorithms based optimization routines. MOGART uses neural networks to estimate tool machinability and forecast tool wear from the experimental cutting force data, and genetic algorithms with the analytical model to monitor tool wear, breakage, run-out, cutting conditions from the cutting force profiles. ^ The performance of MOGART has been tested on the experimental data of over 800 experimental cases and very good agreement has been observed between the theoretical and experimental results. The MOGART package has been applied to the micro-end-milling operation study of Engineering Prototype Center of Radio Technology Division of Motorola Inc. ^

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.