The Unified Modeling Language (UML) is a standard language adopted by the Object Management Group (OMG) for writing object-oriented (OO) descriptions of software systems. UML allows the analyst to add class-level and system-level constraints. However, UML does not describe how to check the correctness of these constraints. Recent studies have shown that Symbolic Model Checking can effectively verify large software specifications. In this thesis, we investigate how to use model checking to verify constraints of UML specifications. We describe the process of specifying, translating and verifying UML specifications for an elevator example. We use the Cadence Symbolic Model Verifier (SMV) to verify the system properties. We demonstrate how to write a UML specification that can be easily translated to SMV. We propose a set of rules and guidelines to translate UML specifications to SMV, and then use these to translate a non-trivial UML elevator specification to SMV. We look at errors detected throughout the specification, translation and verification process, to see how well they reveal errors, ambiguities and omissions in the user requirements.

The Unified Modeling Language (UML) is a standard language adopted by the Object Management Group (OMG) for writing object-oriented (OO) descriptions of software systems. UML allows the analyst to add class-level and system-level constraints. However, UML does not describe how to check the correctness of these constraints. Recent studies have shown that Symbolic Model Checking can effectively verify large software specifications. In this thesis, we investigate how to use model checking to verify constraints of UML specifications. We describe the process of specifying, translating and verifying UML specifications for an elevator example. We use the Cadence Symbolic Model Verifier (SMV) to verify the system properties. We demonstrate how to write a UML specification that can be easily translated to SMV. We propose a set of rules and guidelines to translate UML specifications to SMV, and then use these to translate a non-trivial UML elevator specification to SMV. We look at errors detected throughout the specification, translation and verification process, to see how well they reveal errors, ambiguities and omissions in the user requirements.

Soybean mosaic virus (SMV; Genus Potyvirus; Family Potyviridae) is one of the most widespread viruses in soybean (Glycine max [L.] Merr.). Hutcheson, a cultivar developed in Virginia, is resistant to the common strains of SMV. However, new resistance-breaking (RB) isolates of SMV have emerged in natural infections to break the resistance of Hutcheson containing the Rsv1y allele. These RB isolates are SMV-G5 and G6-like based on the differential reactions on soybean cultivars with the Rsv1 locus, and are more G6-like based on the amino acid sequence of the coat protein (CP). The CP of the RB isolates is diverse at the amino and carboxy termini and highly conserved in the core region. RB isolates reduce the yield of susceptible cultivars and cause mottling of the seed coat. Dual infection of soybeans with SMV and BPMV increased the severity of symptoms, including plant stunting and SMV titer in comparison to single SMV inoculations. The reactions of Hutcheson and herbicide-tolerant Hutcheson RR were similar with or without herbicide application. Resistance to SMV is controlled by single dominant genes at three distinct loci, Rsv1, Rsv3 and Rsv4. The mechanisms of resistance at the Rsv3 and Rsv4 loci were investigated by tracking virus accumulation and movement over time using leaf immunoprints. The mechanisms of Rsv3 resistance include extreme resistance, hypersensitive response, or restriction to virus replication and movement, which are strain specific. The Rsv4 gene was found to function in a non-strain specific and non-necrotic manner. The mechanisms of Rsv4 resistance involve restricting both cell-to-cell and long distance movement of SMV. The Rsv1, Rsv3 and Rsv4 resistance genes exhibit a continuum of SMV-soybean interactions, and include complete susceptibility, local and systemic necrosis, restriction of virus movement (both cell-to-cell and long distance), reduction in virus accumulation, and extreme resistance with no detectable virus. Cultivars containing two genes for resistance, Rsv1 and Rsv3 or Rsv1 and Rsv4, were resistant to multiple strains of SMV tested and show great potential for gene pyramiding efforts to ensure a wider and more durable resistance to SMV in soybeans. / Ph. D.

Soybean mosaic virus (SMV) is the major virus disease reported all over the world in soybean crop. This disease causes reduction in the yield and quality of soybean crop. Three independent genes Rsv1, Rsv3, and Rsv4, were found to provide host resistance in soybean. Rsv1 confers resistance to all but most virulant strains of SMV. Rsv1 has been mapped to soybean molecular linkage group (MLG) F by using molecular markers. The purpose of this study is to investigate the location of Rsv3 gene on soybean map using molecular markers. The Rsv3 gene of soybean confers resistance to the most vurulent strains (G5-G7) of SMV. In order to map the gene, an F2 population was constructed from a cross between L29, an Rsv3 isoline of 'Williams', and 'Lee 68', a susceptible cultivar. Rsv3 genotypes of 183 F2 plants were determined by inoculating F2:3 progeny with the G7 strain of SMV. A preliminary survey of two parental lines, near isogenic lines (NILs), and bulk segregants with 136 restriction fragment length polymorphism (RFLP) markers yielded 36 markers showing variation between the two parents. These polymorphic RFLP markers unable to provided any indication of linkage to Rsv3. As an alternative strategy, amplified fragment length polymorphic (AFLP) marker analysis of the two parental lines, NILs and bulk segregants was performed using 64 primer combinations. Initial breakthrough came in the form of AFLP primer combination of Eco+AAC/Mse+CTG exhibited polymorphism between NILs, bulk segregants, and two parental lines. This AFLP marker was isolated and cloned to convert it into a RFLP clone to further investigate the linkage to Rsv3 by F2 segregation analysis. A mapping population constructed by crossing Glycine max x Glycine soja employed in determining the location AFLP-derived RFLP clone on soybean linkage map. This population has densely mapped molecular marker data that enabled determining the location of AFLP-derived RFLP clone ACR1 on soybean molecular linkage group (MLG) B2 between the markers pA516 and pA519. This finding, made it easy to establish the linkage of markers pA519, pA516, and pA593 in L29 x Lee 68 population by F2 segregation analysis. The closest marker linked pA519, was 0.9 cM away from Rsv3. In another study Rsv4 is reported to be mapped to MLG D1b of soybean. Results of this study are useful in marker-based selection (MAS), pyramiding viral resistance genes and in cloning the Rsv3 gene. / Master of Science

<p>This thesis describes an optimising compiler for translating from SMV to CLP(B). The optimisation is aimed at reducing the number of required variables in order to decrease the size of the resulting BDDs. Also a partitioning of the transition relation is performed. The compiler uses an internal representation of a FSM that is built up from the SMV description. A number of rewrite steps are performed on the problem description such as encoding to a Boolean domain and performing the optimisations. </p><p>The variable reduction heuristic is based on finding sub-circuits that are suitable for reduction and a state space search is performed on those groups. An evaluation of the results shows that in some cases the compiler is able to greatly reduce the size of the resulting BDDs.</p>

This thesis describes an optimising compiler for translating from SMV to CLP(B). The optimisation is aimed at reducing the number of required variables in order to decrease the size of the resulting BDDs. Also a partitioning of the transition relation is performed. The compiler uses an internal representation of a FSM that is built up from the SMV description. A number of rewrite steps are performed on the problem description such as encoding to a Boolean domain and performing the optimisations. The variable reduction heuristic is based on finding sub-circuits that are suitable for reduction and a state space search is performed on those groups. An evaluation of the results shows that in some cases the compiler is able to greatly reduce the size of the resulting BDDs.

This thesis is focused on IEC 61850 communication protocols SMV, GOOSE and MMS and their implementation in SCADA systems. There is a simulator, run on Raspberry Pi, that generates data according to IEC 61850 and transmits the data using protocols in question. The simulation consist of various virtual devices e.g. surge protection, undervoltage protection, circuit breaker, disconnector, HMI. The MMS protocol is used for station control. Simulation can be user-defined from textual configuration file.

The work deals with communication protocols of the IEC 61850 standard. The protocols GOOSE (Generic Object Oriented Substation Events), SMV (Sampled Measured Values) and MMS (Manufacturing Message Specification) are described. The protocols are used to create a simulation network, which is described in this work. The simulation network is created in the OMNeT ++, program installed in the Ubuntu virtual environment.

The operation of the smart grid is expected to be heavily reliant on microprocessor-based control. Thus, there is a strong need for interoperability standards to address the heterogeneous nature of the data in the smart grid. In this research, we analyzed in detail the security threats of the Generic Object Oriented Substation Events (GOOSE) and Sampled Measured Values (SMV) protocol mappings of the IEC 61850 data modeling standard, which is the most widely industry-accepted standard for power system automation and control. We found that there is a strong need for security solutions that are capable of defending the grid against cyber-attacks, minimizing the damage in case a cyber-incident occurs, and restoring services within minimal time. To address these risks, we focused on correlating cyber security algorithms with physical characteristics of the power system by developing intelligent agents that use this knowledge as an important second line of defense in detecting malicious activity. This will complement the cyber security methods, including encryption and authentication. Firstly, we developed a physical-model-checking algorithm, which uses artificial neural networks to identify switching-related attacks on power systems based on load flow characteristics. Secondly, the feasibility of using neural network forecasters to detect spoofed sampled values was investigated. We showed that although such forecasters have high spoofed-data-detection accuracy, they are prone to the accumulation of forecasting error. In this research, we proposed an algorithm to detect the accumulation of the forecasting error based on lightweight statistical indicators. The effectiveness of the proposed algorithms was experimentally verified on the Smart Grid testbed at FIU. The test results showed that the proposed techniques have a minimal detection latency, in the range of microseconds. Also, in this research we developed a network-in-the-loop co-simulation platform that seamlessly integrates the components of the smart grid together, especially since they are governed by different regulations and owned by different entities. Power system simulation software, microcontrollers, and a real communication infrastructure were combined together to provide a cohesive smart grid platform. A data-centric communication scheme was selected to provide an interoperability layer between multi-vendor devices, software packages, and to bridge different protocols together.

We present a methodology of an agile formal method named eXtreme Formal Modeling (XFM) recently developed by us, based on Extreme Programming concepts to construct abstract models from a natural language specification of a complex system. In particular, we focus on Prescriptive Formal Models (PFMs) that capture the specification of the system under design in a mathematically precise manner. Such models can be used as golden reference models for formal verification, test generation, etc. This methodology for incrementally building PFMs work by adding user stories (expressed as LTL formulae) gleaned from the natural language specifications, one by one, into the model. XFM builds the models, retaining correctness with respect to incrementally added properties by regressively model checking all the LTL properties captured theretofore in the model. We illustrate XFM with a graded set of examples including a traffic light controller, a DLX pipeline and a Smart Building control system. To make the regressive model checking steps feasible with current model checking tools, we need to keep the model size increments under control. We therefore analyze the effects of ordering LTL properties in XFM. We compare three different property-ordering methodologies: 'arbitrary ordering', 'property based ordering' and 'predicate based ordering'. We experiment on the models of the ISA bus monitor and the arbitration phase of the Pentium Pro bus. We experimentally show and mathematically reason that predicate based ordering is the best among these orderings. Finally, we present a GUI based toolbox for users to build PFMs using XFM. / Master of Science