Generalized Symbolic Execution for Model Checking and Testing

NASA Technical Reports Server (NTRS)

Khurshid, Sarfraz; Pasareanu, Corina; Visser, Willem; Kofmeyer, David (Technical Monitor)

2003-01-01

Modern software systems, which often are concurrent and manipulate complex data structures must be extremely reliable. We present a novel framework based on symbolic execution, for automated checking of such systems. We provide a two-fold generalization of traditional symbolic execution based approaches: one, we define a program instrumentation, which enables standard model checkers to perform symbolic execution; two, we give a novel symbolic execution algorithm that handles dynamically allocated structures (e.g., lists and trees), method preconditions (e.g., acyclicity of lists), data (e.g., integers and strings) and concurrency. The program instrumentation enables a model checker to automatically explore program heap configurations (using a systematic treatment of aliasing) and manipulate logical formulae on program data values (using a decision procedure). We illustrate two applications of our framework: checking correctness of multi-threaded programs that take inputs from unbounded domains with complex structure and generation of non-isomorphic test inputs that satisfy a testing criterion. Our implementation for Java uses the Java PathFinder model checker.

Test-Case Generation using an Explicit State Model Checker Final Report

NASA Technical Reports Server (NTRS)

Heimdahl, Mats P. E.; Gao, Jimin

2003-01-01

In the project 'Test-Case Generation using an Explicit State Model Checker' we have extended an existing tools infrastructure for formal modeling to export Java code so that we can use the NASA Ames tool Java Pathfinder (JPF) for test case generation. We have completed a translator from our source language RSML(exp -e) to Java and conducted initial studies of how JPF can be used as a testing tool. In this final report, we provide a detailed description of the translation approach as implemented in our tools.

A Scenario-Based Protocol Checker for Public-Key Authentication Scheme

NASA Astrophysics Data System (ADS)

Saito, Takamichi

Security protocol provides communication security for the internet. One of the important features of it is authentication with key exchange. Its correctness is a requirement of the whole of the communication security. In this paper, we introduce three attack models realized as their attack scenarios, and provide an authentication-protocol checker for applying three attack-scenarios based on the models. We also utilize it to check two popular security protocols: Secure SHell (SSH) and Secure Socket Layer/Transport Layer Security (SSL/TLS).

Elderly’s Family Life Supplies - Innovative Chinese Checkers Game Board

NASA Astrophysics Data System (ADS)

CHAO, Fanglin

2017-09-01

The product design course for industrial design students was implemented in our university which spans 9 weeks. Throughout the creativity rules and field study, students achieve high standard on problem identification and concept generation. The prototype test with elderly in design projects is helpful to make students with deeper understand user demand, which in turn enhance the concept further. Traditional Chinese checkers are redesigned using special checkers with different height or shape and specific rules to increase user interest and game diversity. Game is more challenging due to location weighting on score calculation to planning its strategies. Redesign Chinese checkers game board include reconfigurable board and several shape checkers. Checkers has 3 parts: standing ring body, the base body, both support the side holding structure. The body shows slightly concave to facilitate the fingers hold. The upper portion of the body is provided with different shapes extension section which can be engaged with base body. Player move the checker to the opposite target area. When one of player moved all the checkers to the opposite target area; they shift to the scoring calculation stage. The participant may develop specific strategy to gain higher score by maximized weighted checkers into its target block regions.

Efficient design of CMOS TSC checkers

NASA Technical Reports Server (NTRS)

Biddappa, Anita; Shamanna, Manjunath K.; Maki, Gary; Whitaker, Sterling

1990-01-01

This paper considers the design of an efficient, robustly testable, CMOS Totally Self-Checking (TSC) Checker for k-out-of-2k codes. Most existing implementations use primitive gates and assume the single stuck-at fault model. The self-testing property has been found to fail for CMOS TSC checkers under the stuck-open fault model due to timing skews and arbitrary delays in the circuit. A new four level design using CMOS primitive gates (NAND, NOR, INVERTERS) is presented. This design retains its properties under the stuck-open fault model. Additionally, this method offers an impressive reduction (greater than 70 percent) in gate count, gate inputs, and test set size when compared to the existing method. This implementation is easily realizable and is based on Anderson's technique. A thorough comparative study has been made on the proposed implementation and Kundu's implementation and the results indicate that the proposed one is better than Kundu's in all respects for k-out-of-2k codes.

Spot: A Programming Language for Verified Flight Software

NASA Technical Reports Server (NTRS)

Bocchino, Robert L., Jr.; Gamble, Edward; Gostelow, Kim P.; Some, Raphael R.

2014-01-01

The C programming language is widely used for programming space flight software and other safety-critical real time systems. C, however, is far from ideal for this purpose: as is well known, it is both low-level and unsafe. This paper describes Spot, a language derived from C for programming space flight systems. Spot aims to maintain compatibility with existing C code while improving the language and supporting verification with the SPIN model checker. The major features of Spot include actor-based concurrency, distributed state with message passing and transactional updates, and annotations for testing and verification. Spot also supports domain-specific annotations for managing spacecraft state, e.g., communicating telemetry information to the ground. We describe the motivation and design rationale for Spot, give an overview of the design, provide examples of Spot's capabilities, and discuss the current status of the implementation.

Introduction of Virtualization Technology to Multi-Process Model Checking

NASA Technical Reports Server (NTRS)

Leungwattanakit, Watcharin; Artho, Cyrille; Hagiya, Masami; Tanabe, Yoshinori; Yamamoto, Mitsuharu

2009-01-01

Model checkers find failures in software by exploring every possible execution schedule. Java PathFinder (JPF), a Java model checker, has been extended recently to cover networked applications by caching data transferred in a communication channel. A target process is executed by JPF, whereas its peer process runs on a regular virtual machine outside. However, non-deterministic target programs may produce different output data in each schedule, causing the cache to restart the peer process to handle the different set of data. Virtualization tools could help us restore previous states of peers, eliminating peer restart. This paper proposes the application of virtualization technology to networked model checking, concentrating on JPF.

Secure Transaction Protocol for CEPS Compliant EPS in Limited Connectivity Environment

NASA Astrophysics Data System (ADS)

Devane, Satish; Phatak, Deepak

Common Electronic Purse Specification (CEPS) used by European countries, elaborately defines the transaction between customer’s CEP card and merchant’s point of sales (POS) terminal. However it merely defines the specification to transfer the transactions between the Merchant and Merchant Acquirer (MA). This paper proposes a novel approach by introducing an entity, mobile merchant acquirer (MMA) which is a trusted agent of MA and principally works on man in middle concept, but facilitates remote two fold mutual authentication and secure transaction transfer between Merchant and MA through MMA. This approach removes the bottle-neck of connectivity issues between Merchant and MA in limited connectivity environment. The proposed protocol ensures the confidentiality, integrity and money atomicity of transaction batch. The proposed protocol has been verified for correctness by Spin, a model checker and security properties of the protocol have been verified by avispa.

Checking the Symptom Checkers

MedlinePlus

... emergencies, with appropriate advice given in 80% of cases. Some symptom checkers provided more accurate advice than others. Overall, the checkers tended to be cautious, encouraging users to seek health care when self care would do. “These tools may be useful in patients who are trying ...

Efficient Translation of LTL Formulae into Buchi Automata

NASA Technical Reports Server (NTRS)

Giannakopoulou, Dimitra; Lerda, Flavio

2001-01-01

Model checking is a fully automated technique for checking that a system satisfies a set of required properties. With explicit-state model checkers, properties are typically defined in linear-time temporal logic (LTL), and are translated into B chi automata in order to be checked. This report presents how we have combined and improved existing techniques to obtain an efficient LTL to B chi automata translator. In particular, we optimize the core of existing tableau-based approaches to generate significantly smaller automata. Our approach has been implemented and is being released as part of the Java PathFinder software (JPF), an explicit state model checker under development at the NASA Ames Research Center.

Addressing Dynamic Issues of Program Model Checking

NASA Technical Reports Server (NTRS)

Lerda, Flavio; Visser, Willem

2001-01-01

Model checking real programs has recently become an active research area. Programs however exhibit two characteristics that make model checking difficult: the complexity of their state and the dynamic nature of many programs. Here we address both these issues within the context of the Java PathFinder (JPF) model checker. Firstly, we will show how the state of a Java program can be encoded efficiently and how this encoding can be exploited to improve model checking. Next we show how to use symmetry reductions to alleviate some of the problems introduced by the dynamic nature of Java programs. Lastly, we show how distributed model checking of a dynamic program can be achieved, and furthermore, how dynamic partitions of the state space can improve model checking. We support all our findings with results from applying these techniques within the JPF model checker.

Formal methods for test case generation

NASA Technical Reports Server (NTRS)

Rushby, John (Inventor); De Moura, Leonardo Mendonga (Inventor); Hamon, Gregoire (Inventor)

2011-01-01

The invention relates to the use of model checkers to generate efficient test sets for hardware and software systems. The method provides for extending existing tests to reach new coverage targets; searching *to* some or all of the uncovered targets in parallel; searching in parallel *from* some or all of the states reached in previous tests; and slicing the model relative to the current set of coverage targets. The invention provides efficient test case generation and test set formation. Deep regions of the state space can be reached within allotted time and memory. The approach has been applied to use of the model checkers of SRI's SAL system and to model-based designs developed in Stateflow. Stateflow models achieving complete state and transition coverage in a single test case are reported.

Does It Work? 555-Timer Checker Leaves No Doubt

ERIC Educational Resources Information Center

Harman, Charles

2009-01-01

This article details the construction and use of the 555-timer checker. The 555-timer checker allows the user to dynamically check a 555-timer, an integrated circuit device. Of its many applications, it provides timing applications that unijunction transistors once performed. (Contains 4 figures and 3 photos.)

Spelling: Computerised Feedback for Self-Correction

ERIC Educational Resources Information Center

Lawley, Jim

2016-01-01

Research has shown that any assumption that L2 learners of English do well to rely on the feedback provided by generic spell checkers (for example, the MS Word spell checker) is misplaced. Efforts to develop spell checkers specifically for L2 learners have focused on training software to offer more appropriate suggestion lists for replacing…

My New Teaching Partner? Using the Grammar Checker in Writing Instruction

ERIC Educational Resources Information Center

Potter, Reva; Fuller, Dorothy

2008-01-01

Grammar checkers do not claim to teach grammar; they are tools to bring potential problems to the writer's attention. They also offer only formal and Standard English preferences, limiting the freer expression of some literary forms. Without guidance, students may misuse the checker, become frustrated, and feel discouraged. Users must be…

Formal Verification Toolkit for Requirements and Early Design Stages

NASA Technical Reports Server (NTRS)

Badger, Julia M.; Miller, Sheena Judson

2011-01-01

Efficient flight software development from natural language requirements needs an effective way to test designs earlier in the software design cycle. A method to automatically derive logical safety constraints and the design state space from natural language requirements is described. The constraints can then be checked using a logical consistency checker and also be used in a symbolic model checker to verify the early design of the system. This method was used to verify a hybrid control design for the suit ports on NASA Johnson Space Center's Space Exploration Vehicle against safety requirements.

FipsOrtho: A Spell Checker for Learners of French

ERIC Educational Resources Information Center

L'Haire, Sebastien

2007-01-01

This paper presents FipsOrtho, a spell checker targeted at learners of French, and a corpus of learners' errors which has been gathered to test the system and to get a sample of specific language learners' errors. Spell checkers are a standard feature of many software products, however they are not designed for specific language learners' errors.…

The Termination of Checking and the Role of Just Right Feelings: A Study of Obsessional Checkers Compared with Anxious and Non-clinical Controls.

PubMed

Salkovskis, Paul M; Millar, Josie; Gregory, James D; Wahl, Karina

2017-03-01

Repeated checking in OCD can be understood from a cognitive perspective as the motivated need to achieve certainty about the outcome of a potentially risky action, leading to the application of Elevated Evidence Requirements (EER) and overuse of subjective criteria. Twenty-four obsessional checkers, 22 anxious controls, and 26 non-clinical controls were interviewed about and rated recent episodes where they felt (a) they needed to check and (b) checked mainly out of habit (i.e. not obsessionally). Both subjective and objective criteria were rated as significantly more important in obsessional checkers than in controls; obsessional checkers also used more criteria overall for the termination of the check, and rated more criteria as "extremely important" than the control groups. The termination of the check was rated as more effortful for obsessional checkers than for the comparison groups. Analysis of the interview data was consistent with the ratings. Feelings of "rightness" were associated with the termination of a check for obsessional checkers but not for controls. Results were consistent with the proposal that the use of "just right feelings" to terminate checking are related to EER.

Using Runtime Analysis to Guide Model Checking of Java Programs

NASA Technical Reports Server (NTRS)

Havelund, Klaus; Norvig, Peter (Technical Monitor)

2001-01-01

This paper describes how two runtime analysis algorithms, an existing data race detection algorithm and a new deadlock detection algorithm, have been implemented to analyze Java programs. Runtime analysis is based on the idea of executing the program once. and observing the generated run to extract various kinds of information. This information can then be used to predict whether other different runs may violate some properties of interest, in addition of course to demonstrate whether the generated run itself violates such properties. These runtime analyses can be performed stand-alone to generate a set of warnings. It is furthermore demonstrated how these warnings can be used to guide a model checker, thereby reducing the search space. The described techniques have been implemented in the b e grown Java model checker called PathFinder.

Formal Analysis of the Remote Agent Before and After Flight

NASA Technical Reports Server (NTRS)

Havelund, Klaus; Lowry, Mike; Park, SeungJoon; Pecheur, Charles; Penix, John; Visser, Willem; White, Jon L.

2000-01-01

This paper describes two separate efforts that used the SPIN model checker to verify deep space autonomy flight software. The first effort occurred at the beginning of a spiral development process and found five concurrency errors early in the design cycle that the developers acknowledge would not have been found through testing. This effort required a substantial manual modeling effort involving both abstraction and translation from the prototype LISP code to the PROMELA language used by SPIN. This experience and others led to research to address the gap between formal method tools and the development cycle used by software developers. The Java PathFinder tool which directly translates from Java to PROMELA was developed as part of this research, as well as automatic abstraction tools. In 1999 the flight software flew on a space mission, and a deadlock occurred in a sibling subsystem to the one which was the focus of the first verification effort. A second quick-response "cleanroom" verification effort found the concurrency error in a short amount of time. The error was isomorphic to one of the concurrency errors found during the first verification effort. The paper demonstrates that formal methods tools can find concurrency errors that indeed lead to loss of spacecraft functions, even for the complex software required for autonomy. Second, it describes progress in automatic translation and abstraction that eventually will enable formal methods tools to be inserted directly into the aerospace software development cycle.

Model Checking Failed Conjectures in Theorem Proving: A Case Study

NASA Technical Reports Server (NTRS)

Pike, Lee; Miner, Paul; Torres-Pomales, Wilfredo

2004-01-01

Interactive mechanical theorem proving can provide high assurance of correct design, but it can also be a slow iterative process. Much time is spent determining why a proof of a conjecture is not forthcoming. In some cases, the conjecture is false and in others, the attempted proof is insufficient. In this case study, we use the SAL family of model checkers to generate a concrete counterexample to an unproven conjecture specified in the mechanical theorem prover, PVS. The focus of our case study is the ROBUS Interactive Consistency Protocol. We combine the use of a mechanical theorem prover and a model checker to expose a subtle flaw in the protocol that occurs under a particular scenario of faults and processor states. Uncovering the flaw allows us to mend the protocol and complete its general verification in PVS.

SimCheck: An Expressive Type System for Simulink

NASA Technical Reports Server (NTRS)

Roy, Pritam; Shankar, Natarajan

2010-01-01

MATLAB Simulink is a member of a class of visual languages that are used for modeling and simulating physical and cyber-physical systems. A Simulink model consists of blocks with input and output ports connected using links that carry signals. We extend the type system of Simulink with annotations and dimensions/units associated with ports and links. These types can capture invariants on signals as well as relations between signals. We define a type-checker that checks the wellformedness of Simulink blocks with respect to these type annotations. The type checker generates proof obligations that are solved by SRI's Yices solver for satisfiability modulo theories (SMT). This translation can be used to detect type errors, demonstrate counterexamples, generate test cases, or prove the absence of type errors. Our work is an initial step toward the symbolic analysis of MATLAB Simulink models.

Learning Game Evaluation Functions with a Compound Linear Machine.

DTIC Science & Technology

1980-03-01

Comparison to Non-Learning Shannon Type Programs . . . 50 Comparison to Samuel’s Shannon Type Checker Program . 52 Comparison to an Advice-Taking Shannon...examples of programs or algorithms that play games. The most significant of these is usually held to be A. Samuel’s checker playing program because it is...his checker playing program (GRC, 1978:54-72). Another related study nl,. { .. . performed for the Air Force recommends researching computerized

Distinguishing manifestations of anxiety: how do personality traits of compulsive checkers differ from other anxious individuals?

PubMed

Gershuny, B S; Sher, K J; Rossy, L; Bishop, A K

2000-03-01

To better understand relations between personality and anxiety in general, and personality differences between compulsive checkers and nonchecking anxious individuals in particular, the current study was conducted. Participants included a nonclinical undergraduate sample of 36 compulsive checkers, 33 nonchecking anxious controls and 33 nonchecking nonanxious controls who were compared on five basic personality dimensions: emotional stability, extraversion, agreeableness, conscientiousness and intellect (Goldberg, 1992). Results indicated that a combined group of all anxious individuals was less extraverted and less emotionally stable than nonchecking/nonanxious controls. Results further indicated that compulsive checkers were less emotionally stable and more conscientious than nonchecking anxious controls. The implications of these findings, as well as the impact of the order of personality item presentation, are considered and discussed.

The neXtProt peptide uniqueness checker: a tool for the proteomics community.

PubMed

Schaeffer, Mathieu; Gateau, Alain; Teixeira, Daniel; Michel, Pierre-André; Zahn-Zabal, Monique; Lane, Lydie

2017-11-01

The neXtProt peptide uniqueness checker allows scientists to define which peptides can be used to validate the existence of human proteins, i.e. map uniquely versus multiply to human protein sequences taking into account isobaric substitutions, alternative splicing and single amino acid variants. The pepx program is available at https://github.com/calipho-sib/pepx and can be launched from the command line or through a cgi web interface. Indexing requires a sequence file in FASTA format. The peptide uniqueness checker tool is freely available on the web at https://www.nextprot.org/tools/peptide-uniqueness-checker and from the neXtProt API at https://api.nextprot.org/. lydie.lane@sib.swiss. © The Author(s) 2017. Published by Oxford University Press.

Parity generator and parity checker in the modified trinary number system using savart plate and spatial light modulator

NASA Astrophysics Data System (ADS)

Ghosh, Amal K.

2010-09-01

The parity generators and the checkers are the most important circuits in communication systems. With the development of multi-valued logic (MVL), the proposed system with parity generators and checkers is the most required using the recently developed optoelectronic technology in the modified trinary number (MTN) system. This system also meets up the tremendous needs of speeds by exploiting the savart plates and spatial light modulators (SLM) in the optical tree architecture (OTA).

The 5th Generation model of Particle Physics

NASA Astrophysics Data System (ADS)

Lach, Theodore

2009-05-01

The Standard model of Particle Physics is able to account for all known HEP phenomenon, yet it is not able to predict the masses of the quarks or leptons nor can it explain why they have their respective values. The Checker Board Model (CBM) predicts that there are 5 generation of quarks and leptons and shows a pattern to those masses, namely each three quarks or leptons (within adjacent generations or within a generation) are related to each other by a geometric mean relationship. A 2D structure of the nucleus can be imaged as 2D plate spinning on its axis, it would for all practical circumstances appear to be a 3D object. The masses of the hypothesized ``up'' and ``dn'' quarks determined by the CBM are 237.31 MeV and 42.392 MeV respectively. These new quarks in addition to a lepton of 7.4 MeV make up one of the missing generations. The details of this new particle physics model can be found at the web site: checkerboard.dnsalias.net. The only areas were this theory conflicts with existing dogma is in the value of the mass of the Top quark. The particle found at Fermi Lab must be some sort of composite particle containing Top quarks.

Practical Formal Verification of Diagnosability of Large Models via Symbolic Model Checking

NASA Technical Reports Server (NTRS)

Cavada, Roberto; Pecheur, Charles

2003-01-01

This document reports on the activities carried out during a four-week visit of Roberto Cavada at the NASA Ames Research Center. The main goal was to test the practical applicability of the framework proposed, where a diagnosability problem is reduced to a Symbolic Model Checking problem. Section 2 contains a brief explanation of major techniques currently used in Symbolic Model Checking, and how these techniques can be tuned in order to obtain good performances when using Model Checking tools. Diagnosability is performed on large and structured models of real plants. Section 3 describes how these plants are modeled, and how models can be simplified to improve the performance of Symbolic Model Checkers. Section 4 reports scalability results. Three test cases are briefly presented, and several parameters and techniques have been applied on those test cases in order to produce comparison tables. Furthermore, comparison between several Model Checkers is reported. Section 5 summarizes the application of diagnosability verification to a real application. Several properties have been tested, and results have been highlighted. Finally, section 6 draws some conclusions, and outlines future lines of research.

Combining multivariate statistics and the think-aloud protocol to assess Human-Computer Interaction barriers in symptom checkers.

PubMed

Marco-Ruiz, Luis; Bønes, Erlend; de la Asunción, Estela; Gabarron, Elia; Aviles-Solis, Juan Carlos; Lee, Eunji; Traver, Vicente; Sato, Keiichi; Bellika, Johan G

2017-10-01

Symptom checkers are software tools that allow users to submit a set of symptoms and receive advice related to them in the form of a diagnosis list, health information or triage. The heterogeneity of their potential users and the number of different components in their user interfaces can make testing with end-users unaffordable. We designed and executed a two-phase method to test the respiratory diseases module of the symptom checker Erdusyk. Phase I consisted of an online test with a large sample of users (n=53). In Phase I, users evaluated the system remotely and completed a questionnaire based on the Technology Acceptance Model. Principal Component Analysis was used to correlate each section of the interface with the questionnaire responses, thus identifying which areas of the user interface presented significant contributions to the technology acceptance. In the second phase, the think-aloud procedure was executed with a small number of samples (n=15), focusing on the areas with significant contributions to analyze the reasons for such contributions. Our method was used effectively to optimize the testing of symptom checker user interfaces. The method allowed kept the cost of testing at reasonable levels by restricting the use of the think-aloud procedure while still assuring a high amount of coverage. The main barriers detected in Erdusyk were related to problems understanding time repetition patterns, the selection of levels in scales to record intensities, navigation, the quantification of some symptom attributes, and the characteristics of the symptoms. Copyright © 2017 Elsevier Inc. All rights reserved.

John Rogers: "Checkers Up at the Farm."

ERIC Educational Resources Information Center

Zeller, Terry

1987-01-01

Based on John Rogers' 1887 painted plaster sculpture called "Checkers Up at the Farm," this lesson seeks to introduce primary-level students to the idea of sculpture in the round and how sculpture can communicate ideas, emotions, and values. (JDH)

Breast Cyst Aspiration

MedlinePlus

... TestingRead Article >>Plasma Viral Load TestingInsulin TherapyRead Article >>Insulin Therapy Visit our interactive symptom checker Visit our interactive symptom checker Get Started Related ArticlesPlasma Viral Load TestingRead ... TherapyRead Article >>Drugs, Procedures & DevicesInsulin TherapyThe goal of ...

Joint and Soft Tissue Injections

MedlinePlus

... TestingRead Article >>Plasma Viral Load TestingInsulin TherapyRead Article >>Insulin Therapy Visit our interactive symptom checker Visit our interactive symptom checker Get Started Related ArticlesPlasma Viral Load TestingRead ... TherapyRead Article >>Drugs, Procedures & DevicesInsulin TherapyThe goal of ...

Differences in neuropsychological performance between subtypes of obsessive-compulsive disorder.

PubMed

Nedeljkovic, Maja; Kyrios, Michael; Moulding, Richard; Doron, Guy; Wainwright, Kylie; Pantelis, Chris; Purcell, Rosemary; Maruff, Paul

2009-03-01

Neuropsychological studies have suggested that frontal-striatal dysfunction plays a role in obsessive-compulsive disorder (OCD), although findings have been inconsistent, possibly due to heterogeneity within the disorder and methodological issues. The purpose of the present study was therefore to compare the neuropsychological performance of different subtypes of OCD and matched non-clinical controls (NCs) on the Cambridge Automated Neuropsychological Test Battery (CANTAB). Fifty-nine OCD patients and 59 non-clinical controls completed selected tests from CANTAB examining executive function, visual memory and attentional-set shifting. Depression, anxiety and OCD symptoms were also assessed. From 59 OCD patients, four subtypes were identified: (i) washers; (ii) checkers; (iii) obsessionals; and (iv) mixed symptom profile. Comparisons between washers, checkers, obsessionals and NCs indicated few differences, although checkers were generally found to exhibit poorer performance on spatial working memory, while obsessionals performed poorly on the spatial recognition task. Both checkers and the mixed subgroups showed slowed initial movement on the Stockings of Cambridge planning task and poorer pattern recognition relative to NCs. Overall the results suggested greater impairments in performance on neuropsychological tasks in checkers relative to other subtypes, although the observed effects were small and the conclusions limited by the small subtype samples. Future research will need to account for factors that influence neuropsychological performance in OCD subtypes.

Software Certification for Temporal Properties With Affordable Tool Qualification

NASA Technical Reports Server (NTRS)

Xia, Songtao; DiVito, Benedetto L.

2005-01-01

It has been recognized that a framework based on proof-carrying code (also called semantic-based software certification in its community) could be used as a candidate software certification process for the avionics industry. To meet this goal, tools in the "trust base" of a proof-carrying code system must be qualified by regulatory authorities. A family of semantic-based software certification approaches is described, each different in expressive power, level of automation and trust base. Of particular interest is the so-called abstraction-carrying code, which can certify temporal properties. When a pure abstraction-carrying code method is used in the context of industrial software certification, the fact that the trust base includes a model checker would incur a high qualification cost. This position paper proposes a hybrid of abstraction-based and proof-based certification methods so that the model checker used by a client can be significantly simplified, thereby leading to lower cost in tool qualification.

Nixon's Checkers: A Rhetoric-Communication Criticism.

ERIC Educational Resources Information Center

Kneupper, Charles W.; Mabry, Edward A.

Richard Nixon's "Checkers" speech, a response to charges brought against the "Nixon fund," was primarily an effort to explain the behavior of Eisenhower's 1952 presidential-campaign staff. The effectiveness of this speech was largely due to Nixon's self-disclosure within the context of the speech's narrative mode. In…

Food Marketing: Cashier-Checker. Teacher's Guide. Competency Based Curriculum.

ERIC Educational Resources Information Center

Froelich, Larry; And Others

This teacher's guide is designed to accompany the Competency Based Cashier-Checker Curriculum student materials--see note. Contents include a listing of reference materials, tool and equipment lists, copy of the table of contents for student competency sheets, teacher's suggestions, and answer keys for information sheets and exercises.…

The "Checkers" Speech and Televised Political Communication.

ERIC Educational Resources Information Center

Flaningam, Carl

Richard Nixon's 1952 "Checkers" speech was an innovative use of television for political communication. Like television news itself, the campaign fund crisis behind the speech can be thought of in the same terms as other television melodrama, with the speech serving as its climactic episode. The speech adapted well to television because…

The KIT gene is associated with the english spotting coat color locus and congenital megacolon in Checkered Giant rabbits (Oryctolagus cuniculus).

PubMed

Fontanesi, Luca; Vargiolu, Manuela; Scotti, Emilio; Latorre, Rocco; Faussone Pellegrini, Maria Simonetta; Mazzoni, Maurizio; Asti, Martina; Chiocchetti, Roberto; Romeo, Giovanni; Clavenzani, Paolo; De Giorgio, Roberto

2014-01-01

The English spotting coat color locus in rabbits, also known as Dominant white spotting locus, is determined by an incompletely dominant allele (En). Rabbits homozygous for the recessive wild-type allele (en/en) are self-colored, heterozygous En/en rabbits are normally spotted, and homozygous En/En animals are almost completely white. Compared to vital en/en and En/en rabbits, En/En animals are subvital because of a dilated ("mega") cecum and ascending colon. In this study, we investigated the role of the KIT gene as a candidate for the English spotting locus in Checkered Giant rabbits and characterized the abnormalities affecting enteric neurons and c-kit positive interstitial cells of Cajal (ICC) in the megacolon of En/En rabbits. Twenty-one litters were obtained by crossing three Checkered Giant bucks (En/en) with nine Checkered Giant (En/en) and two en/en does, producing a total of 138 F1 and backcrossed rabbits. Resequencing all coding exons and portions of non-coding regions of the KIT gene in 28 rabbits of different breeds identified 98 polymorphisms. A single nucleotide polymorphism genotyped in all F1 families showed complete cosegregation with the English spotting coat color phenotype (θ=0.00 LOD  =75.56). KIT gene expression in cecum and colon specimens of En/En (pathological) rabbits was 5-10% of that of en/en (control) rabbits. En/En rabbits showed reduced and altered c-kit immunolabelled ICC compared to en/en controls. Morphometric data on whole mounts of the ascending colon showed a significant decrease of HuC/D (P<0.05) and substance P (P<0.01) immunoreactive neurons in En/En vs. en/en. Electron microscopy analysis showed neuronal and ICC abnormalities in En/En tissues. The En/En rabbit model shows neuro-ICC changes reminiscent of the human non-aganglionic megacolon. This rabbit model may provide a better understanding of the molecular abnormalities underlying conditions associated with non-aganglionic megacolon.

The KIT Gene Is Associated with the English Spotting Coat Color Locus and Congenital Megacolon in Checkered Giant Rabbits (Oryctolagus cuniculus)

PubMed Central

Fontanesi, Luca; Vargiolu, Manuela; Scotti, Emilio; Latorre, Rocco; Faussone Pellegrini, Maria Simonetta; Mazzoni, Maurizio; Asti, Martina; Chiocchetti, Roberto; Romeo, Giovanni; Clavenzani, Paolo; De Giorgio, Roberto

2014-01-01

The English spotting coat color locus in rabbits, also known as Dominant white spotting locus, is determined by an incompletely dominant allele (En). Rabbits homozygous for the recessive wild-type allele (en/en) are self-colored, heterozygous En/en rabbits are normally spotted, and homozygous En/En animals are almost completely white. Compared to vital en/en and En/en rabbits, En/En animals are subvital because of a dilated (“mega”) cecum and ascending colon. In this study, we investigated the role of the KIT gene as a candidate for the English spotting locus in Checkered Giant rabbits and characterized the abnormalities affecting enteric neurons and c-kit positive interstitial cells of Cajal (ICC) in the megacolon of En/En rabbits. Twenty-one litters were obtained by crossing three Checkered Giant bucks (En/en) with nine Checkered Giant (En/en) and two en/en does, producing a total of 138 F1 and backcrossed rabbits. Resequencing all coding exons and portions of non-coding regions of the KIT gene in 28 rabbits of different breeds identified 98 polymorphisms. A single nucleotide polymorphism genotyped in all F1 families showed complete cosegregation with the English spotting coat color phenotype (θ = 0.00 LOD  = 75.56). KIT gene expression in cecum and colon specimens of En/En (pathological) rabbits was 5–10% of that of en/en (control) rabbits. En/En rabbits showed reduced and altered c-kit immunolabelled ICC compared to en/en controls. Morphometric data on whole mounts of the ascending colon showed a significant decrease of HuC/D (P<0.05) and substance P (P<0.01) immunoreactive neurons in En/En vs. en/en. Electron microscopy analysis showed neuronal and ICC abnormalities in En/En tissues. The En/En rabbit model shows neuro-ICC changes reminiscent of the human non-aganglionic megacolon. This rabbit model may provide a better understanding of the molecular abnormalities underlying conditions associated with non-aganglionic megacolon. PMID:24736498

Integrated Formal Analysis of Timed-Triggered Ethernet

NASA Technical Reports Server (NTRS)

Dutertre, Bruno; Shankar, Nstarajan; Owre, Sam

2012-01-01

We present new results related to the verification of the Timed-Triggered Ethernet (TTE) clock synchronization protocol. This work extends previous verification of TTE based on model checking. We identify a suboptimal design choice in a compression function used in clock synchronization, and propose an improvement. We compare the original design and the improved definition using the SAL model checker.

The HTS barcode checker pipeline, a tool for automated detection of illegally traded species from high-throughput sequencing data.

PubMed

Lammers, Youri; Peelen, Tamara; Vos, Rutger A; Gravendeel, Barbara

2014-02-06

Mixtures of internationally traded organic substances can contain parts of species protected by the Convention on International Trade in Endangered Species of Wild Fauna and Flora (CITES). These mixtures often raise the suspicion of border control and customs offices, which can lead to confiscation, for example in the case of Traditional Chinese medicines (TCMs). High-throughput sequencing of DNA barcoding markers obtained from such samples provides insight into species constituents of mixtures, but manual cross-referencing of results against the CITES appendices is labor intensive. Matching DNA barcodes against NCBI GenBank using BLAST may yield misleading results both as false positives, due to incorrectly annotated sequences, and false negatives, due to spurious taxonomic re-assignment. Incongruence between the taxonomies of CITES and NCBI GenBank can result in erroneous estimates of illegal trade. The HTS barcode checker pipeline is an application for automated processing of sets of 'next generation' barcode sequences to determine whether these contain DNA barcodes obtained from species listed on the CITES appendices. This analytical pipeline builds upon and extends existing open-source applications for BLAST matching against the NCBI GenBank reference database and for taxonomic name reconciliation. In a single operation, reads are converted into taxonomic identifications matched with names on the CITES appendices. By inclusion of a blacklist and additional names databases, the HTS barcode checker pipeline prevents false positives and resolves taxonomic heterogeneity. The HTS barcode checker pipeline can detect and correctly identify DNA barcodes of CITES-protected species from reads obtained from TCM samples in just a few minutes. The pipeline facilitates and improves molecular monitoring of trade in endangered species, and can aid in safeguarding these species from extinction in the wild. The HTS barcode checker pipeline is available at https://github.com/naturalis/HTS-barcode-checker.

The HTS barcode checker pipeline, a tool for automated detection of illegally traded species from high-throughput sequencing data

PubMed Central

2014-01-01

Background Mixtures of internationally traded organic substances can contain parts of species protected by the Convention on International Trade in Endangered Species of Wild Fauna and Flora (CITES). These mixtures often raise the suspicion of border control and customs offices, which can lead to confiscation, for example in the case of Traditional Chinese medicines (TCMs). High-throughput sequencing of DNA barcoding markers obtained from such samples provides insight into species constituents of mixtures, but manual cross-referencing of results against the CITES appendices is labor intensive. Matching DNA barcodes against NCBI GenBank using BLAST may yield misleading results both as false positives, due to incorrectly annotated sequences, and false negatives, due to spurious taxonomic re-assignment. Incongruence between the taxonomies of CITES and NCBI GenBank can result in erroneous estimates of illegal trade. Results The HTS barcode checker pipeline is an application for automated processing of sets of 'next generation’ barcode sequences to determine whether these contain DNA barcodes obtained from species listed on the CITES appendices. This analytical pipeline builds upon and extends existing open-source applications for BLAST matching against the NCBI GenBank reference database and for taxonomic name reconciliation. In a single operation, reads are converted into taxonomic identifications matched with names on the CITES appendices. By inclusion of a blacklist and additional names databases, the HTS barcode checker pipeline prevents false positives and resolves taxonomic heterogeneity. Conclusions The HTS barcode checker pipeline can detect and correctly identify DNA barcodes of CITES-protected species from reads obtained from TCM samples in just a few minutes. The pipeline facilitates and improves molecular monitoring of trade in endangered species, and can aid in safeguarding these species from extinction in the wild. The HTS barcode checker pipeline is available at https://github.com/naturalis/HTS-barcode-checker. PMID:24502833

Formal Verification of a Power Controller Using the Real-Time Model Checker UPPAAL

NASA Technical Reports Server (NTRS)

Havelund, Klaus; Larsen, Kim Guldstrand; Skou, Arne

1999-01-01

A real-time system for power-down control in audio/video components is modeled and verified using the real-time model checker UPPAAL. The system is supposed to reside in an audio/video component and control (read from and write to) links to neighbor audio/video components such as TV, VCR and remote-control. In particular, the system is responsible for the powering up and down of the component in between the arrival of data, and in order to do so in a safe way without loss of data, it is essential that no link interrupts are lost. Hence, a component system is a multitasking system with hard real-time requirements, and we present techniques for modeling time consumption in such a multitasked, prioritized system. The work has been carried out in a collaboration between Aalborg University and the audio/video company B&O. By modeling the system, 3 design errors were identified and corrected, and the following verification confirmed the validity of the design but also revealed the necessity for an upper limit of the interrupt frequency. The resulting design has been implemented and it is going to be incorporated as part of a new product line.

Collaborative Platform for DFM

DTIC Science & Technology

2007-12-20

generation litho hotspot checkers have also been implemented in automated hotspot fixers that can automatically fix designs by making small changes...processing side (ex. new CMP models, etch models, litho models) and on the circuit side (ex. Process aware circuit analysis or yield optimization...Since final gate CD is a function of not only litho , but Post Exposure Bake, ashing, and etch, the processing module can be augmented with more

Framework for Evaluating Loop Invariant Detection Games in Relation to Automated Dynamic Invariant Detectors

DTIC Science & Technology

2015-09-01

Detectability ...............................................................................................37 Figure 20. Excel VBA Codes for Checker...National Vulnerability Database OS Operating System SQL Structured Query Language VC Verification Condition VBA Visual Basic for Applications...checks each of these assertions for detectability by Daikon. The checker is an Excel Visual Basic for Applications ( VBA ) script that checks the

Apprendre l'orthographe avec un correcteur orthographique (Learning Spelling with a Spell-Checker?)?

ERIC Educational Resources Information Center

Desmarais, Lise

1998-01-01

Reports a study with 27 adults, both native French-speakers and native English-speakers, on the effectiveness of using a spell-checker as the core element to teach French spelling. The method used authentic materials, individualized monitoring, screen and hard-copy text reading, and content sequencing based on errors. The approach generated…

Improving Systematic Constraint-driven Analysis Using Incremental and Parallel Techniques

DTIC Science & Technology

2012-05-01

and modeling latency of a cloud based subsystem. Members of my research group provided useful comments and ideas on my work in group meetings and...122 5.7.1 One structurally complex argument . . . . . . . . . . . . . . 122 5.7.2 Multiple independent arguments...Subject Tools . . . . . . . . . . . . . . . . . 131 6.1.1.1 JPF — Model Checker . . . . . . . . . . . . . . . . 131 6.1.1.2 Alloy — Using a SAT

The Pattern and Range of Movement of a Checkered Beetle Predator Relative to its Bark Beetle Prey

Treesearch

James T. Cronin; John D. Reeve; Richard Wilkens; Peter Turchin

2000-01-01

Theoretical studies of predator-prey population dynamics have increasingly centered on the role of space and the movement of organisms. Yet empirical studies have been slow to follow suit. Herein, we quantified the long range movement of a checkered beetle Thanasimus dublus, which is an important predator of a pernicious forest pest the southern...

Effects of Spell Checkers on English as a Second Language Students' Incidental Spelling Learning: A Cognitive Load Perspective

ERIC Educational Resources Information Center

Lin, Po-Han; Liu, Tzu-Chien; Paas, Fred

2017-01-01

Computer-based spell checkers help to correct misspells instantly. Almost all the word processing devices are now equipped with a spell-check function that either automatically corrects errors or provides a list of intended words. However, it is not clear on how the reliance on this convenient technological solution affects spelling learning.…

A Methodology for Formal Hardware Verification, with Application to Microprocessors.

DTIC Science & Technology

1993-08-29

concurrent programming lan- guages. Proceedings of the NATO Advanced Study Institute on Logics and Models of Concurrent Systems ( Colle - sur - Loup , France, 8-19...restricted class of formu- las . Bose and Fisher [26] developed a symbolic model checker based on a Cosmos switch-level model. Their modeling approach...verification using SDVS-the method and a case study. 17th Anuual Microprogramming Workshop (New Orleans, LA , 30 October-2 November 1984). Published as

Formal Methods Tool Qualification

NASA Technical Reports Server (NTRS)

Wagner, Lucas G.; Cofer, Darren; Slind, Konrad; Tinelli, Cesare; Mebsout, Alain

2017-01-01

Formal methods tools have been shown to be effective at finding defects in safety-critical digital systems including avionics systems. The publication of DO-178C and the accompanying formal methods supplement DO-333 allows applicants to obtain certification credit for the use of formal methods without providing justification for them as an alternative method. This project conducted an extensive study of existing formal methods tools, identifying obstacles to their qualification and proposing mitigations for those obstacles. Further, it interprets the qualification guidance for existing formal methods tools and provides case study examples for open source tools. This project also investigates the feasibility of verifying formal methods tools by generating proof certificates which capture proof of the formal methods tool's claim, which can be checked by an independent, proof certificate checking tool. Finally, the project investigates the feasibility of qualifying this proof certificate checker, in the DO-330 framework, in lieu of qualifying the model checker itself.

Didn't You Run the Spell Checker? Effects of Type of Spelling Error and Use of a Spell Checker on Perceptions of the Author

ERIC Educational Resources Information Center

Figueredo, Lauren; Varnhagen, Connie K.

2005-01-01

We investigated expectations regarding a writer's responsibility to proofread text for spelling errors when using a word processor. Undergraduate students read an essay and completed a questionnaire regarding their perceptions of the author and the quality of the essay. They then manipulated type of spelling error (no error, homophone error,…

Press to Test: Shop-Built BJT Checker Is Easy to Use

ERIC Educational Resources Information Center

Harman, Charles

2008-01-01

Whether a student or an instructor in an electronics lab, having the means to check the operation of a bipolar junction transistor (BJT) at the proto-board stage is a blessing. Most students do not have the experience or knowledge that it takes to recognize whether or not a BJT is operating. With this handy BJT checker, a student or the instructor…

Is This Op-Amp Any Good?: Lab-Built Checker Removes All Doubt!

ERIC Educational Resources Information Center

Harman, Charles

2007-01-01

Electronics instructors and students find it very helpful to be able to check an operational amplifier at the proto-board stage. Most students lack the experience or knowledge that it takes to recognize whether an op-amp is operating normally or not. This article discusses a handy op-amp checker that allows one to check and/or test op-amps at the…

Nanoscale on-chip all-optical logic parity checker in integrated plasmonic circuits in optical communication range

PubMed Central

Wang, Feifan; Gong, Zibo; Hu, Xiaoyong; Yang, Xiaoyu; Yang, Hong; Gong, Qihuang

2016-01-01

The nanoscale chip-integrated all-optical logic parity checker is an essential core component for optical computing systems and ultrahigh-speed ultrawide-band information processing chips. Unfortunately, little experimental progress has been made in development of these devices to date because of material bottleneck limitations and a lack of effective realization mechanisms. Here, we report a simple and efficient strategy for direct realization of nanoscale chip-integrated all-optical logic parity checkers in integrated plasmonic circuits in the optical communication range. The proposed parity checker consists of two-level cascaded exclusive-OR (XOR) logic gates that are realized based on the linear interference of surface plasmon polaritons propagating in the plasmonic waveguides. The parity of the number of logic 1s in the incident four-bit logic signals is determined, and the output signal is given the logic state 0 for even parity (and 1 for odd parity). Compared with previous reports, the overall device feature size is reduced by more than two orders of magnitude, while ultralow energy consumption is maintained. This work raises the possibility of realization of large-scale integrated information processing chips based on integrated plasmonic circuits, and also provides a way to overcome the intrinsic limitations of serious surface plasmon polariton losses for on-chip integration applications. PMID:27073154

Nanoscale on-chip all-optical logic parity checker in integrated plasmonic circuits in optical communication range.

PubMed

Wang, Feifan; Gong, Zibo; Hu, Xiaoyong; Yang, Xiaoyu; Yang, Hong; Gong, Qihuang

2016-04-13

The nanoscale chip-integrated all-optical logic parity checker is an essential core component for optical computing systems and ultrahigh-speed ultrawide-band information processing chips. Unfortunately, little experimental progress has been made in development of these devices to date because of material bottleneck limitations and a lack of effective realization mechanisms. Here, we report a simple and efficient strategy for direct realization of nanoscale chip-integrated all-optical logic parity checkers in integrated plasmonic circuits in the optical communication range. The proposed parity checker consists of two-level cascaded exclusive-OR (XOR) logic gates that are realized based on the linear interference of surface plasmon polaritons propagating in the plasmonic waveguides. The parity of the number of logic 1s in the incident four-bit logic signals is determined, and the output signal is given the logic state 0 for even parity (and 1 for odd parity). Compared with previous reports, the overall device feature size is reduced by more than two orders of magnitude, while ultralow energy consumption is maintained. This work raises the possibility of realization of large-scale integrated information processing chips based on integrated plasmonic circuits, and also provides a way to overcome the intrinsic limitations of serious surface plasmon polariton losses for on-chip integration applications.

Parallel Software Model Checking

DTIC Science & Technology

2015-01-08

checker. This project will explore this strategy to parallelize the generalized PDR algorithm for software model checking. It belongs to TF1 due to its ... focus on formal verification . Generalized PDR. Generalized Property Driven Rechability (GPDR) i is an algorithm for solving HORN-SMT reachability...subject to a penalty for failing to comply with a collection of information if it does not display a currently valid OMB control number. 1. REPORT DATE 08

Play It Again, Sam! Adapting Common Games into Multimedia Models Used for Student Reviews.

ERIC Educational Resources Information Center

Metcalf, Karen K.; Barlow, Amy; Hudson, Lisa; Jones, Elizabeth; Lyons, Dennis; Piersall, James; Munfus, Laureen

1998-01-01

Provides guidelines on how to adapt common games such as checkers, tic tac toe, obstacle courses, and memory joggers into interactive games in multimedia courseware. Emphasizes creating generic games that can be recycled and used for multiple topics to save development time and keep costs low. Discusses topic themes, game structure, and…

Adult Competency Education Kit. Basic Skills in Speaking, Math, and Reading for Employment. Part N. ACE Competency Based Job Descriptions: #65--Typist I; #67--Grocery Checker; #68--File Clerk; #69--Receptionist; #70--Bank Teller; #71--Clerk, General Office.

ERIC Educational Resources Information Center

San Mateo County Office of Education, Redwood City, CA. Career Preparation Centers.

This eleventh of fifteen sets of Adult Competency Education (ACE) Competency Based Job Descriptions in the ACE kit contains job descriptions for Typist I, Grocery Checker, File Clerk, Receptionist; Bank Teller; and Clerk, General Office. Each begins with a fact sheet that includes this information: occupational title, D.O.T. code, ACE number,…

Land-based crop phenotyping by image analysis: consistent canopy characterization from inconsistent field illumination.

PubMed

Chopin, Joshua; Kumar, Pankaj; Miklavcic, Stanley J

2018-01-01

One of the main challenges associated with image-based field phenotyping is the variability of illumination. During a single day's imaging session, or between different sessions on different days, the sun moves in and out of cloud cover and has varying intensity. How is one to know from consecutive images alone if a plant has become darker over time, or if the weather conditions have simply changed from clear to overcast? This is a significant problem to address as colour is an important phenotypic trait that can be measured automatically from images. In this work we use an industry standard colour checker to balance the colour in images within and across every day of a field trial conducted over four months in 2016. By ensuring that the colour checker is present in every image we are afforded a 'ground truth' to correct for varying illumination conditions across images. We employ a least squares approach to fit a quadratic model for correcting RGB values of an image in such a way that the observed values of the colour checker tiles align with their true values after the transformation. The proposed method is successful in reducing the error between observed and reference colour chart values in all images. Furthermore, the standard deviation of mean canopy colour across multiple days is reduced significantly after colour correction is applied. Finally, we use a number of examples to demonstrate the usefulness of accurate colour measurements in recording phenotypic traits and analysing variation among varieties and treatments.

Design of parity generator and checker circuit using electro-optic effect of Mach-Zehnder interferometers

NASA Astrophysics Data System (ADS)

Kumar, Santosh; Chanderkanta; Amphawan, Angela

2016-04-01

Parity is an extra bit which is used to add in digital information to detect error at the receiver end. It can be even and odd parity. In case of even parity, the number of one's will be even included the parity and reverse in the case of odd parity. The circuit which is used to generate the parity at the transmitter side, called the parity generator and the circuit which is used to detect the parity at receiver side is called as parity checker. In this paper, an even and odd parity generator and checker circuits are designed using electro-optic effect inside lithium niobate based Mach-Zehnder Interferometers (MZIs). The MZIs structures collectively show powerful capability in switching an input optical signal to a desired output port from a collection of output ports. The paper constitutes a mathematical description of the proposed device and thereafter simulation using MATLAB. The study is verified using beam propagation method (BPM).

Spectral imaging using consumer-level devices and kernel-based regression.

PubMed

Heikkinen, Ville; Cámara, Clara; Hirvonen, Tapani; Penttinen, Niko

2016-06-01

Hyperspectral reflectance factor image estimations were performed in the 400-700 nm wavelength range using a portable consumer-level laptop display as an adjustable light source for a trichromatic camera. Targets of interest were ColorChecker Classic samples, Munsell Matte samples, geometrically challenging tempera icon paintings from the turn of the 20th century, and human hands. Measurements and simulations were performed using Nikon D80 RGB camera and Dell Vostro 2520 laptop screen as a light source. Estimations were performed without spectral characteristics of the devices and by emphasizing simplicity for training sets and estimation model optimization. Spectral and color error images are shown for the estimations using line-scanned hyperspectral images as the ground truth. Estimations were performed using kernel-based regression models via a first-degree inhomogeneous polynomial kernel and a Matérn kernel, where in the latter case the median heuristic approach for model optimization and link function for bounded estimation were evaluated. Results suggest modest requirements for a training set and show that all estimation models have markedly improved accuracy with respect to the DE00 color distance (up to 99% for paintings and hands) and the Pearson distance (up to 98% for paintings and 99% for hands) from a weak training set (Digital ColorChecker SG) case when small representative training data were used in the estimation.

Model checking for linear temporal logic: An efficient implementation

NASA Technical Reports Server (NTRS)

Sherman, Rivi; Pnueli, Amir

1990-01-01

This report provides evidence to support the claim that model checking for linear temporal logic (LTL) is practically efficient. Two implementations of a linear temporal logic model checker is described. One is based on transforming the model checking problem into a satisfiability problem; the other checks an LTL formula for a finite model by computing the cross-product of the finite state transition graph of the program with a structure containing all possible models for the property. An experiment was done with a set of mutual exclusion algorithms and tested safety and liveness under fairness for these algorithms.

A service-oriented architecture for integrating the modeling and formal verification of genetic regulatory networks

PubMed Central

2009-01-01

Background The study of biological networks has led to the development of increasingly large and detailed models. Computer tools are essential for the simulation of the dynamical behavior of the networks from the model. However, as the size of the models grows, it becomes infeasible to manually verify the predictions against experimental data or identify interesting features in a large number of simulation traces. Formal verification based on temporal logic and model checking provides promising methods to automate and scale the analysis of the models. However, a framework that tightly integrates modeling and simulation tools with model checkers is currently missing, on both the conceptual and the implementational level. Results We have developed a generic and modular web service, based on a service-oriented architecture, for integrating the modeling and formal verification of genetic regulatory networks. The architecture has been implemented in the context of the qualitative modeling and simulation tool GNA and the model checkers NUSMV and CADP. GNA has been extended with a verification module for the specification and checking of biological properties. The verification module also allows the display and visual inspection of the verification results. Conclusions The practical use of the proposed web service is illustrated by means of a scenario involving the analysis of a qualitative model of the carbon starvation response in E. coli. The service-oriented architecture allows modelers to define the model and proceed with the specification and formal verification of the biological properties by means of a unified graphical user interface. This guarantees a transparent access to formal verification technology for modelers of genetic regulatory networks. PMID:20042075

Component-Oriented Behavior Extraction for Autonomic System Design

NASA Technical Reports Server (NTRS)

Bakera, Marco; Wagner, Christian; Margaria,Tiziana; Hinchey, Mike; Vassev, Emil; Steffen, Bernhard

2009-01-01

Rich and multifaceted domain specific specification languages like the Autonomic System Specification Language (ASSL) help to design reliable systems with self-healing capabilities. The GEAR game-based Model Checker has been used successfully to investigate properties of the ESA Exo- Mars Rover in depth. We show here how to enable GEAR s game-based verification techniques for ASSL via systematic model extraction from a behavioral subset of the language, and illustrate it on a description of the Voyager II space mission.

Solving the AI Planning Plus Scheduling Problem Using Model Checking via Automatic Translation from the Abstract Plan Preparation Language (APPL) to the Symbolic Analysis Laboratory (SAL)

NASA Technical Reports Server (NTRS)

Butler, Ricky W.; Munoz, Cesar A.; Siminiceanu, Radu I.

2007-01-01

This paper describes a translator from a new planning language named the Abstract Plan Preparation Language (APPL) to the Symbolic Analysis Laboratory (SAL) model checker. This translator has been developed in support of the Spacecraft Autonomy for Vehicles and Habitats (SAVH) project sponsored by the Exploration Technology Development Program, which is seeking to mature autonomy technology for the vehicles and operations centers of Project Constellation.

ANSYS duplicate finite-element checker routine

NASA Technical Reports Server (NTRS)

Ortega, R.

1995-01-01

An ANSYS finite-element code routine to check for duplicated elements within the volume of a three-dimensional (3D) finite-element mesh was developed. The routine developed is used for checking floating elements within a mesh, identically duplicated elements, and intersecting elements with a common face. A space shuttle main engine alternate turbopump development high pressure oxidizer turbopump finite-element model check using the developed subroutine is discussed. Finally, recommendations are provided for duplicate element checking of 3D finite-element models.

Evolution of Control Programs for a Swarm of Autonomous Unmanned Aerial Vehicles

DTIC Science & Technology

2004-03-01

Game of Checkers,” IBM Journal of Research and Development , 3 (3):210–229 (July 1959). 91. Serway , R. A. Physics for Scientists and Engineers (Fourth...incomplete physics model is used for this research. Ignoring mass and the effects of gravity and friction greatly simplifies the model. At the same...of work on GAs [9, 60, 53]. The seminal work in GAs is the 1975 book Adaptation in Natural and Artificial Systems by John H. Holland [41]. In a GA

A High-Level Language for Modeling Algorithms and Their Properties

NASA Astrophysics Data System (ADS)

Akhtar, Sabina; Merz, Stephan; Quinson, Martin

Designers of concurrent and distributed algorithms usually express them using pseudo-code. In contrast, most verification techniques are based on more mathematically-oriented formalisms such as state transition systems. This conceptual gap contributes to hinder the use of formal verification techniques. Leslie Lamport introduced PlusCal, a high-level algorithmic language that has the "look and feel" of pseudo-code, but is equipped with a precise semantics and includes a high-level expression language based on set theory. PlusCal models can be compiled to TLA + and verified using the model checker tlc.

A UMLS-based spell checker for natural language processing in vaccine safety.

PubMed

Tolentino, Herman D; Matters, Michael D; Walop, Wikke; Law, Barbara; Tong, Wesley; Liu, Fang; Fontelo, Paul; Kohl, Katrin; Payne, Daniel C

2007-02-12

The Institute of Medicine has identified patient safety as a key goal for health care in the United States. Detecting vaccine adverse events is an important public health activity that contributes to patient safety. Reports about adverse events following immunization (AEFI) from surveillance systems contain free-text components that can be analyzed using natural language processing. To extract Unified Medical Language System (UMLS) concepts from free text and classify AEFI reports based on concepts they contain, we first needed to clean the text by expanding abbreviations and shortcuts and correcting spelling errors. Our objective in this paper was to create a UMLS-based spelling error correction tool as a first step in the natural language processing (NLP) pipeline for AEFI reports. We developed spell checking algorithms using open source tools. We used de-identified AEFI surveillance reports to create free-text data sets for analysis. After expansion of abbreviated clinical terms and shortcuts, we performed spelling correction in four steps: (1) error detection, (2) word list generation, (3) word list disambiguation and (4) error correction. We then measured the performance of the resulting spell checker by comparing it to manual correction. We used 12,056 words to train the spell checker and tested its performance on 8,131 words. During testing, sensitivity, specificity, and positive predictive value (PPV) for the spell checker were 74% (95% CI: 74-75), 100% (95% CI: 100-100), and 47% (95% CI: 46%-48%), respectively. We created a prototype spell checker that can be used to process AEFI reports. We used the UMLS Specialist Lexicon as the primary source of dictionary terms and the WordNet lexicon as a secondary source. We used the UMLS as a domain-specific source of dictionary terms to compare potentially misspelled words in the corpus. The prototype sensitivity was comparable to currently available tools, but the specificity was much superior. The slow processing speed may be improved by trimming it down to the most useful component algorithms. Other investigators may find the methods we developed useful for cleaning text using lexicons specific to their area of interest.

A UMLS-based spell checker for natural language processing in vaccine safety

PubMed Central

Tolentino, Herman D; Matters, Michael D; Walop, Wikke; Law, Barbara; Tong, Wesley; Liu, Fang; Fontelo, Paul; Kohl, Katrin; Payne, Daniel C

2007-01-01

Background The Institute of Medicine has identified patient safety as a key goal for health care in the United States. Detecting vaccine adverse events is an important public health activity that contributes to patient safety. Reports about adverse events following immunization (AEFI) from surveillance systems contain free-text components that can be analyzed using natural language processing. To extract Unified Medical Language System (UMLS) concepts from free text and classify AEFI reports based on concepts they contain, we first needed to clean the text by expanding abbreviations and shortcuts and correcting spelling errors. Our objective in this paper was to create a UMLS-based spelling error correction tool as a first step in the natural language processing (NLP) pipeline for AEFI reports. Methods We developed spell checking algorithms using open source tools. We used de-identified AEFI surveillance reports to create free-text data sets for analysis. After expansion of abbreviated clinical terms and shortcuts, we performed spelling correction in four steps: (1) error detection, (2) word list generation, (3) word list disambiguation and (4) error correction. We then measured the performance of the resulting spell checker by comparing it to manual correction. Results We used 12,056 words to train the spell checker and tested its performance on 8,131 words. During testing, sensitivity, specificity, and positive predictive value (PPV) for the spell checker were 74% (95% CI: 74–75), 100% (95% CI: 100–100), and 47% (95% CI: 46%–48%), respectively. Conclusion We created a prototype spell checker that can be used to process AEFI reports. We used the UMLS Specialist Lexicon as the primary source of dictionary terms and the WordNet lexicon as a secondary source. We used the UMLS as a domain-specific source of dictionary terms to compare potentially misspelled words in the corpus. The prototype sensitivity was comparable to currently available tools, but the specificity was much superior. The slow processing speed may be improved by trimming it down to the most useful component algorithms. Other investigators may find the methods we developed useful for cleaning text using lexicons specific to their area of interest. PMID:17295907

Locator-Checker-Scaler Object Tracking Using Spatially Ordered and Weighted Patch Descriptor.

PubMed

Kim, Han-Ul; Kim, Chang-Su

2017-08-01

In this paper, we propose a simple yet effective object descriptor and a novel tracking algorithm to track a target object accurately. For the object description, we divide the bounding box of a target object into multiple patches and describe them with color and gradient histograms. Then, we determine the foreground weight of each patch to alleviate the impacts of background information in the bounding box. To this end, we perform random walk with restart (RWR) simulation. We then concatenate the weighted patch descriptors to yield the spatially ordered and weighted patch (SOWP) descriptor. For the object tracking, we incorporate the proposed SOWP descriptor into a novel tracking algorithm, which has three components: locator, checker, and scaler (LCS). The locator and the scaler estimate the center location and the size of a target, respectively. The checker determines whether it is safe to adjust the target scale in a current frame. These three components cooperate with one another to achieve robust tracking. Experimental results demonstrate that the proposed LCS tracker achieves excellent performance on recent benchmarks.

Model Checking the Remote Agent Planner

NASA Technical Reports Server (NTRS)

Khatib, Lina; Muscettola, Nicola; Havelund, Klaus; Norvig, Peter (Technical Monitor)

2001-01-01

This work tackles the problem of using Model Checking for the purpose of verifying the HSTS (Scheduling Testbed System) planning system. HSTS is the planner and scheduler of the remote agent autonomous control system deployed in Deep Space One (DS1). Model Checking allows for the verification of domain models as well as planning entries. We have chosen the real-time model checker UPPAAL for this work. We start by motivating our work in the introduction. Then we give a brief description of HSTS and UPPAAL. After that, we give a sketch for the mapping of HSTS models into UPPAAL and we present samples of plan model properties one may want to verify.

Science of Cyber-Security

DTIC Science & Technology

2010-11-01

that a program is bug free. Also, and this is an important issue in getting people 29 to use them, static checkers tend to have false positives...enormous variety of non-standard dialects took a huge amount of work to get what they describe as full version-specific bug compatibility.) Model...coincident detection by T-cells. In- cidentally, this is why it is enough to get rid of T-cells that bind self-peptides without similarly culling B-cells

Design, Development, and Automated Verification of an Integrity-Protected Hypervisor

DTIC Science & Technology

2012-07-16

mechanism for implementing software virtualization. Since hypervisors execute at a very high privilege level, they must be secure. A fundamental security...using the CBMC model checker. CBMC verified XMHF?s implementation ? about 4700 lines of C code ? in about 80 seconds using less than 2GB of RAM. 15...Hypervisors are a popular mechanism for implementing software virtualization. Since hypervisors execute at a very high privilege level, they must be

Authoring and verification of clinical guidelines: a model driven approach.

PubMed

Pérez, Beatriz; Porres, Ivan

2010-08-01

The goal of this research is to provide a framework to enable authoring and verification of clinical guidelines. The framework is part of a larger research project aimed at improving the representation, quality and application of clinical guidelines in daily clinical practice. The verification process of a guideline is based on (1) model checking techniques to verify guidelines against semantic errors and inconsistencies in their definition, (2) combined with Model Driven Development (MDD) techniques, which enable us to automatically process manually created guideline specifications and temporal-logic statements to be checked and verified regarding these specifications, making the verification process faster and cost-effective. Particularly, we use UML statecharts to represent the dynamics of guidelines and, based on this manually defined guideline specifications, we use a MDD-based tool chain to automatically process them to generate the input model of a model checker. The model checker takes the resulted model together with the specific guideline requirements, and verifies whether the guideline fulfils such properties. The overall framework has been implemented as an Eclipse plug-in named GBDSSGenerator which, particularly, starting from the UML statechart representing a guideline, allows the verification of the guideline against specific requirements. Additionally, we have established a pattern-based approach for defining commonly occurring types of requirements in guidelines. We have successfully validated our overall approach by verifying properties in different clinical guidelines resulting in the detection of some inconsistencies in their definition. The proposed framework allows (1) the authoring and (2) the verification of clinical guidelines against specific requirements defined based on a set of property specification patterns, enabling non-experts to easily write formal specifications and thus easing the verification process. Copyright 2010 Elsevier Inc. All rights reserved.

A demonstration of CMOS VLSI circuit prototyping in support of the site facility using the 1.2 micron standard cell library developed by National Security Agency

NASA Technical Reports Server (NTRS)

Smith, Edwyn D.

1991-01-01

Two silicon CMOS application specific integrated circuits (ASICs), a data generation chip, and a data checker chip were designed. The conversion of the data generator circuitry into a pair of CMOS ASIC chips using the 1.2 micron standard cell library is documented. The logic design of the data checker is discussed. The functions of the control circuitry is described. An accurate estimate of timing relationships is essential to make sure that the logic design performs correctly under practical conditions. Timing and delay information are examined.

Handheld detector using NIR for bottled liquid explosives

NASA Astrophysics Data System (ADS)

Itozaki, Hideo; Sato-Akaba, Hideo

2014-10-01

A handheld bottle checker for detection of liquid explosives is developed using near infrared technology. In order to make it compact, a LED light was used as a light source and a novel circuit board was developed for the device control instead of using a PC. This enables low power consumption and this handheld detector can be powered by a Li-ion battery without an AC power supply. This checker works well to analyze liquids, even using limited bandwidth of NIR by the LED. It is expected that it can be applied not only to airport security but also to wider applications because of its compactness and portability.

COOPER, HERON, AND HEWARD'S APPLIED BEHAVIOR ANALYSIS (2ND ED.): CHECKERED FLAG FOR STUDENTS AND PROFESSORS, YELLOW FLAG FOR THE FIELD

PubMed Central

Friman, Patrick C

2010-01-01

At last, the field of applied behavior analysis has a beautifully crafted, true textbook that can proudly stand cover to cover and spine to spine beside any of the expensive, imposing, and ornately designed textbooks used by college instructors who teach courses in conventional areas of education or psychology. In this review, I fully laud this development, credit Cooper, Heron, and Heward for making it happen, argue that it signifies a checkered flag for students and professors, and recommend the book for classes in applied behavior analysis everywhere. Subsequently, I review its chapters, each of which could easily stand alone as publications in their own right. Finally, I supply a cautionary note, a yellow flag to accompany the well-earned checkered flag, by pointing out that, as is true with all general textbooks on applied behavior analysis, a major portion of the references involves research on persons who occupy only a tail of the normal distribution. To attain the mainstream role Skinner envisioned and most (if not all) behavior analysts desire, the field will have to increase its focus on persons who reside under the dome of that distribution.

A rule-based approach to model checking of UML state machines

NASA Astrophysics Data System (ADS)

Grobelna, Iwona; Grobelny, Michał; Stefanowicz, Łukasz

2016-12-01

In the paper a new approach to formal verification of control process specification expressed by means of UML state machines in version 2.x is proposed. In contrast to other approaches from the literature, we use the abstract and universal rule-based logical model suitable both for model checking (using the nuXmv model checker), but also for logical synthesis in form of rapid prototyping. Hence, a prototype implementation in hardware description language VHDL can be obtained that fully reflects the primary, already formally verified specification in form of UML state machines. Presented approach allows to increase the assurance that implemented system meets the user-defined requirements.

UTP and Temporal Logic Model Checking

NASA Astrophysics Data System (ADS)

Anderson, Hugh; Ciobanu, Gabriel; Freitas, Leo

In this paper we give an additional perspective to the formal verification of programs through temporal logic model checking, which uses Hoare and He Unifying Theories of Programming (UTP). Our perspective emphasizes the use of UTP designs, an alphabetised relational calculus expressed as a pre/post condition pair of relations, to verify state or temporal assertions about programs. The temporal model checking relation is derived from a satisfaction relation between the model and its properties. The contribution of this paper is that it shows a UTP perspective to temporal logic model checking. The approach includes the notion of efficiency found in traditional model checkers, which reduced a state explosion problem through the use of efficient data structures

The PlusCal Algorithm Language

NASA Astrophysics Data System (ADS)

Lamport, Leslie

Algorithms are different from programs and should not be described with programming languages. The only simple alternative to programming languages has been pseudo-code. PlusCal is an algorithm language that can be used right now to replace pseudo-code, for both sequential and concurrent algorithms. It is based on the TLA + specification language, and a PlusCal algorithm is automatically translated to a TLA + specification that can be checked with the TLC model checker and reasoned about formally.

Model Checker for Java Programs

NASA Technical Reports Server (NTRS)

Visser, Willem

2007-01-01

Java Pathfinder (JPF) is a verification and testing environment for Java that integrates model checking, program analysis, and testing. JPF consists of a custom-made Java Virtual Machine (JVM) that interprets bytecode, combined with a search interface to allow the complete behavior of a Java program to be analyzed, including interleavings of concurrent programs. JPF is implemented in Java, and its architecture is highly modular to support rapid prototyping of new features. JPF is an explicit-state model checker, because it enumerates all visited states and, therefore, suffers from the state-explosion problem inherent in analyzing large programs. It is suited to analyzing programs less than 10kLOC, but has been successfully applied to finding errors in concurrent programs up to 100kLOC. When an error is found, a trace from the initial state to the error is produced to guide the debugging. JPF works at the bytecode level, meaning that all of Java can be model-checked. By default, the software checks for all runtime errors (uncaught exceptions), assertions violations (supports Java s assert), and deadlocks. JPF uses garbage collection and symmetry reductions of the heap during model checking to reduce state-explosion, as well as dynamic partial order reductions to lower the number of interleavings analyzed. JPF is capable of symbolic execution of Java programs, including symbolic execution of complex data such as linked lists and trees. JPF is extensible as it allows for the creation of listeners that can subscribe to events during searches. The creation of dedicated code to be executed in place of regular classes is supported and allows users to easily handle native calls and to improve the efficiency of the analysis.

Safety Verification of a Fault Tolerant Reconfigurable Autonomous Goal-Based Robotic Control System

NASA Technical Reports Server (NTRS)

Braman, Julia M. B.; Murray, Richard M; Wagner, David A.

2007-01-01

Fault tolerance and safety verification of control systems are essential for the success of autonomous robotic systems. A control architecture called Mission Data System (MDS), developed at the Jet Propulsion Laboratory, takes a goal-based control approach. In this paper, a method for converting goal network control programs into linear hybrid systems is developed. The linear hybrid system can then be verified for safety in the presence of failures using existing symbolic model checkers. An example task is simulated in MDS and successfully verified using HyTech, a symbolic model checking software for linear hybrid systems.

Experimental Validation of a Time-Accurate Finite Element Model for Coupled Multibody Dynamics and Liquid Sloshing

DTIC Science & Technology

2007-04-16

velocity of the fluid mesh, P is the relative pressure, xr is the position vector, τ is the deviatoric stress tensor, D is the rate of deformation...corresponds to a slip factor of zero. The slip factor determines how much of the fluid and structure forces are mutually exchanged. Equations 22 and 23...updated from last to first. viii.Average the fluid pressure (This step eliminates the pressure checker-boarding effect and allows use of equal

Facial skin color measurement based on camera colorimetric characterization

NASA Astrophysics Data System (ADS)

Yang, Boquan; Zhou, Changhe; Wang, Shaoqing; Fan, Xin; Li, Chao

2016-10-01

The objective measurement of facial skin color and its variance is of great significance as much information can be obtained from it. In this paper, we developed a new skin color measurement procedure which includes following parts: first, a new skin tone color checker made of pantone Skin Tone Color Checker was designed for camera colorimetric characterization; second, the chromaticity of light source was estimated via a new scene illumination estimation method considering several previous algorithms; third, chromatic adaption was used to convert the input facial image into output facial image which appears taken under canonical light; finally the validity and accuracy of our method was verified by comparing the results obtained by our procedure with these by spectrophotometer.

Model Checking Satellite Operational Procedures

NASA Astrophysics Data System (ADS)

Cavaliere, Federico; Mari, Federico; Melatti, Igor; Minei, Giovanni; Salvo, Ivano; Tronci, Enrico; Verzino, Giovanni; Yushtein, Yuri

2011-08-01

We present a model checking approach for the automatic verification of satellite operational procedures (OPs). Building a model for a complex system as a satellite is a hard task. We overcome this obstruction by using a suitable simulator (SIMSAT) for the satellite. Our approach aims at improving OP quality assurance by automatic exhaustive exploration of all possible simulation scenarios. Moreover, our solution decreases OP verification costs by using a model checker (CMurphi) to automatically drive the simulator. We model OPs as user-executed programs observing the simulator telemetries and sending telecommands to the simulator. In order to assess feasibility of our approach we present experimental results on a simple meaningful scenario. Our results show that we can save up to 90% of verification time.

A Prototype Embedding of Bluespec System Verilog in the PVS Theorem Prover

NASA Technical Reports Server (NTRS)

Richards, Dominic; Lester, David

2010-01-01

Bluespec SystemVerilog (BSV) is a Hardware Description Language based on the guarded action model of concurrency. It has an elegant semantics, which makes it well suited for formal reasoning. To date, a number of BSV designs have been verified with hand proofs, but little work has been conducted on the application of automated reasoning. We present a prototype shallow embedding of BSV in the PVS theorem prover. Our embedding is compatible with the PVS model checker, which can automatically prove an important class of theorems, and can also be used in conjunction with the powerful proof strategies of PVS to verify a broader class of properties than can be achieved with model checking alone.

Model Checking with Edge-Valued Decision Diagrams

NASA Technical Reports Server (NTRS)

Roux, Pierre; Siminiceanu, Radu I.

2010-01-01

We describe an algebra of Edge-Valued Decision Diagrams (EVMDDs) to encode arithmetic functions and its implementation in a model checking library. We provide efficient algorithms for manipulating EVMDDs and review the theoretical time complexity of these algorithms for all basic arithmetic and relational operators. We also demonstrate that the time complexity of the generic recursive algorithm for applying a binary operator on EVMDDs is no worse than that of Multi- Terminal Decision Diagrams. We have implemented a new symbolic model checker with the intention to represent in one formalism the best techniques available at the moment across a spectrum of existing tools. Compared to the CUDD package, our tool is several orders of magnitude faster

Building a Formal Model of a Human-Interactive System: Insights into the Integration of Formal Methods and Human Factors Engineering

NASA Technical Reports Server (NTRS)

Bolton, Matthew L.; Bass, Ellen J.

2009-01-01

Both the human factors engineering (HFE) and formal methods communities are concerned with finding and eliminating problems with safety-critical systems. This work discusses a modeling effort that leveraged methods from both fields to use model checking with HFE practices to perform formal verification of a human-interactive system. Despite the use of a seemingly simple target system, a patient controlled analgesia pump, the initial model proved to be difficult for the model checker to verify in a reasonable amount of time. This resulted in a number of model revisions that affected the HFE architectural, representativeness, and understandability goals of the effort. If formal methods are to meet the needs of the HFE community, additional modeling tools and technological developments are necessary.

Towards a Certified Lightweight Array Bound Checker for Java Bytecode

NASA Technical Reports Server (NTRS)

Pichardie, David

2009-01-01

Dynamic array bound checks are crucial elements for the security of a Java Virtual Machines. These dynamic checks are however expensive and several static analysis techniques have been proposed to eliminate explicit bounds checks. Such analyses require advanced numerical and symbolic manipulations that 1) penalize bytecode loading or dynamic compilation, 2) complexify the trusted computing base. Following the Foundational Proof Carrying Code methodology, our goal is to provide a lightweight bytecode verifier for eliminating array bound checks that is both efficient and trustable. In this work, we define a generic relational program analysis for an imperative, stackoriented byte code language with procedures, arrays and global variables and instantiate it with a relational abstract domain as polyhedra. The analysis has automatic inference of loop invariants and method pre-/post-conditions, and efficient checking of analysis results by a simple checker. Invariants, which can be large, can be specialized for proving a safety policy using an automatic pruning technique which reduces their size. The result of the analysis can be checked efficiently by annotating the program with parts of the invariant together with certificates of polyhedral inclusions. The resulting checker is sufficiently simple to be entirely certified within the Coq proof assistant for a simple fragment of the Java bytecode language. During the talk, we will also report on our ongoing effort to scale this approach for the full sequential JVM.

Kate's Model Verification Tools

NASA Technical Reports Server (NTRS)

Morgan, Steve

1991-01-01

Kennedy Space Center's Knowledge-based Autonomous Test Engineer (KATE) is capable of monitoring electromechanical systems, diagnosing their errors, and even repairing them when they crash. A survey of KATE's developer/modelers revealed that they were already using a sophisticated set of productivity enhancing tools. They did request five more, however, and those make up the body of the information presented here: (1) a transfer function code fitter; (2) a FORTRAN-Lisp translator; (3) three existing structural consistency checkers to aid in syntax checking their modeled device frames; (4) an automated procedure for calibrating knowledge base admittances to protect KATE's hardware mockups from inadvertent hand valve twiddling; and (5) three alternatives for the 'pseudo object', a programming patch that currently apprises KATE's modeling devices of their operational environments.

Parallel State Space Construction for a Model Checking Based on Maximality Semantics

NASA Astrophysics Data System (ADS)

El Abidine Bouneb, Zine; Saīdouni, Djamel Eddine

2009-03-01

The main limiting factor of the model checker integrated in the concurrency verification environment FOCOVE [1, 2], which use the maximality based labeled transition system (noted MLTS) as a true concurrency model[3, 4], is currently the amount of available physical memory. Many techniques have been developed to reduce the size of a state space. An interesting technique among them is the alpha equivalence reduction. Distributed memory execution environment offers yet another choice. The main contribution of the paper is to show that the parallel state space construction algorithm proposed in [5], which is based on interleaving semantics using LTS as semantic model, may be adapted easily to the distributed implementation of the alpha equivalence reduction for the maximality based labeled transition systems.

Throat Problems (Symptom Checker)

MedlinePlus

... Kids and Teens Pregnancy and Childbirth Women Men Seniors Your Health Resources Healthcare Management End-of-Life Issues Insurance & Bills Self Care Working With Your Doctor Drugs, Procedures & Devices Over-the- ...

JAVA PathFinder

NASA Technical Reports Server (NTRS)

Mehhtz, Peter

2005-01-01

JPF is an explicit state software model checker for Java bytecode. Today, JPF is a swiss army knife for all sort of runtime based verification purposes. This basically means JPF is a Java virtual machine that executes your program not just once (like a normal VM), but theoretically in all possible ways, checking for property violations like deadlocks or unhandled exceptions along all potential execution paths. If it finds an error, JPF reports the whole execution that leads to it. Unlike a normal debugger, JPF keeps track of every step how it got to the defect.

Towards a Framework for Generating Tests to Satisfy Complex Code Coverage in Java Pathfinder

NASA Technical Reports Server (NTRS)

Staats, Matt

2009-01-01

We present work on a prototype tool based on the JavaPathfinder (JPF) model checker for automatically generating tests satisfying the MC/DC code coverage criterion. Using the Eclipse IDE, developers and testers can quickly instrument Java source code with JPF annotations covering all MC/DC coverage obligations, and JPF can then be used to automatically generate tests that satisfy these obligations. The prototype extension to JPF enables various tasks useful in automatic test generation to be performed, such as test suite reduction and execution of generated tests.

Implementing a Rule-Based Contract Compliance Checker

NASA Astrophysics Data System (ADS)

Strano, Massimo; Molina-Jimenez, Carlos; Shrivastava, Santosh

The paper describes the design and implementation of an independent, third party contract monitoring service called Contract Compliance Checker (CCC). The CCC is provided with the specification of the contract in force, and is capable of observing and logging the relevant business-to-business (B2B) interaction events, in order to determine whether the actions of the business partners are consistent with the contract. A contract specification language called EROP (for Events, Rights, Obligations and Prohibitions) for the CCC has been developed based on business rules, that provides constructs to specify what rights, obligation and prohibitions become active and inactive after the occurrence of events related to the execution of business operations. The system has been designed to work with B2B industry standards such as ebXML and RosettaNet.

Lower Back Pain Symptom Checker Flowchart

MedlinePlus

... Kids and Teens Pregnancy and Childbirth Women Men Seniors Your Health Resources Healthcare Management End-of-Life Issues Insurance & Bills Self Care Working With Your Doctor Drugs, Procedures & Devices Over-the- ...

Analyzing Tabular and State-Transition Requirements Specifications in PVS

NASA Technical Reports Server (NTRS)

Owre, Sam; Rushby, John; Shankar, Natarajan

1997-01-01

We describe PVS's capabilities for representing tabular specifications of the kind advocated by Parnas and others, and show how PVS's Type Correctness Conditions (TCCs) are used to ensure certain well-formedness properties. We then show how these and other capabilities of PVS can be used to represent the AND/OR tables of Leveson and the Decision Tables of Sherry, and we demonstrate how PVS's TCCs can expose and help isolate errors in the latter. We extend this approach to represent the mode transition tables of the Software Cost Reduction (SCR) method in an attractive manner. We show how PVS can check these tables for well-formedness, and how PVS's model checking capabilities can be used to verify invariants and reachability properties of SCR requirements specifications, and inclusion relations between the behaviors of different specifications. These examples demonstrate how several capabilities of the PVS language and verification system can be used in combination to provide customized support for specific methodologies for documenting and analyzing requirements. Because they use only the standard capabilities of PVS, users can adapt and extend these customizations to suit their own needs. Those developing dedicated tools for individual methodologies may find these constructions in PVS helpful for prototyping purposes, or as a useful adjunct to a dedicated tool when the capabilities of a full theorem prover are required. The examples also illustrate the power and utility of an integrated general-purpose system such as PVS. For example, there was no need to adapt or extend the PVS model checker to make it work with SCR specifications described using the PVS TABLE construct: the model checker is applicable to any transition relation, independently of the PVS language constructs used in its definition.

Genital Problems in Men

MedlinePlus

... Toddlers Kids and Teens Pregnancy and Childbirth Women Men Seniors Your Health Resources Healthcare Management End-of- ... chart for more information about genital problems in men. Our trusted Symptom Checker is written and reviewed ...

Realising the Benefits of Adopting and Adapting Existing CF Metadata Conventions to a Broader Range of Geoscience Data

NASA Astrophysics Data System (ADS)

Druken, K. A.; Trenham, C. E.; Wang, J.; Bastrakova, I.; Evans, B. J. K.; Wyborn, L. A.; Ip, A. I.; Poudjom Djomani, Y.

2016-12-01

The National Computational Infrastructure (NCI) hosts one of Australia's largest repositories (10+ PBytes) of research data, colocated with a petascale High Performance Computer and a highly integrated research cloud. Key to maximizing benefit of NCI's collections and computational capabilities is ensuring seamless interoperable access to these datasets. This presents considerable data management challenges across the diverse range of geoscience data; spanning disciplines where netCDF-CF is commonly utilized (e.g., climate, weather, remote-sensing), through to the geophysics and seismology fields that employ more traditional domain- and study-specific data formats. These data are stored in a variety of gridded, irregularly spaced (i.e., trajectories, point clouds, profiles), and raster image structures. They often have diverse coordinate projections and resolutions, thus complicating the task of comparison and inter-discipline analysis. Nevertheless, much can be learned from the netCDF-CF model that has long served the climate community, providing a common data structure for the atmospheric, ocean and cryospheric sciences. We are extending the application of the existing Climate and Forecast (CF) metadata conventions to NCI's broader geoscience data collections. We present simple implementations that can significantly improve interoperability of the research collections, particularly in the case of line survey data. NCI has developed a compliance checker to assist with the data quality across all hosted netCDF-CF collections. The tool is an extension to one of the main existing CF Convention checkers, that we have modified to incorporate the Attribute Convention for Data Discovery (ACDD) and ISO19115 standards, and to perform parallelised checks over collections of files, ensuring compliance and consistency across the NCI data collections as a whole. It is complemented by a checker that also verifies functionality against a range of scientific analysis, programming, and data visualisation tools. By design, these tests are not necessarily domain-specific, and demonstrate that verified data is accessible to end-users, thus allowing for seamless interoperability with other datasets across a wide range of fields.

Neck Swelling (Symptom Checker)

MedlinePlus

... Long-term Abdominal Pain (Stomach Pain), Short-term Ankle Problems Breast Problems in Men Breast Problems in Women Chest Pain in Infants and Children Chest Pain, Acute Chest Pain, Chronic Cold and Flu Cough Diarrhea ...

Bartholin's Gland Cyst

MedlinePlus

... Exercise at Every AgeTics and Tourette SyndromeRead Article >>Tics and Tourette Syndrome Visit our interactive symptom checker ... age. There is a place for exercise at…Tics and Tourette SyndromeRead Article >>Exercise and FitnessTics and ...

Cervical Dysplasia

MedlinePlus

... Exercise at Every AgeTics and Tourette SyndromeRead Article >>Tics and Tourette Syndrome Visit our interactive symptom checker ... age. There is a place for exercise at…Tics and Tourette SyndromeRead Article >>Exercise and FitnessTics and ...

Kidney Cysts

MedlinePlus

... Exercise at Every AgeTics and Tourette SyndromeRead Article >>Tics and Tourette Syndrome Visit our interactive symptom checker ... age. There is a place for exercise at…Tics and Tourette SyndromeRead Article >>Exercise and FitnessTics and ...

Eye Problems: Symptom Checker Flowchart

MedlinePlus

... Long-term Abdominal Pain (Stomach Pain), Short-term Ankle Problems Breast Problems in Men Breast Problems in Women Chest Pain in Infants and Children Chest Pain, Acute Chest Pain, Chronic Cold and Flu Cough Diarrhea ...

Shoulder Problems: Symptom Checker Flowchart

MedlinePlus

... Long-term Abdominal Pain (Stomach Pain), Short-term Ankle Problems Breast Problems in Men Breast Problems in Women Chest Pain in Infants and Children Chest Pain, Acute Chest Pain, Chronic Cold and Flu Cough Diarrhea ...

What Can Union Do with Its Towering, 16-Sided Victorian Masterpiece?

ERIC Educational Resources Information Center

Biemiller, Lawrence

1987-01-01

Union College's Victorian-style Nott Memorial has mysterious and intriguing architectural features, a checkered history, and serious problems of neglect and underutilization. The college must resolve its future soon. (MSE)

Puff and bite: the relationship between the glucocorticoid stress response and anti-predator performance in checkered puffer (Sphoeroides testudineus).

PubMed

Cull, Felicia; O'Connor, Constance M; Suski, Cory D; Shultz, Aaron D; Danylchuk, Andy J; Cooke, Steven J

2015-04-01

Individual variation in the endocrine stress response has been linked to survival and performance in a variety of species. Here, we evaluate the relationship between the endocrine stress response and anti-predator behaviors in wild checkered puffers (Sphoeroides testudineus) captured at Eleuthera Island, Bahamas. The checkered puffer has a unique and easily measurable predator avoidance strategy, which is to inflate or 'puff' to deter potential predators. In this study, we measured baseline and stress-induced circulating glucocorticoid levels, as well as bite force, a performance measure that is relevant to both feeding and predator defence, and 'puff' performance. We found that puff performance and bite force were consistent within individuals, but generally decreased following a standardized stressor. Larger puffers were able to generate a higher bite force, and larger puffers were able to maintain a more robust puff performance following a standardized stressor relative to smaller puffers. In terms of the relationship between the glucocorticoid stress response and performance metrics, we found no relationship between post-stress glucocorticoid levels and either puff performance or bite force. However, we did find that baseline glucocorticoid levels predicted the ability of a puffer to maintain a robust puff response following a repeated stressor, and this relationship was more pronounced in larger individuals. Our work provides a novel example of how baseline glucocorticoids can predict a fitness-related anti-predator behavior. Copyright © 2015 Elsevier Inc. All rights reserved.

Test Input Generation for Red-Black Trees using Abstraction

NASA Technical Reports Server (NTRS)

Visser, Willem; Pasareanu, Corina S.; Pelanek, Radek

2005-01-01

We consider the problem of test input generation for code that manipulates complex data structures. Test inputs are sequences of method calls from the data structure interface. We describe test input generation techniques that rely on state matching to avoid generation of redundant tests. Exhaustive techniques use explicit state model checking to explore all the possible test sequences up to predefined input sizes. Lossy techniques rely on abstraction mappings to compute and store abstract versions of the concrete states; they explore under-approximations of all the possible test sequences. We have implemented the techniques on top of the Java PathFinder model checker and we evaluate them using a Java implementation of red-black trees.

The ANMLite Language and Logic for Specifying Planning Problems

NASA Technical Reports Server (NTRS)

Butler, Ricky W.; Siminiceanu, Radu I.; Munoz, Cesar A.

2007-01-01

We present the basic concepts of the ANMLite planning language. We discuss various aspects of specifying a plan in terms of constraints and checking the existence of a solution with the help of a model checker. The constructs of the ANMLite language have been kept as simple as possible in order to reduce complexity and simplify the verification problem. We illustrate the language with a specification of the space shuttle crew activity model that was constructed under the Spacecraft Autonomy for Vehicles and Habitats (SAVH) project. The main purpose of this study was to explore the implications of choosing a robust logic behind the specification of constraints, rather than simply proposing a new planning language.

Expert system validation in prolog

NASA Technical Reports Server (NTRS)

Stock, Todd; Stachowitz, Rolf; Chang, Chin-Liang; Combs, Jacqueline

1988-01-01

An overview of the Expert System Validation Assistant (EVA) is being implemented in Prolog at the Lockheed AI Center. Prolog was chosen to facilitate rapid prototyping of the structure and logic checkers and since February 1987, we have implemented code to check for irrelevance, subsumption, duplication, deadends, unreachability, and cycles. The architecture chosen is extremely flexible and expansible, yet concise and complementary with the normal interactive style of Prolog. The foundation of the system is in the connection graph representation. Rules and facts are modeled as nodes in the graph and arcs indicate common patterns between rules. The basic activity of the validation system is then a traversal of the connection graph, searching for various patterns the system recognizes as erroneous. To aid in specifying these patterns, a metalanguage is developed, providing the user with the basic facilities required to reason about the expert system. Using the metalanguage, the user can, for example, give the Prolog inference engine the goal of finding inconsistent conclusions among the rules, and Prolog will search the graph intantiations which can match the definition of inconsistency. Examples of code for some of the checkers are provided and the algorithms explained. Technical highlights include automatic construction of a connection graph, demonstration of the use of metalanguage, the A* algorithm modified to detect all unique cycles, general-purpose stacks in Prolog, and a general-purpose database browser with pattern completion.

Meniere's Disease

MedlinePlus

... Every AgeDiabetesRead Article >>DiabetesTics and Tourette SyndromeRead Article >>Tics and Tourette Syndrome Visit our interactive symptom checker ... t make or use the hormone insulin properly.Tics and Tourette SyndromeRead Article >>Family HealthTics and Tourette ...

Sexual Dysfunction in Women

MedlinePlus

... Exercise at Every AgeTics and Tourette SyndromeRead Article >>Tics and Tourette Syndrome Visit our interactive symptom checker ... age. There is a place for exercise at…Tics and Tourette SyndromeRead Article >>Exercise and FitnessTics and ...

Bladder Stones

MedlinePlus

... Every AgeDiabetesRead Article >>DiabetesTics and Tourette SyndromeRead Article >>Tics and Tourette Syndrome Visit our interactive symptom checker ... t make or use the hormone insulin properly.Tics and Tourette SyndromeRead Article >>Family HealthTics and Tourette ...

Our Commitment to Reliable Health and Medical Information

MedlinePlus

... 000 visitors world-wide per day. HONcode Toolbar: search engine and checker of the certification status Automatically checks ... HONcode status when browsing health web sites. The search engine indexes only HONcode-certified sites. HONcodeHunt currently includes ...

Grinding patterns in migraine patients with sleep bruxism: a case-controlled study.

PubMed

Kato, Momoko; Saruta, Juri; Takeuchi, Mifumi; Sugimoto, Masahiro; Kamata, Yohei; Shimizu, Tomoko; To, Masahiro; Fuchida, Shinya; Igarashi, Hisaka; Kawata, Toshitsugu; Tsukinoki, Keiichi

2016-11-01

Details on grinding patterns and types of contact during sleep bruxism in association with migraine headache have not yet been elucidated. This study compared the characteristics of sleep bruxism between patients with migraine and controls. The study included 80 female patients who had been diagnosed with migraine and 52 women with no history of migraine. Grinding patterns were measured using the BruxChecker® (Scheu Dental, Iserlohn, Germany). There was a significant difference between the two groups in the distribution of grinding patterns at the laterotrusive side (p < 0.001). When the anterior teeth and premolar and molar regions in the two groups were compared, the proportion of the grinding area at all sites was significantly larger in the migraine group than in the control group (p < 0.001). The BruxChecker® showed that there was substantial grinding over a large area among migraine patients, particularly in the molar region.

Method and apparatus for checking fire detectors

NASA Technical Reports Server (NTRS)

Clawson, G. T. (Inventor)

1974-01-01

A fire detector checking method and device are disclosed for nondestructively verifying the operation of installed fire detectors of the type which operate on the principle of detecting the rate of temperature rise of the ambient air to sound an alarm and/or which sound an alarm when the temperature of the ambient air reaches a preset level. The fire alarm checker uses the principle of effecting a controlled simulated alarm condition to ascertain wheather or not the detector will respond. The checker comprises a hand-held instrument employing a controlled heat source, e.g., an electric lamp having a variable input, for heating at a controlled rate an enclosed mass of air in a first compartment, which air mass is then disposed about the fire detector to be checked. A second compartment of the device houses an electronic circuit to sense and adjust the temperature level and heating rate of the heat source.

Work-related symptoms and checkstand configuration: an experimental study.

PubMed

Harber, P; Bloswick, D; Luo, J; Beck, J; Greer, D; Peña, L F

1993-07-01

Supermarket checkers are known to be at risk of upper-extremity cumulative trauma disorders. Forty-two experienced checkers checked a standard "market basket" of items on an experimental checkstand. The counter height could be adjusted (high = 35.5, low = 31.5 inches), and the pre-scan queuing area length (between conveyor belt and laser scanner) could be set to "near" or "far" lengths. Each subject scanned under the high-near, high-far, low-near, and low-far conditions in random order. Seven ordinal symptom scales were used to describe comfort. Analysis showed that both counter height and queuing length had significant effects on symptoms. Furthermore, the height of the subject affected the degree and direction of the impact of the checkstand configuration differences. The study suggests that optimization of design may be experimentally evaluated, that modification of postural as well as frequency loading may be beneficial, and that adjustability for the individual may be advisable.

Software Model Checking of ARINC-653 Flight Code with MCP

NASA Technical Reports Server (NTRS)

Thompson, Sarah J.; Brat, Guillaume; Venet, Arnaud

2010-01-01

The ARINC-653 standard defines a common interface for Integrated Modular Avionics (IMA) code. In particular, ARINC-653 Part 1 specifies a process- and partition-management API that is analogous to POSIX threads, but with certain extensions and restrictions intended to support the implementation of high reliability flight code. MCP is a software model checker, developed at NASA Ames, that provides capabilities for model checking C and C++ source code. In this paper, we present recent work aimed at implementing extensions to MCP that support ARINC-653, and we discuss the challenges and opportunities that consequentially arise. Providing support for ARINC-653 s time and space partitioning is nontrivial, though there are implicit benefits for partial order reduction possible as a consequence of the API s strict interprocess communication policy.

Swarm Verification

NASA Technical Reports Server (NTRS)

Holzmann, Gerard J.; Joshi, Rajeev; Groce, Alex

2008-01-01

Reportedly, supercomputer designer Seymour Cray once said that he would sooner use two strong oxen to plow a field than a thousand chickens. Although this is undoubtedly wise when it comes to plowing a field, it is not so clear for other types of tasks. Model checking problems are of the proverbial "search the needle in a haystack" type. Such problems can often be parallelized easily. Alas, none of the usual divide and conquer methods can be used to parallelize the working of a model checker. Given that it has become easier than ever to gain access to large numbers of computers to perform even routine tasks it is becoming more and more attractive to find alternate ways to use these resources to speed up model checking tasks. This paper describes one such method, called swarm verification.

Potential Drug-Drug Interactions among Patients prescriptions collected from Medicine Out-patient Setting.

PubMed

Farooqui, Riffat; Hoor, Talea; Karim, Nasim; Muneer, Mehtab

2018-01-01

To identify and evaluate the frequency, severity, mechanism and common pairs of drug-drug interactions (DDIs) in prescriptions by consultants in medicine outpatient department. This cross sectional descriptive study was done by Pharmacology department of Bahria University Medical & Dental College (BUMDC) in medicine outpatient department (OPD) of a private hospital in Karachi from December 2015 to January 2016. A total of 220 prescriptions written by consultants were collected. Medications given with patient's diagnosis were recorded. Drugs were analyzed for interactions by utilizing Medscape drug interaction checker, drugs.com checker and stockley`s drug interactions index. Two hundred eleven prescriptions were selected while remaining were excluded from the study because of unavailability of the prescribed drugs in the drug interaction checkers. In 211 prescriptions, two common diagnoses were diabetes mellitus (28.43%) and hypertension (27.96%). A total of 978 medications were given. Mean number of medications per prescription was 4.6. A total of 369 drug-drug interactions were identified in 211 prescriptions (175%). They were serious 4.33%, significant 66.12% and minor 29.53%. Pharmacokinetic and pharmacodynamic interactions were 37.94% and 51.21% respectively while 10.84% had unknown mechanism. Number wise common pairs of DDIs were Omeprazole-Losartan (S), Gabapentine- Acetaminophen (M), Losartan-Diclofenac (S). The frequency of DDIs is found to be too high in prescriptions of consultants from medicine OPD of a private hospital in Karachi. Significant drug-drug interactions were more and mostly caused by Pharmacodynamic mechanism. Number wise evaluation showed three common pairs of drugs involved in interactions.

Development and preliminary data on the use of a mobile app specifically designed to increase community awareness of invasive pneumococcal disease and its prevention.

PubMed

Panatto, Donatella; Domnich, Alexander; Gasparini, Roberto; Bonanni, Paolo; Icardi, Giancarlo; Amicizia, Daniela; Arata, Lucia; Bragazzi, Nicola Luigi; Signori, Alessio; Landa, Paolo; Bechini, Angela; Boccalini, Sara

2016-04-02

Given the growing use and great potential of mobile apps, this project aimed to develop and implement a user-friendly app to increase laypeople's knowledge and awareness of invasive pneumococcal disease (IPD). Despite the heavy burden of IPD, the documented low awareness of IPD among both laypeople and healthcare professionals and far from optimal pneumococcal vaccination coverage, no app specifically targeting IPD has been developed so far. The app was designed to be maximally functional and conceived in accordance with user-centered design. Its content, layout and usability were discussed and formally tested during several workshops that involved the principal stakeholders, including experts in IPD and information technology and potential end-users. Following several workshops, it was decided that, in order to make the app more interactive, its core should be a personal "checker" of the risk of contracting IPD and a user-friendly risk-communication strategy. The checker was populated with risk factors identified through both Italian and international official guidelines. Formal evaluation of the app revealed its good readability and usability properties. A sister web site with the same content was created to achieve higher population exposure. Seven months after being launched in a price- and registration-free modality, the app, named "Pneumo Rischio," averaged 20.9 new users/day and 1.3 sessions/user. The first in-field results suggest that "Pneumo Rischio" is a promising tool for increasing the population's awareness of IPD and its prevention through a user-friendly risk checker.

Potential Drug-Drug Interactions among Patients prescriptions collected from Medicine Out-patient Setting

PubMed Central

Farooqui, Riffat; Hoor, Talea; Karim, Nasim; Muneer, Mehtab

2018-01-01

Objective: To identify and evaluate the frequency, severity, mechanism and common pairs of drug-drug interactions (DDIs) in prescriptions by consultants in medicine outpatient department. Methods: This cross sectional descriptive study was done by Pharmacology department of Bahria University Medical & Dental College (BUMDC) in medicine outpatient department (OPD) of a private hospital in Karachi from December 2015 to January 2016. A total of 220 prescriptions written by consultants were collected. Medications given with patient's diagnosis were recorded. Drugs were analyzed for interactions by utilizing Medscape drug interaction checker, drugs.com checker and stockley`s drug interactions index. Two hundred eleven prescriptions were selected while remaining were excluded from the study because of unavailability of the prescribed drugs in the drug interaction checkers. Results: In 211 prescriptions, two common diagnoses were diabetes mellitus (28.43%) and hypertension (27.96%). A total of 978 medications were given. Mean number of medications per prescription was 4.6. A total of 369 drug-drug interactions were identified in 211 prescriptions (175%). They were serious 4.33%, significant 66.12% and minor 29.53%. Pharmacokinetic and pharmacodynamic interactions were 37.94% and 51.21% respectively while 10.84% had unknown mechanism. Number wise common pairs of DDIs were Omeprazole-Losartan (S), Gabapentine- Acetaminophen (M), Losartan-Diclofenac (S). Conclusion: The frequency of DDIs is found to be too high in prescriptions of consultants from medicine OPD of a private hospital in Karachi. Significant drug-drug interactions were more and mostly caused by Pharmacodynamic mechanism. Number wise evaluation showed three common pairs of drugs involved in interactions. PMID:29643896

Efficient micromagnetic modelling of spin-transfer torque and spin-orbit torque

NASA Astrophysics Data System (ADS)

Abert, Claas; Bruckner, Florian; Vogler, Christoph; Suess, Dieter

2018-05-01

While the spin-diffusion model is considered one of the most complete and accurate tools for the description of spin transport and spin torque, its solution in the context of dynamical micromagnetic simulations is numerically expensive. We propose a procedure to retrieve the free parameters of a simple macro-spin like spin-torque model through the spin-diffusion model. In case of spin-transfer torque the simplified model complies with the model of Slonczewski. A similar model can be established for the description of spin-orbit torque. In both cases the spin-diffusion model enables the retrieval of free model parameters from the geometry and the material parameters of the system. Since these parameters usually have to be determined phenomenologically through experiments, the proposed method combines the strength of the diffusion model to resolve material parameters and geometry with the high performance of simple torque models.

From Verified Models to Verifiable Code

NASA Technical Reports Server (NTRS)

Lensink, Leonard; Munoz, Cesar A.; Goodloe, Alwyn E.

2009-01-01

Declarative specifications of digital systems often contain parts that can be automatically translated into executable code. Automated code generation may reduce or eliminate the kinds of errors typically introduced through manual code writing. For this approach to be effective, the generated code should be reasonably efficient and, more importantly, verifiable. This paper presents a prototype code generator for the Prototype Verification System (PVS) that translates a subset of PVS functional specifications into an intermediate language and subsequently to multiple target programming languages. Several case studies are presented to illustrate the tool's functionality. The generated code can be analyzed by software verification tools such as verification condition generators, static analyzers, and software model-checkers to increase the confidence that the generated code is correct.

Pinus ponderosa : A checkered past obscured four species

Treesearch

Ann Willyard; David S. Gernandt; Kevin Potter; Valerie Hipkins; Paula E. Marquardt; Mary Frances Mahalovich; Stephen K. Langer; Frank W. Telewski; Blake Cooper; Connor Douglas; Kristen Finch; Hassani H. Karemera; Julia Lefler; Payton Lea; Austin Wofford

2016-01-01

PREMISE OF THE STUDY: Molecular genetic evidence can help delineate taxa in species complexes that lack diagnostic morphological characters. Pinus ponderosa (Pinaceae; subsection Ponderosae ) is recognized as a problematic taxon: plastid phylogenies of exemplars were paraphyletic, and mitochondrial phylogeography suggested at...

Assume-Guarantee Abstraction Refinement Meets Hybrid Systems

NASA Technical Reports Server (NTRS)

Bogomolov, Sergiy; Frehse, Goran; Greitschus, Marius; Grosu, Radu; Pasareanu, Corina S.; Podelski, Andreas; Strump, Thomas

2014-01-01

Compositional verification techniques in the assume- guarantee style have been successfully applied to transition systems to efficiently reduce the search space by leveraging the compositional nature of the systems under consideration. We adapt these techniques to the domain of hybrid systems with affine dynamics. To build assumptions we introduce an abstraction based on location merging. We integrate the assume-guarantee style analysis with automatic abstraction refinement. We have implemented our approach in the symbolic hybrid model checker SpaceEx. The evaluation shows its practical potential. To the best of our knowledge, this is the first work combining assume-guarantee reasoning with automatic abstraction-refinement in the context of hybrid automata.

Generating Test Templates via Automated Theorem Proving

NASA Technical Reports Server (NTRS)

Kancherla, Mani Prasad

1997-01-01

Testing can be used during the software development process to maintain fidelity between evolving specifications, program designs, and code implementations. We use a form of specification-based testing that employs the use of an automated theorem prover to generate test templates. A similar approach was developed using a model checker on state-intensive systems. This method applies to systems with functional rather than state-based behaviors. This approach allows for the use of incomplete specifications to aid in generation of tests for potential failure cases. We illustrate the technique on the cannonical triangle testing problem and discuss its use on analysis of a spacecraft scheduling system.

A spin exchange model for singlet fission

NASA Astrophysics Data System (ADS)

Yago, Tomoaki; Wakasa, Masanobu

2018-03-01

Singlet fission has been analyzed with the Dexter model in which electron exchange occurs between chromophores, conserving the spin for each electron. In the present study, we propose a spin exchange model for singlet fission. In the spin exchange model, spins are exchanged by the exchange interaction between two electrons. Our analysis with simple spin functions demonstrates that singlet fission is possible by spin exchange. A necessary condition for spin exchange is a variation in exchange interactions. We also adapt the spin exchange model to triplet fusion and triplet energy transfer, which often occur after singlet fission in organic solids.

Algebraic model checking for Boolean gene regulatory networks.

PubMed

Tran, Quoc-Nam

2011-01-01

We present a computational method in which modular and Groebner bases (GB) computation in Boolean rings are used for solving problems in Boolean gene regulatory networks (BN). In contrast to other known algebraic approaches, the degree of intermediate polynomials during the calculation of Groebner bases using our method will never grow resulting in a significant improvement in running time and memory space consumption. We also show how calculation in temporal logic for model checking can be done by means of our direct and efficient Groebner basis computation in Boolean rings. We present our experimental results in finding attractors and control strategies of Boolean networks to illustrate our theoretical arguments. The results are promising. Our algebraic approach is more efficient than the state-of-the-art model checker NuSMV on BNs. More importantly, our approach finds all solutions for the BN problems.

Electronic prescribing system design priorities for antimicrobial stewardship: a cross-sectional survey of 142 UK infection specialists.

PubMed

Hand, Kieran S; Cumming, Debbie; Hopkins, Susan; Ewings, Sean; Fox, Andy; Theminimulle, Sandya; Porter, Robert J; Parker, Natalie; Munns, Joanne; Sheikh, Adel; Keyser, Taryn; Puleston, Richard

2017-04-01

The implementation of electronic prescribing and medication administration (EPMA) systems is a priority for hospitals and a potential component of antimicrobial stewardship (AMS). To identify software features within EPMA systems that could potentially facilitate AMS and to survey practising UK infection specialist healthcare professionals in order to assign priority to these software features. A questionnaire was developed using nominal group technique and transmitted via email links through professional networks. The questionnaire collected demographic data, information on priority areas and anticipated impact of EPMA. Responses from different respondent groups were compared using the Mann-Whitney U -test. Responses were received from 164 individuals (142 analysable). Respondents were predominantly specialist infection pharmacists (48%) or medical microbiologists (37%). Of the pharmacists, 59% had experience of EPMA in their hospitals compared with 35% of microbiologists. Pharmacists assigned higher priority to indication prompt ( P  <   0.001), allergy checker ( P  =   0.003), treatment protocols ( P  =   0.003), drug-indication mismatch alerts ( P  =   0.031) and prolonged course alerts ( P  =   0.041) and lower priority to a dose checker for adults ( P  =   0.02) and an interaction checker ( P  <   0.05) than microbiologists. A 'soft stop' functionality was rated essential or high priority by 89% of respondents. Potential EPMA software features were expected to have the greatest impact on stewardship, treatment efficacy and patient safety outcomes with lowest impact on Clostridium difficile infection, antimicrobial resistance and drug expenditure. The survey demonstrates key differences in health professionals' opinions of potential healthcare benefits of EPMA, but a consensus of anticipated positive impact on patient safety and AMS. © The Author 2016. Published by Oxford University Press on behalf of the British Society for Antimicrobial Chemotherapy. All rights reserved. For Permissions, please email: journals.permissions@oup.com.

Playing checkers: detection and eye hand coordination in simulated prosthetic vision

NASA Astrophysics Data System (ADS)

Dagnelie, Gislin; Walter, Matthias; Yang, Liancheng

2006-09-01

In order to assess the potential for visual inspection and eye hand coordination without tactile feedback under conditions that may be available to future retinal prosthesis wearers, we studied the ability of sighted individuals to act upon pixelized visual information at very low resolution, equivalent to 20/2400 visual acuity. Live images from a head-mounted camera were low-pass filtered and presented in a raster of 6 × 10 circular Gaussian dots. Subjects could either freely move their gaze across the raster (free-viewing condition) or the raster position was locked to the subject's gaze by means of video-based pupil tracking (gaze-locked condition). Four normally sighted and one severely visually impaired subject with moderate nystagmus participated in a series of four experiments. Subjects' task was to count 1 to 16 white fields randomly distributed across an otherwise black checkerboard (counting task) or to place a black checker on each of the white fields (placing task). We found that all subjects were capable of learning both tasks after varying amounts of practice, both in the free-viewing and in the gaze-locked conditions. Normally sighted subjects all reached very similar performance levels independent of the condition. The practiced performance level of the visually impaired subject in the free-viewing condition was indistinguishable from that of the normally sighted subjects, but required approximately twice the amount of time to place checkers in the gaze-locked condition; this difference is most likely attributable to this subject's nystagmus. Thus, if early retinal prosthesis wearers can achieve crude form vision, then on the basis of these results they too should be able to perform simple eye hand coordination tasks without tactile feedback.

The checkered puffer (Spheroides testudineus) and its helminths as bioindicators of chemical pollution in Yucatan coastal lagoons.

PubMed

Pech, Daniel; Vidal-Martínez, Víctor M; Aguirre-Macedo, M Leopoldina; Gold-Bouchot, Gerardo; Herrera-Silveira, Jorge; Zapata-Pérez, Omar; Marcogliese, David J

2009-03-15

The suitability of using helminth communities as bioindicators of environmental quality of the Yucatan coastal lagoons status was tested on the checkered puffer (Spheroides testudineus) in four coastal lagoons along the Yucatan coast. The concentration of chemical pollutants in sediments, water quality parameters, helminth infracommunity characteristics, as well as fish physiological biomarkers, including EROD (7-ethoxyresorufin-O-deethylase) and catalase activities, were measured. Results from sediment analyses demonstrated the presence of hydrocarbons, organochlorine pesticides and polychlorinated biphenyls at varying concentrations, some of which exceeded the Probability Effect Level (PEL). Significant negative associations among organochlorine pesticides, infracommunity characteristics and fish physiological responses were observed in most of the lagoons. Results suggest that EROD activity and parasite infracommunity characteristics could be useful tools to evaluate the effects of chemical pollutants on the fish host and in the environment. Importantly, certain parasites appear to influence biomarker measurements, indicating that parasites should be considered in ecotoxicological studies.

New Spin Foam Models of Quantum Gravity

NASA Astrophysics Data System (ADS)

Miković, A.

We give a brief and a critical review of the Barret-Crane spin foam models of quantum gravity. Then we describe two new spin foam models which are obtained by direct quantization of General Relativity and do not have some of the drawbacks of the Barret-Crane models. These are the model of spin foam invariants for the embedded spin networks in loop quantum gravity and the spin foam model based on the integration of the tetrads in the path integral for the Palatini action.

Style and Usage Software: Mentor, not Judge.

ERIC Educational Resources Information Center

Smye, Randy

Computer software style and usage checkers can encourage students' recursive revision strategies. For example, HOMER is based on the revision pedagogy presented in Richard Lanham's "Revising Prose," while Grammatik II focuses on readability, passive voice, and possibly misused words or phrases. Writer's Workbench "Style" (a UNIX program) provides…

22 CFR Appendix E to Part 62 - Unskilled Occupations

Code of Federal Regulations, 2011 CFR

2011-04-01

... Cleaners (10) Chauffeurs and Taxicab Drivers (11) Cleaners, Hotel and Motel (12) Clerks, General (13) Clerks, Hotel (14) Clerks and Checkers, Grocery Stores (15) Clerk Typist (16) Cooks, Short Order (17... Operators (21) Floorworkers (22) Groundskeepers (23) Guards (24) Helpers, any industry (25) Hotel Cleaners...

What Schools Are Doing. A Roundup of New and Unusual School Practices

ERIC Educational Resources Information Center

Nation's Schools, 1972

1972-01-01

Describes a teen-run cafeteria, a program of giving away obsolete texts, a short term investment plan (a programed approach to cash-flow budgeting), an emergency credit'' plan whereby teachers can acquire credit hours outside school, and an automated attendance checker system. (DN)

Student Online Plagiarism: How Do We Respond?

ERIC Educational Resources Information Center

Scanlon, Patrick M.

2003-01-01

The perception that Internet plagiarism by university students is on the rise has alarmed college teachers, leading to the adoption of electronic plagiarism checkers, among other responses. Although some recent studies suggest that estimates of online plagiarism may be exaggerated, cause for concern remains. This article reviews quantitative…

Choosing the Right Database Management Program.

ERIC Educational Resources Information Center

Vockell, Edward L.; Kopenec, Donald

1989-01-01

Provides a comparison of four database management programs commonly used in schools: AppleWorks, the DOS 3.3 and ProDOS versions of PFS, and MECC's Data Handler. Topics discussed include information storage, spelling checkers, editing functions, search strategies, graphs, printout formats, library applications, and HyperCard. (LRW)

A three-dimensional spin-diffusion model for micromagnetics

PubMed Central

Abert, Claas; Ruggeri, Michele; Bruckner, Florian; Vogler, Christoph; Hrkac, Gino; Praetorius, Dirk; Suess, Dieter

2015-01-01

We solve a time-dependent three-dimensional spin-diffusion model coupled to the Landau-Lifshitz-Gilbert equation numerically. The presented model is validated by comparison to two established spin-torque models: The model of Slonzewski that describes spin-torque in multi-layer structures in the presence of a fixed layer and the model of Zhang and Li that describes current driven domain-wall motion. It is shown that both models are incorporated by the spin-diffusion description, i.e., the nonlocal effects of the Slonzewski model are captured as well as the spin-accumulation due to magnetization gradients as described by the model of Zhang and Li. Moreover, the presented method is able to resolve the time dependency of the spin-accumulation. PMID:26442796

Thermal properties of spin-S Kitaev-Heisenberg model on a honeycomb lattice

NASA Astrophysics Data System (ADS)

Suzuki, Takafumi; Yamaji, Youhei

2018-05-01

Temperature (T) dependence of heat capacity C (T) in the S = 1 / 2 Kitaev honeycomb model shows a double-peak structure resulting from fractionalization of spins into two kinds of Majorana fermions. Recently it has been discussed that the double-peak structure in C (T) is also observed in magnetic ordered phases of the S = 1 / 2 Kitaev-Heisenberg (KH) model on a honeycomb lattice when the system is located in the vicinity of the Kitaev's spin liquid phase. In addition to the S = 1 / 2 spin case, similar double-peak structure has been confirmed in the KH honeycomb model for classical Heisenberg spins, where spin S is regarded as S → ∞ . We investigate spin-S dependence of C (T) for the KH honeycomb models by using thermal pure quantum state. We also perform classical Monte Carlo calculations to obtain C (T) for the classical KH model. From obtained results, we find that the origin of the high-temperature peak is different between the quantum spin case with small Ss and the classical Heisenberg spin case. Furthermore, the high-temperature peak in the quantum spin case, which is one of the clues for fractionalization of spins, disappears for S > 1 .

Do physical habitat complexity and predator cues influence the baseline and stress-induced glucocorticoid levels of a mangrove-associated fish?

PubMed

Magel, Jennifer M T; Pleizier, Naomi; Wilson, Alexander D M; Shultz, Aaron D; Vera Chang, Marilyn N; Moon, Thomas W; Cooke, Steven J

2017-01-01

As human populations continue to expand, increases in coastal development have led to the alteration of much of the world's mangrove habitat, creating problems for the multitude of species that inhabit these unique ecosystems. Habitat alteration often leads to changes in habitat complexity and predation risk, which may serve as additional stressors for those species that rely on mangroves for protection from predators. However, few studies have been conducted to date to assess the effects of these specific stressors on glucocorticoid (GC) stress hormone levels in wild fish populations. Using the checkered puffer as a model, our study sought to examine the effects of physical habitat complexity and predator environment on baseline and acute stress-induced GC levels. This was accomplished by examining changes in glucose and cortisol concentrations of fish placed in artificial environments for short periods (several hours) where substrate type and the presence of mangrove roots and predator cues were manipulated. Our results suggest that baseline and stress-induced GC levels are not significantly influenced by changes in physical habitat complexity or the predator environment using the experimental protocol that we applied. Although more research is required, the current study suggests that checkered puffers may be capable of withstanding changes in habitat complexity and increases in predation risk without experiencing adverse GC-mediated physiological effects, possibly as a result of the puffers' unique morphological and chemical defenses that help them to avoid predation in the wild. Copyright © 2016 Elsevier Inc. All rights reserved.

Testing Linear Temporal Logic Formulae on Finite Execution Traces

NASA Technical Reports Server (NTRS)

Havelund, Klaus; Rosu, Grigore; Norvig, Peter (Technical Monitor)

2001-01-01

We present an algorithm for efficiently testing Linear Temporal Logic (LTL) formulae on finite execution traces. The standard models of LTL are infinite traces, reflecting the behavior of reactive and concurrent systems which conceptually may be continuously alive. In most past applications of LTL. theorem provers and model checkers have been used to formally prove that down-scaled models satisfy such LTL specifications. Our goal is instead to use LTL for up-scaled testing of real software applications. Such tests correspond to analyzing the conformance of finite traces against LTL formulae. We first describe what it means for a finite trace to satisfy an LTL property. We then suggest an optimized algorithm based on transforming LTL formulae. The work is done using the Maude rewriting system. which turns out to provide a perfect notation and an efficient rewriting engine for performing these experiments.

Compilation of Test Data on 111 Free-Spinning Airplane Models Tested in the Langley 15-Foot and 20-Foot Free-Spinning Tunnels

NASA Technical Reports Server (NTRS)

Malvestuto, Frank S.; Gale, Lawrence J.; Wood, John H.

1947-01-01

A compilation of free-spinning-airplane model data on the spin and recovery characteristics of 111 airplanes is presented. These data were previously published in separate memorandum reports and were obtained from free-spinning tests in the Langley 15-foot and the Langley 20-foot free-spinning tunnels. The model test data presented include the steady-spin and recovery characteristics of each model for various combinations of aileron and elevator deflections and for various loadings and dimensional configurations. Dimensional data, mass data, and a three-view drawing of the corresponding free-spinning tunnel model are also presented for each airplane. The data presented should be of value to designers and should facilitate the design of airplanes incorporating satisfactory spin-recovery characteristics.

Property Specification Patterns for intelligence building software

NASA Astrophysics Data System (ADS)

Chun, Seungsu

2018-03-01

In this paper, through the property specification pattern research for Modal MU(μ) logical aspects present a single framework based on the pattern of intelligence building software. In this study, broken down by state property specification pattern classification of Dwyer (S) and action (A) and was subdivided into it again strong (A) and weaknesses (E). Through these means based on a hierarchical pattern classification of the property specification pattern analysis of logical aspects Mu(μ) was applied to the pattern classification of the examples used in the actual model checker. As a result, not only can a more accurate classification than the existing classification systems were easy to create and understand the attributes specified.

Game Board Artists.

ERIC Educational Resources Information Center

Szekely, George

2000-01-01

Explores children's fascination with creating their own unique games as an art form. Focuses on different games, such as chess, checkers, pogs, and monopoly. States that observing children playing games offers a firsthand lesson in how children create. Discusses what it means to be an art teacher who promotes creative play with games. (CMK)

Federal Workplace Literacy Project. Internal Evaluation Report.

ERIC Educational Resources Information Center

Matuszak, David J.

This report describes the following components of the Nestle Workplace Literacy Project: six job task analyses, curricula for six workplace basic skills training programs, delivery of courses using these curricula, and evaluation of the process. These six job categories were targeted for training: forklift loader/checker, BB's processing systems…

Logic and Simulation.

ERIC Educational Resources Information Center

Straumanis, Joan

A major problem in teaching symbolic logic is that of providing individualized and early feedback to students who are learning to do proofs. To overcome this difficulty, a computer program was developed which functions as a line-by-line proof checker in Sentential Calculus. The program, DEMON, first evaluates any statement supplied by the student…

Device-Enabled Authorization in the Grey System

DTIC Science & Technology

2005-02-01

proof checker. Journal of Automated Reasoning 31(3-4):231–260, 2003. [7] D. Balfanz , D. Dean, and M. Spreitzer. A security infrastructure for...distributed Java applications. In Proceedings of the 21st IEEE Symposium on Security and Privacy, May 2002. [8] D. Balfanz and E. Felten. Hand-held computers

Hoosier Lawmaker? Vouchers, ALEC Legislative Puppets, and Indiana's Abdication of Democracy

ERIC Educational Resources Information Center

Shaffer, Michael B.; Ellis, John G.; Swensson, Jeff

2018-01-01

"Getting poor kids out of failing schools" sounds like an altruistic cause most Americans support. However, one policy mechanism utilized to achieve that result, parental choice vouchers, has a checkered past. This descriptive analysis explores the policy-bubble created when state legislators eschewed their constitutional responsibility…

Improving ESL Writing Using an Online Formulaic Sequence Word-Combination Checker

ERIC Educational Resources Information Center

Grami, G. M. A.; Alkazemi, B. Y.

2016-01-01

Writing correct English sentences can be challenging. Furthermore, writing correct formulaic sequences can be especially difficult because accepted combinations do not follow clear rules governing which words appear together in a sequence. One solution is to provide examples of correct usage accompanied by statistical feedback from web-based…

Computer Language Settings and Canadian Spellings

ERIC Educational Resources Information Center

Shuttleworth, Roger

2011-01-01

The language settings used on personal computers interact with the spell-checker in Microsoft Word, which directly affects the flagging of spellings that are deemed incorrect. This study examined the language settings of personal computers owned by a group of Canadian university students. Of 21 computers examined, only eight had their Windows…

Troublemaker: The Education of Chester Finn

ERIC Educational Resources Information Center

Finn, Chester E., Jr.

2008-01-01

"Troublemaker," the memoir of "Education Next" senior editor and veteran education reformer Chester E. "Checker" Finn Jr., weaves into the chronicle of Finn's life and career the broader history of education reform, in which he has played a vital and sometimes rambunctious role. Currently president of the Thomas B.…

Writing Conferences Using the Microcomputer.

ERIC Educational Resources Information Center

Pufahl, John

1986-01-01

Describes a teaching strategy using Apple IIe computers in a sequence of individual conferences. Includes asking questions while scrolling through the paper, showing students how to elaborate ideas by entering suggested changes and prompts in capital letters during the conference, and using a spelling checker to prompt revision (e.g., by compiling…

Universality and phase diagrams of the Baxter-Wu Model in a Crystal Field: spin-1 and spin-3/2

NASA Astrophysics Data System (ADS)

Dias, D. A.; Xavier, J. C.; Plascak, J. A.

2017-11-01

Conventional finite-size scaling and conformal invariance theory are used in order to study the critical behavior of the spin-1 and spin-3/2 Baxter-Wu model. For spin-1 the results are similar to the Blume-Capel model. However, for spin-3/2, the phase diagram is much richer, and presents, besides a pentacritical point, an additional multicritical endpoint. In both cases, the universality class is the same as the spin-1/2 model, even at the multicritical points.

Correlation study of theoretical and experimental results for spin tests of a 1/10 scale radio control model

NASA Technical Reports Server (NTRS)

Bihrle, W., Jr.

1976-01-01

A correlation study was conducted to determine the ability of current analytical spin prediction techniques to predict the flight motions of a current fighter airplane configuration during the spin entry, the developed spin, and the spin recovery motions. The airplane math model used aerodynamics measured on an exact replica of the flight test model using conventional static and forced-oscillation wind-tunnel test techniques and a recently developed rotation-balance test apparatus capable of measuring aerodynamics under steady spinning conditions. An attempt was made to predict the flight motions measured during stall/spin flight testing of an unpowered, radio-controlled model designed to be a 1/10 scale, dynamically-scaled model of a current fighter configuration. Comparison of the predicted and measured flight motions show that while the post-stall and spin entry motions were not well-predicted, the developed spinning motion (a steady flat spin) and the initial phases of the spin recovery motion are reasonably well predicted.

Compositional schedulability analysis of real-time actor-based systems.

PubMed

Jaghoori, Mohammad Mahdi; de Boer, Frank; Longuet, Delphine; Chothia, Tom; Sirjani, Marjan

2017-01-01

We present an extension of the actor model with real-time, including deadlines associated with messages, and explicit application-level scheduling policies, e.g.,"earliest deadline first" which can be associated with individual actors. Schedulability analysis in this setting amounts to checking whether, given a scheduling policy for each actor, every task is processed within its designated deadline. To check schedulability, we introduce a compositional automata-theoretic approach, based on maximal use of model checking combined with testing. Behavioral interfaces define what an actor expects from the environment, and the deadlines for messages given these assumptions. We use model checking to verify that actors match their behavioral interfaces. We extend timed automata refinement with the notion of deadlines and use it to define compatibility of actor environments with the behavioral interfaces. Model checking of compatibility is computationally hard, so we propose a special testing process. We show that the analyses are decidable and automate the process using the Uppaal model checker.

Specification and Verification of Web Applications in Rewriting Logic

NASA Astrophysics Data System (ADS)

Alpuente, María; Ballis, Demis; Romero, Daniel

This paper presents a Rewriting Logic framework that formalizes the interactions between Web servers and Web browsers through a communicating protocol abstracting HTTP. The proposed framework includes a scripting language that is powerful enough to model the dynamics of complex Web applications by encompassing the main features of the most popular Web scripting languages (e.g. PHP, ASP, Java Servlets). We also provide a detailed characterization of browser actions (e.g. forward/backward navigation, page refresh, and new window/tab openings) via rewrite rules, and show how our models can be naturally model-checked by using the Linear Temporal Logic of Rewriting (LTLR), which is a Linear Temporal Logic specifically designed for model-checking rewrite theories. Our formalization is particularly suitable for verification purposes, since it allows one to perform in-depth analyses of many subtle aspects related to Web interaction. Finally, the framework has been completely implemented in Maude, and we report on some successful experiments that we conducted by using the Maude LTLR model-checker.

Experimental Evaluation of a Planning Language Suitable for Formal Verification

NASA Technical Reports Server (NTRS)

Butler, Rick W.; Munoz, Cesar A.; Siminiceanu, Radu I.

2008-01-01

The marriage of model checking and planning faces two seemingly diverging alternatives: the need for a planning language expressive enough to capture the complexity of real-life applications, as opposed to a language simple, yet robust enough to be amenable to exhaustive verification and validation techniques. In an attempt to reconcile these differences, we have designed an abstract plan description language, ANMLite, inspired from the Action Notation Modeling Language (ANML) [17]. We present the basic concepts of the ANMLite language as well as an automatic translator from ANMLite to the model checker SAL (Symbolic Analysis Laboratory) [7]. We discuss various aspects of specifying a plan in terms of constraints and explore the implications of choosing a robust logic behind the specification of constraints, rather than simply propose a new planning language. Additionally, we provide an initial assessment of the efficiency of model checking to search for solutions of planning problems. To this end, we design a basic test benchmark and study the scalability of the generated SAL models in terms of plan complexity.

Free-Spinning-Tunnel Investigation to Determine the Effect of Spin-Recovery Rockets and Thrust Simulation on the Recovery Characteristics of a 1/21-Scale Model of the Chance Vought F7U-3 Airplane, TED No. NACA AD 3103

NASA Technical Reports Server (NTRS)

Burk, Sanger H., Jr.; Healy, Frederick M.

1955-01-01

An investigation of a l/21-scale model of the Chance Vought F7U-3 airplane in the co&at-load- condition has been conducted in the Langley 20-foot free-spinning tunnel, The recovery characteristics of the model were determined by use of spin-recovery rockets for the erect and inverted spinning condition. The rockets were so placed as to provide either a yawing or rolling moment about the model center of gravity. Also included in the investigation were tests to determine the effect of simulated engine thrust on the recovery characteristics of the model. On the basis of model tests, recoveries from erect and inverted spins were satisfactory when a yawing moment of 22,200 foot-pounds (full scale) was provided against the spin by rockets attached to the wing tips; the anti-spin yawing moment was applied for approximately 9 seconds, (full scale). Satisfactory recoveries were obtained from erect spins when a rolling moment of 22,200 foot-pounds (full scale) was provided with the spin (rolls right wing down in right spin). Although the inverted spin was satisfactorily terminated when a rolling moment of equal magnitude was provided, a roll rocket was not considered to be an optimum spin-recovery device to effect recoveries from inverted spins for this airplane because of resulting gyrations during spin recovery. Simulation of engine thrust had no apparent effect on the spin recovery characteristics.

Lattice spin models for non-Abelian chiral spin liquids

DOE PAGES

Lecheminant, P.; Tsvelik, A. M.

2017-04-26

Here, we suggest a class of two-dimensional lattice spin Hamiltonians describing non-Abelian SU(2) chiral spin liquids—spin analogs of fractional non-Abelian quantum Hall states—with gapped bulk and gapless chiral edge excitations described by the SU(2) n Wess-Zumino-Novikov-Witten conformal field theory. The models are constructed from an array of generalized spin-n/2 ladders with multi-spin-exchange interactions which are coupled by isolated spins. Such models allow a controllable analytic treatment starting from the one-dimensional limit and are characterized by a bulk gap and non-Abelian SU(2) n gapless edge excitations.

Critical behavior of the spin-1 and spin-3/2 Baxter-Wu model in a crystal field.

PubMed

Dias, D A; Xavier, J C; Plascak, J A

2017-01-01

The phase diagram and the critical behavior of the spin-1 and the spin-3/2 two-dimensional Baxter-Wu model in a crystal field are studied by conventional finite-size scaling and conformal invariance theory. The phase diagram of this model, for the spin-1 case, is qualitatively the same as those of the diluted 4-states Potts model and the spin-1 Blume-Capel model. However, for the present case, instead of a tricritical point one has a pentacritical point for a finite value of the crystal field, in disagreement with previous work based on finite-size calculations. On the other hand, for the spin-3/2 case, the phase diagram is much richer and can present, besides a pentacritical point, an additional multicritical end point. Our results also support that the universality class of the critical behavior of the spin-1 and spin-3/2 Baxter-Wu model in a crystal field is the same as the pure Baxter-Wu model, even at the multicritical points.

Immunotherapy for glioblastoma: playing chess, not checkers.

PubMed

Jackson, Christopher M; Lim, Michael

2018-04-24

Patients with glioblastoma (GBM) exhibit a complex state of immune dysfunction involving multiple mechanisms of local, regional, and systemic immune suppression and tolerance. These pathways are now being identified and their relative contributions explored. Delineating how these pathways are interrelated is paramount to effectively implementing immunotherapy for GBM. Copyright ©2018, American Association for Cancer Research.

Checking the Grammar Checker: Integrating Grammar Instruction with Writing.

ERIC Educational Resources Information Center

McAlexander, Patricia J.

2000-01-01

Notes Rei Noguchi's recommendation of integrating grammar instruction with writing instruction and teaching only the most vital terms and the most frequently made errors. Presents a project that provides a review of the grammar lessons, applies many grammar rules specifically to the students' writing, and teaches students the effective use of the…

Food Marketing: Cashier-Checker. Student Material. Competency Based Curriculum.

ERIC Educational Resources Information Center

Froelich, Larry; And Others

This curriculum for food marketing (cashier-checking) is designed to provide entry-level employment skills. It is organized into 13 units which contain one to ten competencies. A student competency sheet provided for each competency is organized into this format: unit and competency number and name, learning steps, learning activities, and…

The Use of Board Games in Child Psychotherapy

ERIC Educational Resources Information Center

Oren, Ayala

2008-01-01

Playing checkers, football or more recently, computer games, is an important part of the latency child's culture. The ability to play games demands a level of emotional development similar to that needed to cope with the emotional/developmental demands characteristic of latency. A game shared by the therapist and child provides a picture of the…

Behavior and space utilization of two common fishes within Caribbean mangroves: implications for the protective function of mangrove habitats

NASA Astrophysics Data System (ADS)

MacDonald, J. A.; Shahrestani, S.; Weis, J. S.

2009-09-01

Behaviors, activity budgets, and spatial locations of reef-associated schoolmaster snapper ( Lutjanus apodus) and non-reef-associated checkered puffer ( Sphoeroides testudineus) were cataloged in mangrove forests in Caribbean Honduras to see how and where they spent their time and whether this changed as they grew. For schoolmasters, swimming was the most common behavior, while checkered puffers spent the majority of their time resting. Both remained completely within (as opposed to outside) the mangrove roots and in the lower half of the water column most of the time. However, as the size of the fish increased there was a clear decrease in the time spent both within the root system and closer to the substrate; the larger fish spent more time higher up in the water column and outside the root system. This was observed in both the schoolmaster and the puffer; the schoolmaster subsequently moves to reefs while the puffer does not. Coupled with limited feeding, the results suggest a primarily protective function for mangroves.

Spin Foam Models of Quantum Gravity

NASA Astrophysics Data System (ADS)

Miković, A.

2005-03-01

We give a short review of the spin foam models of quantum gravity, with an emphasis on the Barret-Crane model. After explaining the shortcomings of the Barret-Crane model, we briefly discuss two new approaches, one based on the 3d spin foam state sum invariants for the embedded spin networks, and the other based on representing the string scattering amplitudes as 2d spin foam state sum invariants.

Hypothesized diprotomeric enzyme complex supported by stochastic modelling of palytoxin-induced Na/K pump channels

PubMed Central

Vilallonga, Gabriel D.; de Almeida, Antônio-Carlos G.; Ribeiro, Kelison T.; Campos, Sergio V. A.

2018-01-01

The sodium–potassium pump (Na+/K+ pump) is crucial for cell physiology. Despite great advances in the understanding of this ionic pumping system, its mechanism is not completely understood. We propose the use of a statistical model checker to investigate palytoxin (PTX)-induced Na+/K+ pump channels. We modelled a system of reactions representing transitions between the conformational substates of the channel with parameters, concentrations of the substates and reaction rates extracted from simulations reported in the literature, based on electrophysiological recordings in a whole-cell configuration. The model was implemented using the UPPAAL-SMC platform. Comparing simulations and probabilistic queries from stochastic system semantics with experimental data, it was possible to propose additional reactions to reproduce the single-channel dynamic. The probabilistic analyses and simulations suggest that the PTX-induced Na+/K+ pump channel functions as a diprotomeric complex in which protein–protein interactions increase the affinity of the Na+/K+ pump for PTX. PMID:29657808

Free-Spinning-Tunnel Investigation of a 1/24-Scale Model of the Grumman F9F-6 Airplane TED No. NACA DE 364

NASA Technical Reports Server (NTRS)

Klinar, Walter J.; Healy, Frederick M.

1952-01-01

An investigation of a 1/24-scale model of the Grumman F9F-6 airplane has been conducted in the Langley 20-foot free-spinning tunnel. The erect and inverted spin and recovery characteristics of the model were determined for the normal flight loading with the model in the clean condition. The effect of loading variations was investigated briefly. Spin-recovery parachute tests were also performed. The results indicate that erect spins obtained on the airplane in the clean condition will be satisfactorily terminated for all loading conditions provided full rudder reversal is accompanied by moving the ailerons and flaperons (lateral controls) to full with the spin (stick right in a right spin). Inverted spins should be satisfactorily terminated by full reversal of the rudder alone. The model tests indicate that an 11.4-foot (laid-out-flat diameter) tail parachute (drag coefficient approximately 0.73) should be effective as an emergency spin-recovery device during demonstration spins of the airplane provided the towline is attached above the horizontal stabilizer.

Free-Spinning-Tunnel Tests of a 1/24-Scale Model of the Grumman XF9F-2 Airplane, TED No. NACA DE 317

NASA Technical Reports Server (NTRS)

Berman, Theodore

1948-01-01

An investigation of the spin and recovery characteristics of a scale model of the Grumman XF9F-2 airplane has been conducted in the Langley 20-foot free-spinning tunnel. The effects of control settings and movements on the erect and inverted spin and recovery characteristics of the model in the flight loading were determined. The investigation also included spin-recovery-parachute, pilot-escape, and rudder-pedal- . force tests. The recovery characteristics of the model were satisfactory for all configurations tested. Spins for the normal control configuration were oscillatory in roll and yaw. Deflecting the leading-edge flaps or the dive brakes did not change the spin and recovery characteristics of the model noticeably. A 10.0-foot tail parachute or a 6.0-foot wing-tip parachute (drag coefficient of 0.75) was found to be effective for recoveries from demonstration spins. The rudder forces in the spin appeared to be within the capabilities of the pilot.

Phase transition and monopole densities in a nearest neighbor two-dimensional spin ice model

NASA Astrophysics Data System (ADS)

Morais, C. W.; de Freitas, D. N.; Mota, A. L.; Bastone, E. C.

2017-12-01

In this work, we show that, due to the alternating orientation of the spins in the ground state of the artificial square spin ice, the influence of a set of spins at a certain distance of a reference spin decreases faster than the expected result for the long range dipolar interaction, justifying the use of the nearest neighbor two-dimensional square spin ice model as an effective model. Using an extension of the model presented in Y. L. Xie et al., Sci. Rep. 5, 15875 (2015), considering the influence of the eight nearest neighbors of each spin on the lattice, we analyze the thermodynamics of the model and study the dependence of monopoles and string densities as a function of the temperature.

Finding Feasible Abstract Counter-Examples

NASA Technical Reports Server (NTRS)

Pasareanu, Corina S.; Dwyer, Matthew B.; Visser, Willem; Clancy, Daniel (Technical Monitor)

2002-01-01

A strength of model checking is its ability to automate the detection of subtle system errors and produce traces that exhibit those errors. Given the high computational cost of model checking most researchers advocate the use of aggressive property-preserving abstractions. Unfortunately, the more aggressively a system is abstracted the more infeasible behavior it will have. Thus, while abstraction enables efficient model checking it also threatens the usefulness of model checking as a defect detection tool, since it may be difficult to determine whether a counter-example is feasible and hence worth developer time to analyze. We have explored several strategies for addressing this problem by extending an explicit-state model checker, Java PathFinder (JPF), to search for and analyze counter-examples in the presence of abstractions. We demonstrate that these techniques effectively preserve the defect detection ability of model checking in the presence of aggressive abstraction by applying them to check properties of several abstracted multi-threaded Java programs. These new capabilities are not specific to JPF and can be easily adapted to other model checking frameworks; we describe how this was done for the Bandera toolset.

Enabling model checking for collaborative process analysis: from BPMN to `Network of Timed Automata'

NASA Astrophysics Data System (ADS)

Mallek, Sihem; Daclin, Nicolas; Chapurlat, Vincent; Vallespir, Bruno

2015-04-01

Interoperability is a prerequisite for partners involved in performing collaboration. As a consequence, the lack of interoperability is now considered a major obstacle. The research work presented in this paper aims to develop an approach that allows specifying and verifying a set of interoperability requirements to be satisfied by each partner in the collaborative process prior to process implementation. To enable the verification of these interoperability requirements, it is necessary first and foremost to generate a model of the targeted collaborative process; for this research effort, the standardised language BPMN 2.0 is used. Afterwards, a verification technique must be introduced, and model checking is the preferred option herein. This paper focuses on application of the model checker UPPAAL in order to verify interoperability requirements for the given collaborative process model. At first, this step entails translating the collaborative process model from BPMN into a UPPAAL modelling language called 'Network of Timed Automata'. Second, it becomes necessary to formalise interoperability requirements into properties with the dedicated UPPAAL language, i.e. the temporal logic TCTL.

Boson-mediated quantum spin simulators in transverse fields: X Y model and spin-boson entanglement

NASA Astrophysics Data System (ADS)

Wall, Michael L.; Safavi-Naini, Arghavan; Rey, Ana Maria

2017-01-01

The coupling of spins to long-wavelength bosonic modes is a prominent means to engineer long-range spin-spin interactions, and has been realized in a variety of platforms, such as atoms in optical cavities and trapped ions. To date, much of the experimental focus has been on the realization of long-range Ising models, but generalizations to other spin models are highly desirable. In this work, we explore a previously unappreciated connection between the realization of an X Y model by off-resonant driving of a single sideband of boson excitation (i.e., a single-beam Mølmer-Sørensen scheme) and a boson-mediated Ising simulator in the presence of a transverse field. In particular, we show that these two schemes have the same effective Hamiltonian in suitably defined rotating frames, and analyze the emergent effective X Y spin model through a truncated Magnus series and numerical simulations. In addition to X Y spin-spin interactions that can be nonperturbatively renormalized from the naive Ising spin-spin coupling constants, we find an effective transverse field that is dependent on the thermal energy of the bosons, as well as other spin-boson couplings that cause spin-boson entanglement not to vanish at any time. In the case of a boson-mediated Ising simulator with transverse field, we discuss the crossover from transverse field Ising-like to X Y -like spin behavior as a function of field strength.

Free-Spinning-Tunnel Investigation of a 1/28-Scale Model of the North American FJ-4 Airplane with External Fuel Tanks, TED No. NACA AD 3112

NASA Technical Reports Server (NTRS)

Healy, Frederick M.

1958-01-01

A supplementary investigation to determine the effect of external fuel tanks on the spin and recovery characteristics of a l/28-scale model of the North American FJ-4 airplane has been conducted in the Langley 20-foot free-spinning tunnel. The model had been extensively tested previously (NACA Research Memorandum SL38A29) and therefore only brief tests were made to evaluate the effect of tank installation. Erect spin tests of the model indicate that flat-type spins-are more prevalent with 200-gallon external fuel tanks than with tanks not installed. The recovery technique determined for spins without tanks, rudder reversal to full against the spin accompanied by simultaneous movement of ailerons to full with the spin, is recommended for spins encountered with external tanks installed. If inverted spins are encountered with external tanks installed, the tanks should be jettisoned and recovery attempted by rudder reversal to full against the spin with ailerons maintained at neutral.

Generalized Kondo lattice model and its spin-polaron realization by the projection method for cuprates

NASA Astrophysics Data System (ADS)

Valkov, V. V.; Dzebisashvili, D. M.; Barabanov, A. F.

2017-05-01

The spin-fermion model, which is an effective low-energy realization of the three-band Emery model after passing to the Wannier representation for the px and py orbitals of the subsystem of oxygen ions, reduces to the generalized Kondo lattice model. A specific feature of this model is the existence of spin-correlated hoppings of the current carriers between distant cells. Numerical calculations of the spectrum of spin-electron excitations highlight the important role of the long-range spin-correlated hoppings.

Nuclear spin noise in the central spin model

NASA Astrophysics Data System (ADS)

Fröhling, Nina; Anders, Frithjof B.; Glazov, Mikhail

2018-05-01

We study theoretically the fluctuations of the nuclear spins in quantum dots employing the central spin model which accounts for the hyperfine interaction of the nuclei with the electron spin. These fluctuations are calculated both with an analytical approach using homogeneous hyperfine couplings (box model) and with a numerical simulation using a distribution of hyperfine coupling constants. The approaches are in good agreement. The box model serves as a benchmark with low computational cost that explains the basic features of the nuclear spin noise well. We also demonstrate that the nuclear spin noise spectra comprise a two-peak structure centered at the nuclear Zeeman frequency in high magnetic fields with the shape of the spectrum controlled by the distribution of the hyperfine constants. This allows for direct access to this distribution function through nuclear spin noise spectroscopy.

TechWriter: An Evolving System for Writing Assistance for Advanced Learners of English

ERIC Educational Resources Information Center

Napolitano, Diane M.; Stent, Amanda

2009-01-01

Writing assistance systems, from simple spelling checkers to more complex grammar and readability analyzers, can be helpful aids to nonnative writers of English. However, many writing assistance systems have two disadvantages. First, they are not designed to encourage skills learning and independence in their users; instead, users may begin to use…

Checker Takes the Guesswork out of Diode Identification

ERIC Educational Resources Information Center

Harman, Charles

2011-01-01

At technical colleges and secondary-level tech schools, students enrolled in basic electronics labs who have learned about diodes that do rectification are used to seeing power diodes like the 1N4001. When the students are introduced to low-power zener diodes and signal diodes, component identification gets more complex. If the small zeners are…

Don't Lose Your Marbles!: Game Project Teaches Introductory Manufacturing Skills

ERIC Educational Resources Information Center

Kapur, Arjun; Carter, Horlin; Dillon, Dave

2006-01-01

This article describes a lab activity conducted in an introductory manufacturing class. In this good, simple, mass-production project, the students designed and produced a small game composed of a piece of plywood and 14 glass marbles. In appearance, the game is something like Chinese checkers, but it involves jumping over marbles, then removing…

Check that JFET! Easy-to-Build Tester Makes It Simple

ERIC Educational Resources Information Center

Harman, Charles

2008-01-01

This article describes an activity that will allow students to learn how to make a junction field effect transistor (JFET) checker. Most electronics students do not have the experience or knowledge that it takes to recognize whether a JFET is operating normally, and both instructors and students will find having the means to check the operation of…

Dave Moore: Taking Roundabout Path to Perovskite Fast Track | News | NREL

Science.gov Websites

energy of academia is awesome and contagious. It keeps you young to hang around young people and keep learning." Although he'd had a checkered high school academic career prior to stepping on the college ," Moore said. "That's where I first learned about the energy crisis." And that's when he

Protocol Programmability

DTIC Science & Technology

2013-12-01

First, any subproject that involved an implementation shared some implementation infrastructure with other subprojects. For example, the Plaid backend ...very same language. We followed this advice in Plaid, and we therefore implemented the compiler backend in Plaid (code generation, type checker, Æminim...programming language aimed at enforcing security properties in web and mobile applications [Nistor et al., 2013]. Wyvern therefore provides an excellent

Mountain Plains Learning Experience Guide: Marketing. Course: Cash Register Operation.

ERIC Educational Resources Information Center

Egan, B.

One of thirteen individualized courses included in a marketing curriculum, this course is on the fundamentals of operating a cash register. The course is comprised of four units: (1) Face of Cash Register, (2) Operating a Checkout Station, (3) Checker-Cashier Qualities, and (4) NCR 250 Electronic Cash Register. Each unit begins with a Unit…

To Kill a Messenger; Television News and the Real World.

ERIC Educational Resources Information Center

Small, William

From his vantage point as News Director of CBS News in Washington, the author examines the role of television news in our society and gives an insider's view of the day-to-day process of selecting and presenting news. Highlighting the book are in-depth discussions of past and recent news events. The Nixon "Checkers" speech, John…

Studies Relating to Computer Use of Spelling and Grammar Checkers and Educational Achievement

ERIC Educational Resources Information Center

Radi, Odette Bourjaili

2015-01-01

The content of this paper will focus on both language and computer practices and how school age students develop their literacy skills in the two domains of "language" and "computers." The term literacy is a broad concept that has attracted many interpretations over the years. Some of the concepts raised by the literature apply…

A Preliminary Report on a New Grammar Checker to Help Students of English as a Foreign Language

ERIC Educational Resources Information Center

Lawley, Jim

2004-01-01

Whereas many pre-intermediate and intermediate level students of English as a Foreign Language (EFL) might benefit from receiving detailed feedback on mistakes in their written compositions, there are obvious practical limits to the amount of corrective feedback that teachers in schools and universities can provide. This article briefly describes…

Adding Statistical Machine Translation Adaptation to Computer-Assisted Translation

DTIC Science & Technology

2013-09-01

are automatically searched and used to suggest possible translations; (2) spell-checkers; (3) glossaries; (4) dictionaries ; (5) alignment and...matching against TMs to propose translations; spell-checking, glossary, and dictionary look-up; support for multiple file formats; regular expressions...on Telecommunications. Tehran, 2012, 822–826. Bertoldi, N.; Federico, M. Domain Adaptation for Statistical Machine Translation with Monolingual

Comprehension Monitoring by Elementary Students: When Does It Occur?

ERIC Educational Resources Information Center

Pace, Ann Jaffe

The effect of passage topic and task demands on elementary school students' monitoring of their own comprehension was examined. Second, fourth, and sixth grade students read a short passage about a well-known event (playing checkers) or one about which they had little existing information (making lye soap). Half of the students in each grade were…

Cerebral oximetry: a replacement for pulse oximetry?

PubMed

Frost, Elizabeth A M

2012-10-01

Cerebral oximetry has been around for some 3 decades but has had a somewhat checkered history regarding application and reliability. More recently several monitors have been approved in the United States and elsewhere and the technique is emerging as a useful tool for assessing not only adequate cerebral oxygenation but also tissue oxygenation and perfusion in other organs.

Test SCRs and Triacs with a Lab-Built Checker

ERIC Educational Resources Information Center

Harman, Charles

2010-01-01

Students enrolled in advanced electronics courses and/or industrial electronics classes at the high school level and at technical colleges ultimately learn about solid-state switches such as the SCR (silicon controlled rectifier) and the triac. Both the SCR and the triac are in a family of four-layer devices called thyristors. They are both…

Simple universal models capture all classical spin physics.

PubMed

De las Cuevas, Gemma; Cubitt, Toby S

2016-03-11

Spin models are used in many studies of complex systems because they exhibit rich macroscopic behavior despite their microscopic simplicity. Here, we prove that all the physics of every classical spin model is reproduced in the low-energy sector of certain "universal models," with at most polynomial overhead. This holds for classical models with discrete or continuous degrees of freedom. We prove necessary and sufficient conditions for a spin model to be universal and show that one of the simplest and most widely studied spin models, the two-dimensional Ising model with fields, is universal. Our results may facilitate physical simulations of Hamiltonians with complex interactions. Copyright © 2016, American Association for the Advancement of Science.

Concluding Report on Free-Spinning and Recovery Characteristics of a 1/24-Scale Model of the Grumman F11F-1 Airplane, TED No. NACA AD 395

NASA Technical Reports Server (NTRS)

Bowman, James S., Jr.

1956-01-01

An investigation has been completed in the Langley 20-foot free-spinning tunnel on a l/24-scale model of the Grumman F11F-1 airplane to determine its spin and recovery characteristics. An interim report, Research Memorandum SL55G20, was published earlier and the present report concludes the presentation of results of the investigation. Primarily, the present report presents results obtained with engine gyroscopic moments simulated on the model. Also, the current results were obtained with a revised larger vertical tail recently incorporated on the airplane. It was difficult to obtain developed spins on the model when the spin direction was in the same sense as that of the engine rotation (right spin on the airplane). The developed spins obtained were very oscillatory and the recoveries were unsatisfactory. These results were similar to those previously reported for which engine rotation was not simulated. When the spin direction was in the opposite sense (left spin on the airplane), however, developed spins were readily obtainable. Recoveries from these spins also were unsatisfactory. Satisfactory recoveries were obtained on the model, however, when rudder reversal was accompanied by extension of small canards near the nose of the airplane or by deflection of the horizontal tail differentially with the spin.

Two-level system in spin baths: Non-adiabatic dynamics and heat transport

NASA Astrophysics Data System (ADS)

Segal, Dvira

2014-04-01

We study the non-adiabatic dynamics of a two-state subsystem in a bath of independent spins using the non-interacting blip approximation, and derive an exact analytic expression for the relevant memory kernel. We show that in the thermodynamic limit, when the subsystem-bath coupling is diluted (uniformly) over many (infinite) degrees of freedom, our expression reduces to known results, corresponding to the harmonic bath with an effective, temperature-dependent, spectral density function. We then proceed and study the heat current characteristics in the out-of-equilibrium spin-spin-bath model, with a two-state subsystem bridging two thermal spin-baths of different temperatures. We compare the behavior of this model to the case of a spin connecting boson baths, and demonstrate pronounced qualitative differences between the two models. Specifically, we focus on the development of the thermal diode effect, and show that the spin-spin-bath model cannot support it at weak (subsystem-bath) coupling, while in the intermediate-strong coupling regime its rectifying performance outplays the spin-boson model.

Influence of Dzyaloshinskii-Moriya interaction and ballistic spin transport in the two and three-dimensional Heisenberg model

NASA Astrophysics Data System (ADS)

Lima, L. S.

2018-06-01

We study the effect of Dzyaloshisnkii-Moriya interaction on spin transport in the two and three-dimensional Heisenberg antiferromagnetic models in the square lattice and cubic lattice respectively. For the three-dimensional model, we obtain a large peak for the spin conductivity and therefore a finite AC conductivity. For the two-dimensional model, we have gotten the AC spin conductivity tending to the infinity at ω → 0 limit and a suave decreasing in the spin conductivity with increase of ω. We obtain a small influence of the Dzyaloshinskii-Moriya interaction on the spin conductivity in all cases analyzed.

Spin-tunnel investigation of a 1/25-scale model of the General Dynamics F-16XL airplane

NASA Technical Reports Server (NTRS)

Whipple, R. D.; White, W. L.

1984-01-01

A spin-tunnel investigation of the spin and recovery characteristics of a 1/25-scale model to the General Dynamics F-16XL aircraft was conducted in the Langley Spin Tunnel. Tests included erect and inverted spins at various symmetric and asymmetric loading conditions. The required size of an emergency spin-recovery parachute was determined.

Spintronics: spin accumulation in mesoscopic systems.

PubMed

Johnson, Mark

2002-04-25

In spintronics, in which use is made of the spin degree of freedom of the electron, issues concerning electrical spin injection and detection of electron spin diffusion are fundamentally important. Jedema et al. describe a magneto-resistance study in which they claim to have observed spin accumulation in a mesoscopic copper wire, but their one-dimensional model ignores two-dimensional spin-diffusion effects, which casts doubt on their analysis. A two-dimensional vector formalism of spin transport is called for to model spin-injection experiments, and the identification of spurious background resistance effects is crucial.

Designing Kitaev Spin Liquids in Metal-Organic Frameworks

NASA Astrophysics Data System (ADS)

Yamada, Masahiko G.; Fujita, Hiroyuki; Oshikawa, Masaki

2017-08-01

Kitaev's honeycomb lattice spin model is a remarkable exactly solvable model, which has a particular type of spin liquid (Kitaev spin liquid) as the ground state. Although its possible realization in iridates and α -RuCl3 has been vigorously discussed recently, these materials have substantial non-Kitaev direct exchange interactions and do not have a spin liquid ground state. We propose metal-organic frameworks (MOFs) with Ru3 + (or Os3 + ), forming the honeycomb lattice as promising candidates for a more ideal realization of Kitaev-type spin models, where the direct exchange interaction is strongly suppressed. The great flexibility of MOFs allows generalization to other three-dimensional lattices for the potential realization of a variety of spin liquids, such as a Weyl spin liquid.

Spinning Characteristics of the XN2Y-1 Airplane Obtained from the Spinning Balance and Compared with Results from the Spinning Tunnel and from Flight Tests

NASA Technical Reports Server (NTRS)

Bamber, M J; House, R O

1937-01-01

Report presents the results of tests of a 1/10-scale model of the XN2Y-1 airplane tested in the NACA 5-foot vertical wind tunnel in which the six components of forces and moments were measured. The model was tested in 17 attitudes in which the full-scale airplane had been observed to spin, in order to determine the effects of scale, tunnel, and interference. In addition, a series of tests was made to cover the range of angles of attack, angles of sideslip, rates of rotation, and control setting likely to be encountered by a spinning airplane. The data were used to estimate the probable attitudes in steady spins of an airplane in flight and of a model in the free-spinning tunnel. The estimated attitudes of steady spin were compared with attitudes measured in flight and in the spinning tunnel. The results indicate that corrections for certain scale and tunnel effects are necessary to estimate full-scale spinning attitudes from model results.

High spin systems with orbital degeneracy.

PubMed

Shen, Shun-Qing; Xie, X C; Zhang, F C

2002-01-14

High-spin systems with orbital degeneracy are studied in the large spin limit. In the absence of Hund's coupling, the classical spin model is mapped onto disconnected orbital systems with spins up and down, respectively. The ground state of the isotropic model is an orbital valence bond state where each bond is an orbital singlet with parallel spins, and neighboring bonds interact antiferromagnetically. Possible relevance to the transition metal oxides is discussed.

Monitoring Programs Using Rewriting

NASA Technical Reports Server (NTRS)

Havelund, Klaus; Rosu, Grigore; Lan, Sonie (Technical Monitor)

2001-01-01

We present a rewriting algorithm for efficiently testing future time Linear Temporal Logic (LTL) formulae on finite execution traces, The standard models of LTL are infinite traces, reflecting the behavior of reactive and concurrent systems which conceptually may be continuously alive in most past applications of LTL, theorem provers and model checkers have been used to formally prove that down-scaled models satisfy such LTL specifications. Our goal is instead to use LTL for up-scaled testing of real software applications, corresponding to analyzing the conformance of finite traces against LTL formulae. We first describe what it means for a finite trace to satisfy an LTL property end then suggest an optimized algorithm based on transforming LTL formulae. We use the Maude rewriting logic, which turns out to be a good notation and being supported by an efficient rewriting engine for performing these experiments. The work constitutes part of the Java PathExplorer (JPAX) project, the purpose of which is to develop a flexible tool for monitoring Java program executions.

Exchange interactions in transition metal oxides: the role of oxygen spin polarization.

PubMed

Logemann, R; Rudenko, A N; Katsnelson, M I; Kirilyuk, A

2017-08-23

Magnetism of transition metal (TM) oxides is usually described in terms of the Heisenberg model, with orientation-independent interactions between the spins. However, the applicability of such a model is not fully justified for TM oxides because spin polarization of oxygen is usually ignored. In the conventional model based on the Anderson principle, oxygen effects are considered as a property of the TM ion and only TM interactions are relevant. Here, we perform a systematic comparison between two approaches for spin polarization on oxygen in typical TM oxides. To this end, we calculate the exchange interactions in NiO, MnO and hematite (Fe 2 O 3 ) for different magnetic configurations using the magnetic force theorem. We consider the full spin Hamiltonian including oxygen sites, and also derive an effective model where the spin polarization on oxygen renormalizes the exchange interactions between TM sites. Surprisingly, the exchange interactions in NiO depend on the magnetic state if spin polarization on oxygen is neglected, resulting in non-Heisenberg behavior. In contrast, the inclusion of spin polarization in NiO makes the Heisenberg model more applicable. Just the opposite, MnO behaves as a Heisenberg magnet when oxygen spin polarization is neglected, but shows strong non-Heisenberg effects when spin polarization on oxygen is included. In hematite, both models result in non-Heisenberg behavior. The general applicability of the magnetic force theorem as well as the Heisenberg model to TM oxides is discussed.

Is nucleon spin structure inconsistent with the constituent quark model?

NASA Astrophysics Data System (ADS)

Qing, Di; Chen, Xiang-Song; Wang, Fan

1998-12-01

Proton spin structure discovered in polarized deep inelastic scattering is shown to be consistent with the valence-sea quark mixing constituent quark model. The relativistic correction and quark-antiquark pair creation (annihilation) terms inherently involved in the quark axial vector current suppress the quark spin contribution to the proton spin. The relativistic quark orbital angular momentum provides compensative terms to keep the proton spin 12 untouched. The tensor charge of the proton is predicted to have a similar but smaller suppression. An explanation on why baryon magnetic moments can be parametrized by the naive quark model spin content as well as the spin structure discovered in polarized deep inelastic scattering is given.

Meissner mechanism for the spin supercurrent and interplay between quantum phase transition and spin transport in the frustrated Heisenberg model

NASA Astrophysics Data System (ADS)

Lima, Leonardo S.

2018-04-01

We have propose the Meissner mechanism for the spin supercurrent in quantum spin systems. Besides, we study the behavior of the AC spin conductivity in neighborhood of quantum phase transition in a frustrated spin model such as the antiferromagnet in the union jack lattice with single ion anisotropy at T = 0 . We investigate the spin conductivity for this model that presents exchange interactions J1 and J2 . Our results show a single peak for the conductivity with the height varying with the behavior of critical anisotropy Dc with J2 . We obtain the conductivity tending to zero in the limit ω → 0 .

Analysis of a gauged model with a spin-1/2 field directly coupled to a Rarita-Schwinger spin-3/2 field

NASA Astrophysics Data System (ADS)

Adler, Stephen L.

2018-02-01

We give a detailed analysis of an Abelianized gauge field model in which a Rarita-Schwinger spin-3/2 field is directly coupled to a spin-1/2 field. The model permits a perturbative expansion in powers of the gauge field coupling, and from the Feynman rules for the model we calculate the chiral anomaly.

Certified In-lined Reference Monitoring on .NET

DTIC Science & Technology

2006-06-01

Introduction Language -based approaches to computer security have employed two major strategies for enforcing security policies over untrusted programs. • Low...automatically verify IRM’s using a static type-checker. Mobile (MOnitorable BIL with Effects) is an exten- sion of BIL (Baby Intermediate Language ) [15], a...AVAILABILITY STATEMENT Approved for public release; distribution unlimited 13. SUPPLEMENTARY NOTES Proceedings of the 2006 Programming Languages and

Authenticity in Education: From Narcissism and Freedom to the Messy Interplay of Self-Exploration and Acceptable Tension

ERIC Educational Resources Information Center

Thompson, Merlin B.

2015-01-01

The problem with authenticity--the idea of being "true to one's self"--is that its somewhat checkered reputation garners a complete range of favorable and unfavorable reactions. In educational settings, authenticity is lauded as one of the top two traits students desire in their teachers. Yet, authenticity is criticized for its tendency…

76 FR 36955 - West Los Angeles VA Medical Center Veterans Programs Enhancement Act of 1998; Master Plan

Federal Register 2010, 2011, 2012, 2013, 2014

2011-06-23

... Brentwood School and MacArthur Field as part of the land use agreements for those spaces. A planned future..., the historic Rose Garden, will be completed in fall of 2011. This area, located just across the street from the Domiciliary, will include meditative gardens, tables for chess and checkers, and soothing...

Crowdsourcing quality control for Dark Energy Survey images

DOE PAGES

Melchior, P.

2016-07-01

We have developed a crowdsourcing web application for image quality control employed by the Dark Energy Survey. Dubbed the "DES exposure checker", it renders science-grade images directly to a web browser and allows users to mark problematic features from a set of predefined classes. Users can also generate custom labels and thus help identify previously unknown problem classes. User reports are fed back to hardware and software experts to help mitigate and eliminate recognized issues. We report on the implementation of the application and our experience with its over 100 users, the majority of which are professional or prospective astronomersmore » but not data management experts. We discuss aspects of user training and engagement, and demonstrate how problem reports have been pivotal to rapidly correct artifacts which would likely have been too subtle or infrequent to be recognized otherwise. We conclude with a number of important lessons learned, suggest possible improvements, and recommend this collective exploratory approach for future astronomical surveys or other extensive data sets with a sufficiently large user base. We also release open-source code of the web application and host an online demo versionat http://des-exp-checker.pmelchior.net« less

Crowdsourcing quality control for Dark Energy Survey images

NASA Astrophysics Data System (ADS)

Melchior, P.; Sheldon, E.; Drlica-Wagner, A.; Rykoff, E. S.; Abbott, T. M. C.; Abdalla, F. B.; Allam, S.; Benoit-Lévy, A.; Brooks, D.; Buckley-Geer, E.; Carnero Rosell, A.; Carrasco Kind, M.; Carretero, J.; Crocce, M.; D'Andrea, C. B.; da Costa, L. N.; Desai, S.; Doel, P.; Evrard, A. E.; Finley, D. A.; Flaugher, B.; Frieman, J.; Gaztanaga, E.; Gerdes, D. W.; Gruen, D.; Gruendl, R. A.; Honscheid, K.; James, D. J.; Jarvis, M.; Kuehn, K.; Li, T. S.; Maia, M. A. G.; March, M.; Marshall, J. L.; Nord, B.; Ogando, R.; Plazas, A. A.; Romer, A. K.; Sanchez, E.; Scarpine, V.; Sevilla-Noarbe, I.; Smith, R. C.; Soares-Santos, M.; Suchyta, E.; Swanson, M. E. C.; Tarle, G.; Vikram, V.; Walker, A. R.; Wester, W.; Zhang, Y.

2016-07-01

We have developed a crowdsourcing web application for image quality control employed by the Dark Energy Survey. Dubbed the "DES exposure checker", it renders science-grade images directly to a web browser and allows users to mark problematic features from a set of predefined classes. Users can also generate custom labels and thus help identify previously unknown problem classes. User reports are fed back to hardware and software experts to help mitigate and eliminate recognized issues. We report on the implementation of the application and our experience with its over 100 users, the majority of which are professional or prospective astronomers but not data management experts. We discuss aspects of user training and engagement, and demonstrate how problem reports have been pivotal to rapidly correct artifacts which would likely have been too subtle or infrequent to be recognized otherwise. We conclude with a number of important lessons learned, suggest possible improvements, and recommend this collective exploratory approach for future astronomical surveys or other extensive data sets with a sufficiently large user base. We also release open-source code of the web application and host an online demo version at http://des-exp-checker.pmelchior.net.

Crowdsourcing quality control for Dark Energy Survey images

DOE Office of Scientific and Technical Information (OSTI.GOV)

Melchior, P.

We have developed a crowdsourcing web application for image quality control employed by the Dark Energy Survey. Dubbed the "DES exposure checker", it renders science-grade images directly to a web browser and allows users to mark problematic features from a set of predefined classes. Users can also generate custom labels and thus help identify previously unknown problem classes. User reports are fed back to hardware and software experts to help mitigate and eliminate recognized issues. We report on the implementation of the application and our experience with its over 100 users, the majority of which are professional or prospective astronomersmore » but not data management experts. We discuss aspects of user training and engagement, and demonstrate how problem reports have been pivotal to rapidly correct artifacts which would likely have been too subtle or infrequent to be recognized otherwise. We conclude with a number of important lessons learned, suggest possible improvements, and recommend this collective exploratory approach for future astronomical surveys or other extensive data sets with a sufficiently large user base. We also release open-source code of the web application and host an online demo versionat http://des-exp-checker.pmelchior.net« less

Free-Spinning-Tunnel Investigation of a 1/25-Scale Model of the McDonnell F3H-1N Airplane, TED No. NACA AD 3100

NASA Technical Reports Server (NTRS)

Lee, Henry A.; Wilkes, L. Faye

1954-01-01

An investigation was conducted in the Langley 20-foot free-spinning tunnel on a 1/23-scale model of the McDonnell F3H-1N airplane. The effects of control settings and movements upon the erect and inverted spin and recovery characteristics of the model were determined for the clean condition. Spin-recovery parachute tests were also performed. The results indicated that erect spins obtained on the airplane for the take-off or combat loadings should be satisfactorily terminated if full rudder reversal is accompanied by moving the ailerons to full with the spin (stick full right in a right spin). The spins obtained should be oscillatory in pitch, roll, and yaw. Recoveries from inverted spins should be satisfactory by full reversal of the rudder. A 16.7-foot- diameter tail parachute with a towline length of 30 feet and a drag coefficient of 0.734 should be adequate for emergency recovery from demonstration spins.

How to fold a spin chain: Integrable boundaries of the Heisenberg XXX and Inozemtsev hyperbolic models

NASA Astrophysics Data System (ADS)

De La Rosa Gomez, Alejandro; MacKay, Niall; Regelskis, Vidas

2017-04-01

We present a general method of folding an integrable spin chain, defined on a line, to obtain an integrable open spin chain, defined on a half-line. We illustrate our method through two fundamental models with sl2 Lie algebra symmetry: the Heisenberg XXX and the Inozemtsev hyperbolic spin chains. We obtain new long-range boundary Hamiltonians and demonstrate that they exhibit Yangian symmetries, thus ensuring integrability of the models we obtain. The method presented provides a ;bottom-up; approach for constructing integrable boundaries and can be applied to any spin chain model.

Role of spin-orbit coupling in the Kugel-Khomskii model on the honeycomb lattice

NASA Astrophysics Data System (ADS)

Koga, Akihisa; Nakauchi, Shiryu; Nasu, Joji

2018-03-01

We study the effective spin-orbital model for honeycomb-layered transition metal compounds, applying the second-order perturbation theory to the three-orbital Hubbard model with the anisotropic hoppings. This model is reduced to the Kitaev model in the strong spin-orbit coupling limit. Combining the cluster mean-field approximations with the exact diagonalization, we treat the Kugel-Khomskii type superexchange interaction and spin-orbit coupling on an equal footing to discuss ground-state properties. We find that a zigzag ordered state is realized in the model within nearest-neighbor interactions. We clarify how the ordered state competes with the nonmagnetic state, which is adiabatically connected to the quantum spin liquid state realized in a strong spin-orbit coupling limit. Thermodynamic properties are also addressed. The present paper should provide another route to account for the Kitaev-based magnetic properties in candidate materials.

Free-Spinning-Tunnel Investigation of a 1/20-Scale Model of the North American T2J-1 Airplane

NASA Technical Reports Server (NTRS)

Bowman, James S., Jr.; Healy, Frederick M.

1959-01-01

An investigation has been made in the Langley 20-foot free-spinning tunnel to determine the erect and inverted spin and recovery characteristics of a 1/20-scale dynamic model of the North American T2J-1 airplane. The model results indicate that the optimum technique for recovery from erect spins of the airplane will be dependent on the distribution of the disposable load. The recommended recovery procedure for spins encountered at the flight design gross weight is simultaneous rudder reversal to against the spin and aileron movement to with the spin. With full wingtip tanks plus rocket installation and full internal fuel load, rudder reversal should be followed by a downward movement of the elevator. For the flight design gross weight plus partially full wingtip tanks, recovery should be attempted by simultaneous rudder reversal to against the spin, movement of ailerons to with the spin, and ejection of the wing-tip tanks. The optimum recovery technique for airplane-inverted spins is rudder reversal to against the spin with the stick maintained longitudinally and laterally neutral.

Spin-scattering rates in metallic thin films measured by ferromagnetic resonance damping enhanced by spin-pumping

DOE Office of Scientific and Technical Information (OSTI.GOV)

Boone, C. T.; Shaw, J. M.; Nembach, H. T.

2015-06-14

We determined the spin-transport properties of Pd and Pt thin films by measuring the increase in ferromagnetic resonance damping due to spin-pumping in ferromagnetic (FM)-nonferromagnetic metal (NM) multilayers with varying NM thicknesses. The increase in damping with NM thickness depends strongly on both the spin- and charge-transport properties of the NM, as modeled by diffusion equations that include both momentum- and spin-scattering parameters. We use the analytical solution to the spin-diffusion equations to obtain spin-diffusion lengths for Pt and Pd. By measuring the dependence of conductivity on NM thickness, we correlate the charge- and spin-transport parameters, and validate the applicabilitymore » of various models for momentum-scattering and spin-scattering rates in these systems: constant, inverse-proportional (Dyakanov-Perel), and linear-proportional (Elliot-Yafet). We confirm previous reports that the spin-scattering time appears to be shorter than the momentum scattering time in Pt, and the Dyakanov-Perel-like model is the best fit to the data.« less

Breakdown of single spin-fluid model in the heavily hole-doped superconductor CsFe2As2

NASA Astrophysics Data System (ADS)

Zhao, D.; Li, S. J.; Wang, N. Z.; Li, J.; Song, D. W.; Zheng, L. X.; Nie, L. P.; Luo, X. G.; Wu, T.; Chen, X. H.

2018-01-01

Although Fe-based superconductors are correlated electronic systems with multiorbital, previous nuclear magnetic resonance (NMR) measurement suggests that a single spin-fluid model is sufficient to describe its spin behavior. Here, we first observed the breakdown of single spin-fluid model in a heavily hole-doped Fe-based superconductor CsFe2As2 by site-selective NMR measurement. At high-temperature regime, both Knight shift and nuclear spin-lattice relaxation at 133Cs and 75As nuclei exhibit distinct temperature-dependent behavior, suggesting the breakdown of the single spin-fluid model in CsFe2As2 . This is ascribed to the coexistence of both localized and itinerant spin degree of freedom at 3 d orbitals, which is consistent with the orbital-selective Mott phase. With decreasing temperature, the single spin-fluid behavior is recovered below T*˜75 K due to a coherent state among 3 d orbitals. The Kondo liquid scenario is proposed to understand the low-temperature coherent state.

Inconsistent Strategies to Spin up Models in CMIP5: Implications for Ocean Biogeochemical Model Performance Assessment

NASA Technical Reports Server (NTRS)

Seferian, Roland; Gehlen, Marion; Bopp, Laurent; Resplandy, Laure; Orr, James C.; Marti, Olivier; Dunne, John P.; Christian, James R.; Doney, Scott C.; Ilyina, Tatiana;

Ground-state energies of the nonlinear sigma model and the Heisenberg spin chains

NASA Technical Reports Server (NTRS)

Zhang, Shoucheng; Schulz, H. J.; Ziman, Timothy

1989-01-01

A theorem on the O(3) nonlinear sigma model with the topological theta term is proved, which states that the ground-state energy at theta = pi is always higher than the ground-state energy at theta = 0, for the same value of the coupling constant g. Provided that the nonlinear sigma model gives the correct description for the Heisenberg spin chains in the large-s limit, this theorem makes a definite prediction relating the ground-state energies of the half-integer and the integer spin chains. The ground-state energies obtained from the exact Bethe ansatz solution for the spin-1/2 chain and the numerical diagonalization on the spin-1, spin-3/2, and spin-2 chains support this prediction.

Free-Spinning Characteristics of a 1/24-Scale Model of the Grumman F11F-1 Airplane, TED No. NACA AD 395

NASA Technical Reports Server (NTRS)

Bowman, James S., Jr.

1955-01-01

An investigation is being conducted in the Langley 20-foot free-spinning tunnel on a 1/24-scale model of the Grumman F11F-1 airplane to determine spin and recovery characteristics and the minimum-size parachute required to satisfactorily terminate the spin in an emergency. Results obtained to date are presented herein. Test results indicate that it may be difficult to obtain an erect or inverted spin on the airplane, but, if a spin is obtained, the spin will be very oscillatory and recovery from the developed erect spin by rudder reversal may not be possible. The lateral controls will have no appreciable effect on recoveries from erect.spins. Recovery from the inverted spin by merely neutralizing the rudder will be satisfactory. After recoveries by rudder reversal and after recoveries from spins without control movement (no spins), the model oftentimes rolled very rapidly about the X-axis. Based on limited preliminary tests made in this investigation to make the model recover satisfactorily, it appears that canards near the nose of the airplane or differentially operated horizontal tails may be utilized to provide rapid recoveries. The parachute test results indicate that an 11-foot-diameter (laid-out-flat) parachute with a drag coefficient of 0.650 (based on the laid- out-flat diameter) and with a towline length equal to the wing span is the minimum-size parachute required to satisfactorily terminate an erect or inverted spin in an emergency.

Free-Spinning-Tunnel Investigation of a 0.034-Scale Model of the Production Version of the Chance Vought F7U-3 Airplane, TED No. NACA AD 3103

NASA Technical Reports Server (NTRS)

Klinar, Walter J.; Healy, Frederick M.

1955-01-01

An investigation of a 0.034-scale model of the production version of the Chance Vought F7U-3 airplane has been conducted in the Langley 20-foot free-spinning tunnel. The inverted and erect spin and recovery characteristics of the model were determined for the combat loading with the model in the clean condition and the effect of extending slats was investigated. A brief investigation of pilot ejection was also performed. The results indicate that the inverted spin-recovery characteristics of the airplane will be satisfactory by full rudder reversal. If the rudders can only be neutralized because of high pedal forces in the inverted spins, satisfactory recovery will be obtained if the auxiliary rudders can be moved to neutral or against the spin provided the stick is held full forward. Optimum control technique for satisfactory recovery from erect spins will be full rudder reversal in conjunction with aileron movement to full with the spin (stick right in a right spin). Extension of the slats will have a slightly adverse effect on recoveries from (1 inverted spins but will have a favorable effect on recoveries from erect spins. The results of brief tests indicate that if a pilot is ejected during a spin while a spin-recovery parachute is extended and fully inflated, he will probably clear the tail parachute.

Relativistic Zeroth-Order Regular Approximation Combined with Nonhybrid and Hybrid Density Functional Theory: Performance for NMR Indirect Nuclear Spin-Spin Coupling in Heavy Metal Compounds.

PubMed

Moncho, Salvador; Autschbach, Jochen

2010-01-12

A benchmark study for relativistic density functional calculations of NMR spin-spin coupling constants has been performed. The test set contained 47 complexes with heavy metal atoms (W, Pt, Hg, Tl, Pb) with a total of 88 coupling constants involving one or two heavy metal atoms. One-, two-, three-, and four-bond spin-spin couplings have been computed at different levels of theory (nonhybrid vs hybrid DFT, scalar vs two-component relativistic). The computational model was based on geometries fully optimized at the BP/TZP scalar relativistic zeroth-order regular approximation (ZORA) and the conductor-like screening model (COSMO) to include solvent effects. The NMR computations also employed the continuum solvent model. Computations in the gas phase were performed in order to assess the importance of the solvation model. The relative median deviations between various computational models and experiment were found to range between 13% and 21%, with the highest-level computational model (hybrid density functional computations including scalar plus spin-orbit relativistic effects, the COSMO solvent model, and a Gaussian finite-nucleus model) performing best.

Rotational Invariance of the 2d Spin - Spin Correlation Function

NASA Astrophysics Data System (ADS)

Pinson, Haru

2012-09-01

At the critical temperature in the 2d Ising model on the square lattice, we establish the rotational invariance of the spin-spin correlation function using the asymptotics of the spin-spin correlation function along special directions (McCoy and Wu in the two dimensional Ising model. Harvard University Press, Cambridge, 1973) and the finite difference Hirota equation for which the spin-spin correlation function is shown to satisfy (Perk in Phys Lett A 79:3-5, 1980; Perk in Proceedings of III international symposium on selected topics in statistical mechanics, Dubna, August 22-26, 1984, JINR, vol II, pp 138-151, 1985).

Bifurcation analysis and phase diagram of a spin-string model with buckled states.

PubMed

Ruiz-Garcia, M; Bonilla, L L; Prados, A

2017-12-01

We analyze a one-dimensional spin-string model, in which string oscillators are linearly coupled to their two nearest neighbors and to Ising spins representing internal degrees of freedom. String-spin coupling induces a long-range ferromagnetic interaction among spins that competes with a spin-spin antiferromagnetic coupling. As a consequence, the complex phase diagram of the system exhibits different flat rippled and buckled states, with first or second order transition lines between states. This complexity translates to the two-dimensional version of the model, whose numerical solution has been recently used to explain qualitatively the rippled to buckled transition observed in scanning tunneling microscopy experiments with suspended graphene sheets. Here we describe in detail the phase diagram of the simpler one-dimensional model and phase stability using bifurcation theory. This gives additional insight into the physical mechanisms underlying the different phases and the behavior observed in experiments.

Fast spinning strings on η deformed AdS 5 × S 5

NASA Astrophysics Data System (ADS)

Banerjee, Aritra; Bhattacharyya, Arpan; Roychowdhury, Dibakar

2018-02-01

In this paper, considering the correspondence between spin chains and string sigma models, we explore the rotating string solutions over η deformed AdS 5 × S 5 in the so-called fast spinning limit. In our analysis, we focus only on the bosonic part of the full superstring action and compute the relevant limits on both ( R × S 3) η and ( R × S 5) η models. The resulting system reveals that in the fast spinning limit, the sigma model on η deformed S 5 could be approximately thought of as the continuum limit of anisotropic SU(3) Heisenberg spin chain model. We compute the energy for a certain class of spinning strings in deformed S 5 and we show that this energy can be mapped to that of a similar spinning string in the purely imaginary β deformed background.

Spin-flip transitions and departure from the Rashba model in the Au(111) surface

NASA Astrophysics Data System (ADS)

Ibañez-Azpiroz, Julen; Bergara, Aitor; Sherman, E. Ya.; Eiguren, Asier

2013-09-01

We present a detailed analysis of the spin-flip excitations induced by a periodic time-dependent electric field in the Rashba prototype Au(111) noble metal surface. Our calculations incorporate the full spinor structure of the spin-split surface states and employ a Wannier-based scheme for the spin-flip matrix elements. We find that the spin-flip excitations associated with the surface states exhibit an strong dependence on the electron momentum magnitude, a feature that is absent in the standard Rashba model [E. I. Rashba, Sov. Phys. Solid State 2, 1109 (1960)]. Furthermore, we demonstrate that the maximum of the calculated spin-flip absorption rate is about twice the model prediction. These results show that, although the Rashba model accurately describes the spectrum and spin polarization, it does not fully account for the dynamical properties of the surface states.

Bifurcation analysis and phase diagram of a spin-string model with buckled states

NASA Astrophysics Data System (ADS)

Ruiz-Garcia, M.; Bonilla, L. L.; Prados, A.

2017-12-01

We analyze a one-dimensional spin-string model, in which string oscillators are linearly coupled to their two nearest neighbors and to Ising spins representing internal degrees of freedom. String-spin coupling induces a long-range ferromagnetic interaction among spins that competes with a spin-spin antiferromagnetic coupling. As a consequence, the complex phase diagram of the system exhibits different flat rippled and buckled states, with first or second order transition lines between states. This complexity translates to the two-dimensional version of the model, whose numerical solution has been recently used to explain qualitatively the rippled to buckled transition observed in scanning tunneling microscopy experiments with suspended graphene sheets. Here we describe in detail the phase diagram of the simpler one-dimensional model and phase stability using bifurcation theory. This gives additional insight into the physical mechanisms underlying the different phases and the behavior observed in experiments.

Hierarchy of low-energy models of the electronic structure of cuprate HTSCs: The role of long-range spin-correlated hops

NASA Astrophysics Data System (ADS)

Val'kov, V. V.; Mitskan, V. A.; Dzebisashvili, D. M.; Barabanov, A. F.

2018-02-01

It is shown that for the three-band Emery p-d-model that reflects the real structure of the CuO2-plane of high-temperature superconductors in the regime of strong electron correlations, it is possible to carry out a sequence of reductions to the effective models reproducing low-energy features of elementary excitation spectrum and revealing the spin-polaron nature of the Fermi quasiparticles. The first reduction leads to the spin-fermion model in which the subsystem of spin moments, coupled by the exchange interaction and localized on copper ions, strongly interacts with oxygen holes. The second reduction deals with the transformation from the spin-fermion model to the φ-d-exchange model. An important feature of this transformation is the large energy of the φ-d-exchange coupling, which leads to the formation of spin polarons. The use of this fact allows us to carry out the third reduction, resulting in the t ˜-J˜ *-I -model. Its distinctive feature is the importance of spin-correlated hops as compared to the role of such processes in the commonly used t-J*-model derived from the Hubbard model. Based on the comparative analysis of the spectrum of Fermi excitations calculated for the obtained effective models of the CuO2-plane of high-temperature superconductors, the important role of the usually ignored long-range spin-correlated hops is determined.

Spin Ice

NASA Astrophysics Data System (ADS)

Bramwell, Steven T.; Gingras, Michel J. P.; Holdsworth, Peter C. W.

2013-03-01

Pauling's model of hydrogen disorder in water ice represents the prototype of a frustrated system. Over the years it has spawned several analogous models, including Anderson's model antiferromagnet and the statistical "vertex" models. Spin Ice is a sixteen vertex model of "ferromagnetic frustration" that is approximated by real materials, most notably the rare earth pyrochlores Ho2Ti2O7, Dy2Ti2O7 and Ho2Sn2O7. These "spin ice materials" have the Pauling zero point entropy and in all respects represent almost ideal realisations of Pauling's model. They provide experimentalists with unprecedented access to a wide variety of novel magnetic states and phase transitions that are located in different regions of the field-temperature phase diagram. They afford theoreticians the opportunity to explore many new features of the magnetic interactions and statistical mechanics of frustrated systems. This chapter is a comprehensive review of the physics -- both experimental and theoretical -- of spin ice. It starts with a discussion of the historic problem of water ice and its relation to spin ice and other frustrated magnets. The properties of spin ice are then discussed in three sections that deal with the zero field spin ice state, the numerous field-induced states (including the recently identified "kagomé ice") and the magnetic dynamics. Some materials related to spin ice are briefly described and the chapter is concluded with a short summary of spin ice physics.

Effective model with strong Kitaev interactions for α -RuCl3

NASA Astrophysics Data System (ADS)

Suzuki, Takafumi; Suga, Sei-ichiro

2018-04-01

We use an exact numerical diagonalization method to calculate the dynamical spin structure factors of three ab initio models and one ab initio guided model for a honeycomb-lattice magnet α -RuCl3 . We also use thermal pure quantum states to calculate the temperature dependence of the heat capacity, the nearest-neighbor spin-spin correlation function, and the static spin structure factor. From the results obtained from these four effective models, we find that, even when the magnetic order is stabilized at low temperature, the intensity at the Γ point in the dynamical spin structure factors increases with increasing nearest-neighbor spin correlation. In addition, we find that the four models fail to explain heat-capacity measurements whereas two of the four models succeed in explaining inelastic-neutron-scattering experiments. In the four models, when temperature decreases, the heat capacity shows a prominent peak at a high temperature where the nearest-neighbor spin-spin correlation function increases. However, the peak temperature in heat capacity is too low in comparison with that observed experimentally. To address these discrepancies, we propose an effective model that includes strong ferromagnetic Kitaev coupling, and we show that this model quantitatively reproduces both inelastic-neutron-scattering experiments and heat-capacity measurements. To further examine the adequacy of the proposed model, we calculate the field dependence of the polarized terahertz spectra, which reproduces the experimental results: the spin-gapped excitation survives up to an onset field where the magnetic order disappears and the response in the high-field region is almost linear. Based on these numerical results, we argue that the low-energy magnetic excitation in α -RuCl3 is mainly characterized by interactions such as off-diagonal interactions and weak Heisenberg interactions between nearest-neighbor pairs, rather than by the strong Kitaev interactions.

Spin-foam models and the physical scalar product

DOE Office of Scientific and Technical Information (OSTI.GOV)

Alesci, Emanuele; Centre de Physique Theorique de Luminy, Universite de la Mediterranee, F-13288 Marseille; Noui, Karim

2008-11-15

This paper aims at clarifying the link between loop quantum gravity and spin-foam models in four dimensions. Starting from the canonical framework, we construct an operator P acting on the space of cylindrical functions Cyl({gamma}), where {gamma} is the four-simplex graph, such that its matrix elements are, up to some normalization factors, the vertex amplitude of spin-foam models. The spin-foam models we are considering are the topological model, the Barrett-Crane model, and the Engle-Pereira-Rovelli model. If one of these spin-foam models provides a covariant quantization of gravity, then the associated operator P should be the so-called ''projector'' into physical statesmore » and its matrix elements should give the physical scalar product. We discuss the possibility to extend the action of P to any cylindrical functions on the space manifold.« less

Kinetic analysis of spin current contribution to spectrum of electromagnetic waves in spin-1/2 plasma. I. Dielectric permeability tensor for magnetized plasmas

NASA Astrophysics Data System (ADS)

Andreev, Pavel A.

2017-02-01

The dielectric permeability tensor for spin polarized plasmas is derived in terms of the spin-1/2 quantum kinetic model in six-dimensional phase space. Expressions for the distribution function and spin distribution function are derived in linear approximations on the path of dielectric permeability tensor derivation. The dielectric permeability tensor is derived for the spin-polarized degenerate electron gas. It is also discussed at the finite temperature regime, where the equilibrium distribution function is presented by the spin-polarized Fermi-Dirac distribution. Consideration of the spin-polarized equilibrium states opens possibilities for the kinetic modeling of the thermal spin current contribution in the plasma dynamics.

Dynamics of Topological Excitations in a Model Quantum Spin Ice

NASA Astrophysics Data System (ADS)

Huang, Chun-Jiong; Deng, Youjin; Wan, Yuan; Meng, Zi Yang

2018-04-01

We study the quantum spin dynamics of a frustrated X X Z model on a pyrochlore lattice by using large-scale quantum Monte Carlo simulation and stochastic analytic continuation. In the low-temperature quantum spin ice regime, we observe signatures of coherent photon and spinon excitations in the dynamic spin structure factor. As the temperature rises to the classical spin ice regime, the photon disappears from the dynamic spin structure factor, whereas the dynamics of the spinon remain coherent in a broad temperature window. Our results provide experimentally relevant, quantitative information for the ongoing pursuit of quantum spin ice materials.

Resonance measurement of nonlocal spin torque in a three-terminal magnetic device.

PubMed

Xue, Lin; Wang, Chen; Cui, Yong-Tao; Liu, Luqiao; Swander, A; Sun, J Z; Buhrman, R A; Ralph, D C

2012-04-06

A pure spin current generated within a nonlocal spin valve can exert a spin-transfer torque on a nanomagnet. This nonlocal torque enables new design schemes for magnetic memory devices that do not require the application of large voltages across tunnel barriers that can suffer electrical breakdown. Here we report a quantitative measurement of this nonlocal spin torque using spin-torque-driven ferromagnetic resonance. Our measurement agrees well with the prediction of an effective circuit model for spin transport. Based on this model, we suggest strategies for optimizing the strength of nonlocal torque. © 2012 American Physical Society

Checker Board Model predicts 5 Generations of Quarks

NASA Astrophysics Data System (ADS)

Lach, Theodore M., II

2002-10-01

The Checker Board Model (CBM) of the nucleus is a 2 Dimensional model that relies on the belief that nature is superbly symmetric and the belief that the synchronization of the 2 outer rotating quarks in the nucleons accounts for magnetic moment of the nucleons and that the magnetic flux from the nucleons couples (weaves) into the checker board array structures and this in addition to electrostatic forces of the rotating and stationary quarks accounts for the apparent strong nuclear force. The symmetry of the He nucleus, one might call it Super Symmetric, helps explain the stable structure of the alpha particle. A semi-classical (relativistic) approach was used to explain the mass of the proton and neutron, along with their magnetic moments and their absolute and relative sizes in terms of the above structure and two newly proposed quarks (1) : the "up" and the "dn" quarks, not to be confused with the lighter u and d quarks in the standard model. Using the prescribed 2D checkerboard arrays where protons go on dark squares and neutrons go on light squares, one is able to recreate all the known nuclei. This exercise came up with structures that could explain the rational for the Halo nuclei and why 9He was so unstable where as 8He was much more stable and 10He is not a bound structure. Since the heavy masses of the "up" and "dn" quark (237.31 MeV and 42.392 MeV respectively) did not fit within the standard model as candidates for u and d, a new model (New Physics) had to be invented that would explain why "up" and "dn" were so heavy. Trial and error resulted in the empirical fitting of these two new quarks into a scheme that placed them between the mass of u / d and the c / s quarks. This new particle physics model predicts that nature has 5 generations not 3. Perhaps it should be called the 5G model. The two new generations come from the "up" and "dn' quark and a much heavier generation of a 42.5 GeV "massive dn" or (Big Bottom, B') and 65 GeV "massive up" or (Big Top, T') quark. This model was uploaded to the lanl web server just before the Aug. 2000 NP meeting at Michigan State. (2) Subsequent versions of this paper explain the rational of the 27 GeV lepton, which this model dubbed the "gluon" and for that information please refer to pages 608 to 618 of the "Rise of the Standard Model", editors: Hoddeson, Brown, Riordan, and Dresden. NOTE: the 27 GeV lepton was predicted by this model and uploaded before the author read the Rise of the Standard Model, so indeed it was a prediction, not a fitting. Early on it was believed that the 27 GeV resonance was attributed to the finding of the gluon, yet today this is not the case and the standard model requires the gluon be massless. One key conflict between the 3G and 5G model is that the 3G model has established the mass of the "t" quark as 175 GeV based upon experimental findings, whereas the 5G model anticipates the "t" quark is hidden among the Upsilon mesons between 10 and 11 GeV. The recent find by CERN of an 113 GeV particle may end up being the meson of the combination of the massive "up" and massive "dn" (T' B'). The final convincing argument in favor of the 5G model is that all the masses of the quarks and leptons in this model are related with one another based upon a simple geometric mean. The masses of all the "up like" quarks fall on a straight line on semi-log paper, as do the "dn like" quarks, and the leptons. All three of these (equally spaced) curves come together at about 430 GeV. One last point, the upper bound masses of the neutrinos also fall on a straight line in this theory and also appear to join the other curves at about 430 GeV. The Checkerboard model has a close association with the Cluster Model, since the structures envisioned by the Cluster model are totally compatible with the CBM. Binding energies of the nuclei are also easily explained in this 2D model, see reference #1. (1). T.M. Lach, Checkerboard Structure of the Nucleus, Infinite Energy, Vol. 5, issue 30, (2000). (2). T.M. Lach, Masses of the Sub-Nuclear Particles, nucl-th/0008026, @http://xxx.lanl.gov/

Supplementary Investigation in the Free-Spinning Tunnel of a 1/24-Scale Model of the Grumman F9F-6 Airplane Incorporating only Flaperons for Lateral Control, TED No. NACA DE 364

NASA Technical Reports Server (NTRS)

Klinar, Walter J.; Lee, Henry A.

1954-01-01

A supplementary investigation was conducted in the Langley 20-foot free-spinning tunnel on a 1/24-scale model of the Grumman F9F-6 airplane. The primary purpose of the investigation was to reevaluate the spin-recovery characteristics of the airplane in view of the fact that the ailerons had been eliminated from the flaperon-aileron lateral control system of the airplane. A spin-tunnel investigation on a model of the earlier version of the F9F-6 airplane had indicated that use of ailerons with the spin (stick right in a right spin) was essential to insure recovery. The results indicate that with.ailerons eliminated, it may be difficult to obtain an erect developed spin but if a fully developed spin is obtained on the airplane, recovery therefrom may be difficult or impossible. Flaperon deflection should have little effect on spins or recoveries.

Quantum phase transitions in effective spin-ladder models for graphene zigzag nanoribbons

NASA Astrophysics Data System (ADS)

Koop, Cornelie; Wessel, Stefan

2017-10-01

We examine the magnetic correlations in quantum spin models that were derived recently as effective low-energy theories for electronic correlation effects on the edge states of graphene nanoribbons. For this purpose, we employ quantum Monte Carlo simulations to access the large-distance properties, accounting for quantum fluctuations beyond mean-field-theory approaches to edge magnetism. For certain chiral nanoribbons, antiferromagnetic interedge couplings were previously found to induce a gapped quantum disordered ground state of the effective spin model. We find that the extended nature of the intraedge couplings in the effective spin model for zigzag nanoribbons leads to a quantum phase transition at a large, finite value of the interedge coupling. This quantum critical point separates the quantum disordered region from a gapless phase of stable edge magnetism at weak intraedge coupling, which includes the ground states of spin-ladder models for wide zigzag nanoribbons. To study the quantum critical behavior, the effective spin model can be related to a model of two antiferromagnetically coupled Haldane-Shastry spin-half chains with long-ranged ferromagnetic intrachain couplings. The results for the critical exponents are compared also to several recent renormalization-group calculations for related long-ranged interacting quantum systems.

Entangled spin chain

NASA Astrophysics Data System (ADS)

Salberger, Olof; Korepin, Vladimir

We introduce a new model of interacting spin 1/2. It describes interactions of three nearest neighbors. The Hamiltonian can be expressed in terms of Fredkin gates. The Fredkin gate (also known as the controlled swap gate) is a computational circuit suitable for reversible computing. Our construction generalizes the model presented by Peter Shor and Ramis Movassagh to half-integer spins. Our model can be solved by means of Catalan combinatorics in the form of random walks on the upper half plane of a square lattice (Dyck walks). Each Dyck path can be mapped on a wave function of spins. The ground state is an equally weighted superposition of Dyck walks (instead of Motzkin walks). We can also express it as a matrix product state. We further construct a model of interacting spins 3/2 and greater half-integer spins. The models with higher spins require coloring of Dyck walks. We construct a SU(k) symmetric model (where k is the number of colors). The leading term of the entanglement entropy is then proportional to the square root of the length of the lattice (like in the Shor-Movassagh model). The gap closes as a high power of the length of the lattice [5, 11].

Central Limit Theorem for Exponentially Quasi-local Statistics of Spin Models on Cayley Graphs

NASA Astrophysics Data System (ADS)

Reddy, Tulasi Ram; Vadlamani, Sreekar; Yogeshwaran, D.

2018-04-01

Central limit theorems for linear statistics of lattice random fields (including spin models) are usually proven under suitable mixing conditions or quasi-associativity. Many interesting examples of spin models do not satisfy mixing conditions, and on the other hand, it does not seem easy to show central limit theorem for local statistics via quasi-associativity. In this work, we prove general central limit theorems for local statistics and exponentially quasi-local statistics of spin models on discrete Cayley graphs with polynomial growth. Further, we supplement these results by proving similar central limit theorems for random fields on discrete Cayley graphs taking values in a countable space, but under the stronger assumptions of α -mixing (for local statistics) and exponential α -mixing (for exponentially quasi-local statistics). All our central limit theorems assume a suitable variance lower bound like many others in the literature. We illustrate our general central limit theorem with specific examples of lattice spin models and statistics arising in computational topology, statistical physics and random networks. Examples of clustering spin models include quasi-associated spin models with fast decaying covariances like the off-critical Ising model, level sets of Gaussian random fields with fast decaying covariances like the massive Gaussian free field and determinantal point processes with fast decaying kernels. Examples of local statistics include intrinsic volumes, face counts, component counts of random cubical complexes while exponentially quasi-local statistics include nearest neighbour distances in spin models and Betti numbers of sub-critical random cubical complexes.

Quenching of dynamic nuclear polarization by spin-orbit coupling in GaAs quantum dots.

PubMed

Nichol, John M; Harvey, Shannon P; Shulman, Michael D; Pal, Arijeet; Umansky, Vladimir; Rashba, Emmanuel I; Halperin, Bertrand I; Yacoby, Amir

2015-07-17

The central-spin problem is a widely studied model of quantum decoherence. Dynamic nuclear polarization occurs in central-spin systems when electronic angular momentum is transferred to nuclear spins and is exploited in quantum information processing for coherent spin manipulation. However, the mechanisms limiting this process remain only partially understood. Here we show that spin-orbit coupling can quench dynamic nuclear polarization in a GaAs quantum dot, because spin conservation is violated in the electron-nuclear system, despite weak spin-orbit coupling in GaAs. Using Landau-Zener sweeps to measure static and dynamic properties of the electron spin-flip probability, we observe that the size of the spin-orbit and hyperfine interactions depends on the magnitude and direction of applied magnetic field. We find that dynamic nuclear polarization is quenched when the spin-orbit contribution exceeds the hyperfine, in agreement with a theoretical model. Our results shed light on the surprisingly strong effect of spin-orbit coupling in central-spin systems.

Flight Guidance System Requirements Specification

NASA Technical Reports Server (NTRS)

Miller, Steven P.; Tribble, Alan C.; Carlson, Timothy M.; Danielson, Eric J.

2003-01-01

This report describes a requirements specification written in the RSML-e language for the mode logic of a Flight Guidance System of a typical regional jet aircraft. This model was created as one of the first steps in a five-year project sponsored by the NASA Langley Research Center, Rockwell Collins Inc., and the Critical Systems Research Group of the University of Minnesota to develop new methods and tools to improve the safety of avionics designs. This model will be used to demonstrate the application of a variety of methods and techniques, including safety analysis of system and subsystem requirements, verification of key properties using theorem provers and model checkers, identification of potential sources mode confusion in system designs, partitioning of applications based on the criticality of system hazards, and autogeneration of avionics quality code. While this model is representative of the mode logic of a typical regional jet aircraft, it does not describe an actual or planned product. Several aspects of a full Flight Guidance System, such as recovery from failed sensors, have been omitted, and no claims are made regarding the accuracy or completeness of this specification.

Verification and Optimal Control of Context-Sensitive Probabilistic Boolean Networks Using Model Checking and Polynomial Optimization

PubMed Central

Hiraishi, Kunihiko

2014-01-01

One of the significant topics in systems biology is to develop control theory of gene regulatory networks (GRNs). In typical control of GRNs, expression of some genes is inhibited (activated) by manipulating external stimuli and expression of other genes. It is expected to apply control theory of GRNs to gene therapy technologies in the future. In this paper, a control method using a Boolean network (BN) is studied. A BN is widely used as a model of GRNs, and gene expression is expressed by a binary value (ON or OFF). In particular, a context-sensitive probabilistic Boolean network (CS-PBN), which is one of the extended models of BNs, is used. For CS-PBNs, the verification problem and the optimal control problem are considered. For the verification problem, a solution method using the probabilistic model checker PRISM is proposed. For the optimal control problem, a solution method using polynomial optimization is proposed. Finally, a numerical example on the WNT5A network, which is related to melanoma, is presented. The proposed methods provide us useful tools in control theory of GRNs. PMID:24587766

Model-Checking with Edge-Valued Decision Diagrams

NASA Technical Reports Server (NTRS)

Roux, Pierre; Siminiceanu, Radu I.

2010-01-01

We describe an algebra of Edge-Valued Decision Diagrams (EVMDDs) to encode arithmetic functions and its implementation in a model checking library along with state-of-the-art algorithms for building the transition relation and the state space of discrete state systems. We provide efficient algorithms for manipulating EVMDDs and give upper bounds of the theoretical time complexity of these algorithms for all basic arithmetic and relational operators. We also demonstrate that the time complexity of the generic recursive algorithm for applying a binary operator on EVMDDs is no worse than that of Multi-Terminal Decision Diagrams. We have implemented a new symbolic model checker with the intention to represent in one formalism the best techniques available at the moment across a spectrum of existing tools: EVMDDs for encoding arithmetic expressions, identity-reduced MDDs for representing the transition relation, and the saturation algorithm for reachability analysis. We compare our new symbolic model checking EVMDD library with the widely used CUDD package and show that, in many cases, our tool is several orders of magnitude faster than CUDD.

Using software security analysis to verify the secure socket layer (SSL) protocol

NASA Technical Reports Server (NTRS)

Powell, John D.

2004-01-01

nal Aeronautics and Space Administration (NASA) have tens of thousands of networked computer systems and applications. Software Security vulnerabilities present risks such as lost or corrupted data, information the3, and unavailability of critical systems. These risks represent potentially enormous costs to NASA. The NASA Code Q research initiative 'Reducing Software Security Risk (RSSR) Trough an Integrated Approach '' offers, among its capabilities, formal verification of software security properties, through the use of model based verification (MBV) to address software security risks. [1,2,3,4,5,6] MBV is a formal approach to software assurance that combines analysis of software, via abstract models, with technology, such as model checkers, that provide automation of the mechanical portions of the analysis process. This paper will discuss: The need for formal analysis to assure software systems with respect to software and why testing alone cannot provide it. The means by which MBV with a Flexible Modeling Framework (FMF) accomplishes the necessary analysis task. An example of FMF style MBV in the verification of properties over the Secure Socket Layer (SSL) communication protocol as a demonstration.

Investigation of Spinning and Tumbling Characteristics of a 1/20-Scale Model of the Consolidated Vultee XFY-1 Airplane in the Free-Spinning Tunnel, TED No. NACA DE 370

NASA Technical Reports Server (NTRS)

Lee, Henry A.

1952-01-01

An investigation has been conducted in the Langley 20-foot free-spinning tunnel on a l/20-scale model of the Consolidated Vultee XFY-1 airplane with a windmilling propeller simulated to determine the effects of control setting and movements upon the erect spin and recovery characteristics for a range of airplane-loading conditions. The effects on the model's spin-recovery characteristics of removing the lower vertical tail, removing the gun pods, and fixing the rudders at neutral were also investigated briefly. The investigation included determination of the size parachute required for emergency recovery from demonstration spins. The tumbling tendencies of the model were also investigated. Brief static force tests were made to determine the aerodynamic characteristics in pitch at high angles of attack. The investigation indicated that the spin and recovery characteristics of the airplane with propeller windmilling will be satisfactory for all loading conditions if recovery is attempted by full rudder reversal accompanied by simultaneous movement of the stick laterally to full with the spin (stick right in a right spin) and longitudinally to neutral. Inverted spins should be satisfactorily terminated by fully reversing the rudder followed immediately by moving the stick laterally towards the forward rudder pedal and longitudinally to neutral. Removal of the gun pods or fixing the rudders at neutral will not adversely affect the airplane's spin-recovery characteristics, but removal of the lower vertical tail will result in unsatisfactory spin-recovery characteristics. The model-test results showed that a 13.3-foot wing-tip conventional parachute (drag coefficient approximately 0.7) should be effective as an emergency spin-recovery device during demonstration spins of the airplane. It was indicated that the airplane should not tumble and that no unusual longitudinal-trim characteristics should be obtained for the center-of-gravity positions investigated.

A Probabilistic Model of Spin and Spin Measurements

NASA Astrophysics Data System (ADS)

Niehaus, Arend

2016-01-01

Several theoretical publications on the Dirac equation published during the last decades have shown that, an interpretation is possible, which ascribes the origin of electron spin and magnetic moment to an autonomous circular motion of the point-like charged particle around a fixed centre. In more recent publications an extension of the original so called "Zitterbewegung Interpretation" of quantum mechanics was suggested, in which the spin results from an average of instantaneous spin vectors over a Zitterbewegung period. We argue that, the corresponding autonomous motion of the electron should, if it is real, determine non-relativistic spin measurements. Such a direct connection with the established formal quantum mechanical description of spin measurements, into which spin is introduced as a "non-classical" quantity has, to our knowledge, not been reported. In the present work we show that, under certain "model assumptions" concerning the proposed autonomous motion, results of spin measurements, including measurements of angular correlations in singlet systems, can indeed be correctly described using classical probabilities. The success of the model is evidence for the "reality" of the assumed autonomous motion. The resulting model violates the Bell—inequalities to the same extent as quantum mechanics.

Influence of the Verwey Transition on the Spin-Wave Dispersion of Magnetite

DOE Office of Scientific and Technical Information (OSTI.GOV)

McQueeny, R. J.; Yethiraj, Mohana; Montfrooij, W.

Inelastic neutron-scattering measurements of the spin-wave spectrum of magnetite (Fe{sub 3}O{sub 4}) that shed new light on the Verwey transition problem are presented. Above the Verwey transition, the spin waves can fit a simple Heisenberg model. Below TV, a large gap (8?meV) forms in the acoustic spin-wave branch at q = (0,0,1/2) and E = 43?meV. Heisenberg models with large unit cells were used to examine the spin waves when the superexchange is modified to reflect the crystallographic symmetry lowering due to either atomic distortions or charge ordering and find that neither of these models predicts the spin-wave gap.

Antiresonance induced spin-polarized current generation

NASA Astrophysics Data System (ADS)

Yin, Sun; Min, Wen-Jing; Gao, Kun; Xie, Shi-Jie; Liu, De-Sheng

2011-12-01

According to the one-dimensional antiresonance effect (Wang X R, Wang Y and Sun Z Z 2003 Phys. Rev. B 65 193402), we propose a possible spin-polarized current generation device. Our proposed model consists of one chain and an impurity coupling to the chain. The energy level of the impurity can be occupied by an electron with a specific spin, and the electron with such a spin is blocked because of the antiresonance effect. Based on this phenomenon our model can generate the spin-polarized current flowing through the chain due to different polarization rates. On the other hand, the device can also be used to measure the generated spin accumulation. Our model is feasible with today's technology.

Quantum model of a solid-state spin qubit: Ni cluster on a silicon surface by the generalized spin Hamiltonian and X-ray absorption spectroscopy investigations

NASA Astrophysics Data System (ADS)

Farberovich, Oleg V.; Mazalova, Victoria L.; Soldatov, Alexander V.

2015-11-01

We present here the quantum model of a Ni solid-state electron spin qubit on a silicon surface with the use of a density-functional scheme for the calculation of the exchange integrals in the non-collinear spin configurations in the generalized spin Hamiltonian (GSH) with the anisotropic exchange coupling parameters linking the nickel ions with a silicon substrate. In this model the interaction of a spin qubit with substrate is considered in GSH at the calculation of exchange integrals Jij of the nanosystem Ni7-Si in the one-electron approach taking into account chemical bonds of all Si-atoms of a substrate (environment) with atoms of the Ni7-cluster. The energy pattern was found from the effective GSH Hamiltonian acting in the restricted spin space of the Ni ions by the application of the irreducible tensor operators (ITO) technique. In this paper we offer the model of the quantum solid-state N-spin qubit based on the studying of the spin structure and the spin-dynamics simulations of the 3d-metal Ni clusters on the silicon surface. The solution of the problem of the entanglement between spin states in the N-spin systems is becoming more interesting when considering clusters or molecules with a spectral gap in their density of states. For quantifying the distribution of the entanglement between the individual spin eigenvalues (modes) in the spin structure of the N-spin system we use the density of entanglement (DOE). In this study we have developed and used the advanced high-precision numerical techniques to accurately assess the details of the decoherence process governing the dynamics of the N-spin qubits interacting with a silicon surface. We have studied the Rabi oscillations to evaluate the N-spin qubits system as a function of the time and the magnetic field. We have observed the stabilized Rabi oscillations and have stabilized the quantum dynamical qubit state and Rabi driving after a fixed time (0.327 μs). The comparison of the energy pattern with the anisotropic exchange models conventionally used for the analysis of this system and, with the results of the experimental XANES spectra, shows that our complex investigations provide a good description of the pattern of the spin levels and the spin structures of the nanomagnetic Ni7 qubit. The results are discussed in the view of the general problem of the solid-state spin qubits and the spin structure of the Ni cluster.

Tilting Styx and Nix but not Uranus with a Spin-Precession-Mean-motion resonance

NASA Astrophysics Data System (ADS)

Quillen, Alice C.; Chen, Yuan-Yuan; Noyelles, Benoît; Loane, Santiago

2018-02-01

A Hamiltonian model is constructed for the spin axis of a planet perturbed by a nearby planet with both planets in orbit about a star. We expand the planet-planet gravitational potential perturbation to first order in orbital inclinations and eccentricities, finding terms describing spin resonances involving the spin precession rate and the two planetary mean motions. Convergent planetary migration allows the spinning planet to be captured into spin resonance. With initial obliquity near zero, the spin resonance can lift the planet's obliquity to near 90° or 180° depending upon whether the spin resonance is first or zeroth order in inclination. Past capture of Uranus into such a spin resonance could give an alternative non-collisional scenario accounting for Uranus's high obliquity. However, we find that the time spent in spin resonance must be so long that this scenario cannot be responsible for Uranus's high obliquity. Our model can be used to study spin resonance in satellite systems. Our Hamiltonian model explains how Styx and Nix can be tilted to high obliquity via outward migration of Charon, a phenomenon previously seen in numerical simulations.

Effects of several factors on theoretical predictions of airplane spin characteristics. [dynamic models

NASA Technical Reports Server (NTRS)

Bihrle, W., Jr.; Barnhart, B.

1974-01-01

The influence of different mathematical and aerodynamic models on computed spin motion was investigated along with the importance of some of the aerodynamic and nonaerodynamic quantities defined in these models. An analytical technique was used which included the aerodynamic forces and moments acting on a spinning aircraft due to steady rotational flow and the contribution of the rotary derivatives to the oscillatory component of the total angular rates. It was shown that (1) during experimental-analytical correlation studies, the flight-recorded control time histories must be faithfully duplicated since the spinning motion can be sensitive to a small change in the application of the spin entry controls; (2) an error in the assumed inertias, yawing moments at high angle of attack, and initial spin entry bank angle do not influence the developed spin significantly; (3) damping in pitch derivatives and the center of gravity location play a role in the spinning motion; and (4) the experimental spin investigations conducted in a constant atmospheric density environment duplicate the Froude number only at the initial full-scale spin altitude (since the full-scale airplane at high altitudes experiences large density changes during the spin.)

Competing Spin Liquids and Hidden Spin-Nematic Order in Spin Ice with Frustrated Transverse Exchange

NASA Astrophysics Data System (ADS)

Taillefumier, Mathieu; Benton, Owen; Yan, Han; Jaubert, L. D. C.; Shannon, Nic

2017-10-01

Frustration in magnetic interactions can give rise to disordered ground states with subtle and beautiful properties. The spin ices Ho2 Ti2 O7 and Dy2 Ti2 O7 exemplify this phenomenon, displaying a classical spin-liquid state, with fractionalized magnetic-monopole excitations. Recently, there has been great interest in closely related "quantum spin-ice" materials, following the realization that anisotropic exchange interactions could convert spin ice into a massively entangled, quantum spin liquid, where magnetic monopoles become the charges of an emergent quantum electrodynamics. Here we show that even the simplest model of a quantum spin ice, the XXZ model on the pyrochlore lattice, can realize a still-richer scenario. Using a combination of classical Monte Carlo simulation, semiclassical molecular-dynamics simulation, and analytic field theory, we explore the properties of this model for frustrated transverse exchange. We find not one, but three competing forms of spin liquid, as well as a phase with hidden, spin-nematic order. We explore the experimental signatures of each of these different states, making explicit predictions for inelastic neutron scattering. These results show an intriguing similarity to experiments on a range of pyrochlore oxides.

Spinon dynamics in quantum integrable antiferromagnets

NASA Astrophysics Data System (ADS)

Vlijm, R.; Caux, J.-S.

2016-05-01

The excitations of the Heisenberg antiferromagnetic spin chain in zero field are known as spinons. As pairwise-created fractionalized excitations, spinons are important in the understanding of inelastic neutron scattering experiments in (quasi-)one-dimensional materials. In the present paper, we consider the real space-time dynamics of spinons originating from a local spin flip on the antiferromagnetic ground state of the (an)isotropic Heisenberg spin-1/2 model and the Babujan-Takhtajan spin-1 model. By utilizing algebraic Bethe ansatz methods at finite system size to compute the expectation value of the local magnetization and spin-spin correlations, spinons are visualized as propagating domain walls in the antiferromagnetic spin ordering with anisotropy dependent behavior. The spin-spin correlation after the spin flip displays a light cone, satisfying the Lieb-Robinson bound for the propagation of correlations at the spinon velocity.

Spatiotemporal access model based on reputation for the sensing layer of the IoT.

PubMed

Guo, Yunchuan; Yin, Lihua; Li, Chao; Qian, Junyan

2014-01-01

Access control is a key technology in providing security in the Internet of Things (IoT). The mainstream security approach proposed for the sensing layer of the IoT concentrates only on authentication while ignoring the more general models. Unreliable communications and resource constraints make the traditional access control techniques barely meet the requirements of the sensing layer of the IoT. In this paper, we propose a model that combines space and time with reputation to control access to the information within the sensing layer of the IoT. This model is called spatiotemporal access control based on reputation (STRAC). STRAC uses a lattice-based approach to decrease the size of policy bases. To solve the problem caused by unreliable communications, we propose both nondeterministic authorizations and stochastic authorizations. To more precisely manage the reputation of nodes, we propose two new mechanisms to update the reputation of nodes. These new approaches are the authority-based update mechanism (AUM) and the election-based update mechanism (EUM). We show how the model checker UPPAAL can be used to analyze the spatiotemporal access control model of an application. Finally, we also implement a prototype system to demonstrate the efficiency of our model.

The influence of further-neighbor spin-spin interaction on a ground state of 2D coupled spin-electron model in a magnetic field

NASA Astrophysics Data System (ADS)

Čenčariková, Hana; Strečka, Jozef; Gendiar, Andrej; Tomašovičová, Natália

2018-05-01

An exhaustive ground-state analysis of extended two-dimensional (2D) correlated spin-electron model consisting of the Ising spins localized on nodal lattice sites and mobile electrons delocalized over pairs of decorating sites is performed within the framework of rigorous analytical calculations. The investigated model, defined on an arbitrary 2D doubly decorated lattice, takes into account the kinetic energy of mobile electrons, the nearest-neighbor Ising coupling between the localized spins and mobile electrons, the further-neighbor Ising coupling between the localized spins and the Zeeman energy. The ground-state phase diagrams are examined for a wide range of model parameters for both ferromagnetic as well as antiferromagnetic interaction between the nodal Ising spins and non-zero value of external magnetic field. It is found that non-zero values of further-neighbor interaction leads to a formation of new quantum states as a consequence of competition between all considered interaction terms. Moreover, the new quantum states are accompanied with different magnetic features and thus, several kinds of field-driven phase transitions are observed.

Controlling measurement-induced nonlocality in the Heisenberg XX model by three-spin interactions

NASA Astrophysics Data System (ADS)

Xie, Yu-Xia; Sun, Yu-Hang; Li, Zhao

2018-01-01

We investigate the well-defined measures of measurement-induced nonlocality (MIN) for thermal states of the transverse field XX model, with the addition of three-spin interaction terms being introduced. The results showed that the MINs are very sensitive to system parameters of the chain. The three-spin interactions can serve as flexible parameters for enhancing MINs of the boundary spins, and the maximum enhancement achievable by varying strengths of the three-spin interactions are different for the chain with different number of spins.

Land Desertification and it’s Control in Gonghe Basin of Qinghai Plateau, China

NASA Astrophysics Data System (ADS)

Zhang, D.; Gao, S.; Lu, R.

2009-12-01

Land desertification is an important environmental and social-economic problems that threatening people’s living conditions and impacting social sustainable development. The Gonghe basin in Qinghai Plateau is a fragile cold alpine area which is one of the places seriously threatened by desertification in China. This paper selected Gonghe basin as a study area to study land sandy desertification and its controlling measures. The engineering measures for sandy desertification control include setting clay sand barrier, Salix cheilophila sand barrier, Tamarix sand barrier, Artemisia sand barrier and straw-checker sand-barriers to fix dunes; the biological measures include closure for natural vegetation recovery, direct seeding forestation, transplanting seedlings, and so on. The combination of engineering and biologic measures can fix dunes 2~3 years earlier than the common single measure; and the costs were basically identical. A synthesized evaluation system established based on experimental results and experience in recent years indicated that the effectiveness of the four kinds of sand barrier for prevention and control of sand in study area were: Tamarix sand barrier > Artemisia sand barrier > clay sand barrier > straw-checker sand-barriers. In addition, different optimized management model can be selected according to local material and geographical place. New plants such as Salix cheilophila and Tamarix, which are available in study area, can change from dead sand barrier to live one set in proper seasons, changing engineering measure to biological one directly speeds the progress of forestation and dunes fixation. In addition, we developed new technique of deep planting Salix cheilophila and Tamarix with their long stem, which can effectively resist drought. We found that it had lower cost and higher live rate, and has a better sand prevention effect than deep planting of Poplar. Finally we choose the optimize management model as follows: Artemisia direct seeding > Caragana direct seeding, Tamarix cutting and seedling > Salix cheilophila deep planting, Sea-buckthorn seedling > Tamarix deep planting > Tamarix seedling > Poplar deep planting > Salix cheilophila seedling > Poplar seedling. It has resolved the key problem of control sand flow speed and low efficiency, sand burying and wind erosion and low conservation rate for forestation in the sandy area.

Spin-tunnel investigation of the spinning characteristics of typical single-engine general aviation airplane designs. 2: Low-wing model A; tail parachute diameter and canopy distance for emergency spin recovery

NASA Technical Reports Server (NTRS)

Burk, S. M., Jr.; Bowman, J. S., Jr.; White, W. L.

1977-01-01

A spin tunnel study is reported on a scale model of a research airplane typical of low-wing, single-engine, light general aviation airplanes to determine the tail parachute diameter and canopy distance (riser length plus suspension-line length) required for energency spin recovery. Nine tail configurations were tested, resulting in a wide range of developed spin conditions, including steep spins and flat spins. The results indicate that the full-scale parachute diameter required for satisfactory recovery from the most critical conditions investigated is about 3.2 m and that the canopy distance, which was found to be critical for flat spins, should be between 4.6 and 6.1 m.

Spin Funneling for Enhanced Spin Injection into Ferromagnets

PubMed Central

Sayed, Shehrin; Diep, Vinh Q.; Camsari, Kerem Yunus; Datta, Supriyo

2016-01-01

It is well-established that high spin-orbit coupling (SOC) materials convert a charge current density into a spin current density which can be used to switch a magnet efficiently and there is increasing interest in identifying materials with large spin Hall angle for lower switching current. Using experimentally benchmarked models, we show that composite structures can be designed using existing spin Hall materials such that the effective spin Hall angle is larger by an order of magnitude. The basic idea is to funnel spins from a large area of spin Hall material into a small area of ferromagnet using a normal metal with large spin diffusion length and low resistivity like Cu or Al. We show that this approach is increasingly effective as magnets get smaller. We avoid unwanted charge current shunting by the low resistive NM layer utilizing the newly discovered phenomenon of pure spin conduction in ferromagnetic insulators via magnon diffusion. We provide a spin circuit model for magnon diffusion in FMI that is benchmarked against recent experiments and theory. PMID:27374496

Spin Funneling for Enhanced Spin Injection into Ferromagnets

NASA Astrophysics Data System (ADS)

Sayed, Shehrin; Diep, Vinh Q.; Camsari, Kerem Yunus; Datta, Supriyo

2016-07-01

It is well-established that high spin-orbit coupling (SOC) materials convert a charge current density into a spin current density which can be used to switch a magnet efficiently and there is increasing interest in identifying materials with large spin Hall angle for lower switching current. Using experimentally benchmarked models, we show that composite structures can be designed using existing spin Hall materials such that the effective spin Hall angle is larger by an order of magnitude. The basic idea is to funnel spins from a large area of spin Hall material into a small area of ferromagnet using a normal metal with large spin diffusion length and low resistivity like Cu or Al. We show that this approach is increasingly effective as magnets get smaller. We avoid unwanted charge current shunting by the low resistive NM layer utilizing the newly discovered phenomenon of pure spin conduction in ferromagnetic insulators via magnon diffusion. We provide a spin circuit model for magnon diffusion in FMI that is benchmarked against recent experiments and theory.

Preliminary Tests in the NACA Free-Spinning Wind Tunnel

NASA Technical Reports Server (NTRS)

Zimmerman, C H

1937-01-01

Typical models and the testing technique used in the NACA free-spinning wind tunnel are described in detail. The results of tests on two models afford a comparison between the spinning characteristics of scale models in the tunnel and of the airplanes that they represent.

Magnetic properties of magnetic bilayer Kekulene structure: A Monte Carlo study

NASA Astrophysics Data System (ADS)

Jabar, A.; Masrour, R.

2018-06-01

In the present work, we have studied the magnetic properties of magnetic bilayer Kekulene structure with mixed spin-5/2 and spin-2 Ising model using Monte Carlo study. The magnetic phase diagrams of mixed spins Ising model have been given. The thermal total, partial magnetization and magnetic susceptibilities of the mixed spin-5/2 and spin-2 Ising model on a magnetic bilayer Kekulene structure are obtained. The transition temperature has been deduced. The effect of crystal field and exchange interactions on the this bilayers has been studied. The partial and total magnetic hysteresis cycles of the mixed spin-5/2 and spin-2 Ising model on a magnetic bilayer Kekulene structure have been given. The superparamagnetism behavior is observed in magnetic bilayer Kekulene structure. The magnetic coercive field decreases with increasing the exchange interactions between σ-σ and temperatures values and increases with increasing the absolute value of exchange interactions between σ-S. The multiple hysteresis behavior appears.

Detection of single electron spin resonance in a double quantum dota)

NASA Astrophysics Data System (ADS)

Koppens, F. H. L.; Buizert, C.; Vink, I. T.; Nowack, K. C.; Meunier, T.; Kouwenhoven, L. P.; Vandersypen, L. M. K.

2007-04-01

Spin-dependent transport measurements through a double quantum dot are a valuable tool for detecting both the coherent evolution of the spin state of a single electron, as well as the hybridization of two-electron spin states. In this article, we discuss a model that describes the transport cycle in this regime, including the effects of an oscillating magnetic field (causing electron spin resonance) and the effective nuclear fields on the spin states in the two dots. We numerically calculate the current flow due to the induced spin flips via electron spin resonance, and we study the detector efficiency for a range of parameters. The experimental data are compared with the model and we find a reasonable agreement.

Unveiling the thermal entanglement in a mixed-spin XXZ model with Dzyaloshinskii-Moriya interaction under a homogeneous magnetic field

NASA Astrophysics Data System (ADS)

Liu, Cheng-Cheng; Xu, Shuai; He, Juan; Ye, Liu

2015-10-01

We analytically investigate the thermal entanglement of three-mixed-spin (1/2, 1, 1/2) XXZ model with the DM interaction under an external magnetic field B. Two different cases are considered: one subsystem (1/2, 1/2) consists of two spin-1/2 fermions and the other subsystem (1/2, 1) contains a spin-1/2 fermion and a spin-1 boson. It is shown that the DM interaction parameter D, the external magnetic field strength B and coupling constant J have different effects on Fermi and mixed Fermi-Bose systems. All of the factors mentioned above can be utilized to control entanglement switch of any two particles in mixed spins model.

Microscopic theory of the nearest-neighbor valence bond sector of the spin-1/2 kagome antiferromagnet

NASA Astrophysics Data System (ADS)

Ralko, Arnaud; Mila, Frédéric; Rousochatzakis, Ioannis

2018-03-01

The spin-1/2 Heisenberg model on the kagome lattice, which is closely realized in layered Mott insulators such as ZnCu3(OH) 6Cl2 , is one of the oldest and most enigmatic spin-1/2 lattice models. While the numerical evidence has accumulated in favor of a quantum spin liquid, the debate is still open as to whether it is a Z2 spin liquid with very short-range correlations (some kind of resonating valence bond spin liquid), or an algebraic spin liquid with power-law correlations. To address this issue, we have pushed the program started by Rokhsar and Kivelson in their derivation of the effective quantum dimer model description of Heisenberg models to unprecedented accuracy for the spin-1/2 kagome, by including all the most important virtual singlet contributions on top of the orthogonalization of the nearest-neighbor valence bond singlet basis. Quite remarkably, the resulting picture is a competition between a Z2 spin liquid and a diamond valence bond crystal with a 12-site unit cell, as in the density-matrix renormalization group simulations of Yan et al. Furthermore, we found that, on cylinders of finite diameter d , there is a transition between the Z2 spin liquid at small d and the diamond valence bond crystal at large d , the prediction of the present microscopic description for the two-dimensional lattice. These results show that, if the ground state of the spin-1/2 kagome antiferromagnet can be described by nearest-neighbor singlet dimers, it is a diamond valence bond crystal, and, a contrario, that, if the system is a quantum spin liquid, it has to involve long-range singlets, consistent with the algebraic spin liquid scenario.

Influence of spin creepage and contact angle on curve squeal: A numerical approach

NASA Astrophysics Data System (ADS)

Zenzerovic, I.; Kropp, W.; Pieringer, A.

2018-04-01

Curve squeal is a loud tonal sound that may arise when a railway vehicle negotiates a tight curve. Due to the nonlinear nature of squeal, time-domain models provide a higher degree of accuracy in comparison to frequency-domain models and also enable the determination of squeal amplitudes. In the present paper, a previously developed engineering time-domain model for curve squeal is extended to include the effects of the contact angle and spin creepage. The extensions enable the evaluation of more realistic squeal cases with the computationally efficient model. The model validation against Kalker's variational contact model shows good agreement between the models. Results of studies on the influence of spin creepage and contact angle show that the contact angle has a significant influence on the vertical-lateral dynamics coupling and, therefore, influences both squeal amplitude and frequency. Spin creepage mainly influences processes in the contact, therefore influencing the tangential contact force amplitude. In the combined spin-contact angle study the spin creepage value is kinematically related to the contact angle value. Results indicate that the influence of the contact angle is dominant over the influence of spin creepage. In general, results indicate that the most crucial factors in squeal are those that influence the dynamics coupling: the contact angle, wheel/rail contact positions and friction.

Magnus effects on spinning transonic missiles

NASA Technical Reports Server (NTRS)

Seginer, A.; Rosenwasser, I.

1983-01-01

Magnus forces and moments were measured on a basic-finner model spinning in transonic flow. Spin was induced by canted fins or by full-span or semi-span, outboard and inboard roll controls. Magnus force and moment reversals were caused by Mach number, reduced spin rate, and angle of attack variations. Magnus center of pressure was found to be independent of the angle of attack but varied with the Mach number and model configuration or reduced spin rate.

Free-Spinning-Tunnel Tests of a 1/27-Scale Model of the Douglas XF3D-1 Airplane, TED No. NACA DE 312

NASA Technical Reports Server (NTRS)

Scher, Stanley H.

1947-01-01

Free-spinning-tunnel tests have been made on a 1/27-scale model of the Douglas XF3D-1 airplane to confirm a preliminary evaluation made of the airplane spin and recovery characteristics and previously reported. Recovery characteristics were satisfactory for erect and inverted spins when the model was in the clean condition. When the slow-down brakes were open, recoveries were slow. The pedal force necessary to reverse the airplane rudder during a spin will be within the physical capabilities of the pilot. A 10-foot-diameter parachute attached to the tail of the airplane (laid-out-flat diameter, drag coefficient 0.7) or a 4.5-foot-diameter parachute attached to the outboard wing tip will be satisfactory for emergency spin recovery from demonstration spins. If it becomes necessary for the crew to abandon the airplane during a spin, they should leave from the outboard side of the cockpit. The test results indicated spin and recovery characteristics generally similar to those indicated in the preliminary evaluation.

Improved Analysis of GW150914 Using a Fully Spin-Precessing Waveform Model

NASA Astrophysics Data System (ADS)

Abbott, B. P.; Abbott, R.; Abbott, T. D.; Abernathy, M. R.; Acernese, F.; Ackley, K.; Adams, C.; Adams, T.; Addesso, P.; Adhikari, R. X.; Adya, V. B.; Affeldt, C.; Agathos, M.; Agatsuma, K.; Aggarwal, N.; Aguiar, O. D.; Aiello, L.; Ain, A.; Ajith, P.; Allen, B.; Allocca, A.; Altin, P. A.; Anderson, S. B.; Anderson, W. G.; Arai, K.; Araya, M. C.; Arceneaux, C. C.; Areeda, J. S.; Arnaud, N.; Arun, K. G.; Ascenzi, S.; Ashton, G.; Ast, M.; Aston, S. M.; Astone, P.; Aufmuth, P.; Aulbert, C.; Babak, S.; Bacon, P.; Bader, M. K. M.; Baker, P. T.; Baldaccini, F.; Ballardin, G.; Ballmer, S. W.; Barayoga, J. C.; Barclay, S. E.; Barish, B. C.; Barker, D.; Barone, F.; Barr, B.; Barsotti, L.; Barsuglia, M.; Barta, D.; Bartlett, J.; Bartos, I.; Bassiri, R.; Basti, A.; Batch, J. C.; Baune, C.; Bavigadda, V.; Bazzan, M.; Bejger, M.; Bell, A. S.; Berger, B. K.; Bergmann, G.; Berry, C. P. L.; Bersanetti, D.; Bertolini, A.; Betzwieser, J.; Bhagwat, S.; Bhandare, R.; Bilenko, I. A.; Billingsley, G.; Birch, J.; Birney, R.; Birnholtz, O.; Biscans, S.; Bisht, A.; Bitossi, M.; Biwer, C.; Bizouard, M. A.; Blackburn, J. K.; Blair, C. D.; Blair, D. G.; Blair, R. M.; Bloemen, S.; Bock, O.; Boer, M.; Bogaert, G.; Bogan, C.; Bohe, A.; Bond, C.; Bondu, F.; Bonnand, R.; Boom, B. A.; Bork, R.; Boschi, V.; Bose, S.; Bouffanais, Y.; Bozzi, A.; Bradaschia, C.; Brady, P. R.; Braginsky, V. B.; Branchesi, M.; Brau, J. E.; Briant, T.; Brillet, A.; Brinkmann, M.; Brisson, V.; Brockill, P.; Broida, J. E.; Brooks, A. F.; Brown, D. A.; Brown, D. D.; Brown, N. M.; Brunett, S.; Buchanan, C. C.; Buikema, A.; Bulik, T.; Bulten, H. J.; Buonanno, A.; Buskulic, D.; Buy, C.; Byer, R. L.; Cabero, M.; Cadonati, L.; Cagnoli, G.; Cahillane, C.; Calderón Bustillo, J.; Callister, T.; Calloni, E.; Camp, J. B.; Cannon, K. C.; Cao, J.; Capano, C. D.; Capocasa, E.; Carbognani, F.; Caride, S.; Casanueva Diaz, C.; Casentini, J.; Caudill, S.; Cavaglià, M.; Cavalier, F.; Cavalieri, R.; Cella, G.; Cepeda, C. B.; Cerboni Baiardi, L.; Cerretani, G.; Cesarini, E.; Chamberlin, S. J.; Chan, M.; Chao, S.; Charlton, P.; Chassande-Mottin, E.; Cheeseboro, B. D.; Chen, H. Y.; Chen, Y.; Cheng, C.; Chincarini, A.; Chiummo, A.; Cho, H. S.; Cho, M.; Chow, J. H.; Christensen, N.; Chu, Q.; Chua, S.; Chung, S.; Ciani, G.; Clara, F.; Clark, J. A.; Cleva, F.; Coccia, E.; Cohadon, P.-F.; Colla, A.; Collette, C. G.; Cominsky, L.; Constancio, M.; Conte, A.; Conti, L.; Cook, D.; Corbitt, T. R.; Cornish, N.; Corsi, A.; Cortese, S.; Costa, C. A.; Coughlin, M. W.; Coughlin, S. B.; Coulon, J.-P.; Countryman, S. T.; Couvares, P.; Cowan, E. E.; Coward, D. M.; Cowart, M. J.; Coyne, D. C.; Coyne, R.; Craig, K.; Creighton, J. D. E.; Cripe, J.; Crowder, S. G.; Cumming, A.; Cunningham, L.; Cuoco, E.; Dal Canton, T.; Danilishin, S. L.; D'Antonio, S.; Danzmann, K.; Darman, N. S.; Dasgupta, A.; Da Silva Costa, C. F.; Dattilo, V.; Dave, I.; Davier, M.; Davies, G. S.; Daw, E. J.; Day, R.; De, S.; DeBra, D.; Debreczeni, G.; Degallaix, J.; De Laurentis, M.; Deléglise, S.; Del Pozzo, W.; Denker, T.; Dent, T.; Dergachev, V.; De Rosa, R.; DeRosa, R. T.; DeSalvo, R.; Devine, R. C.; Dhurandhar, S.; Díaz, M. C.; Di Fiore, L.; Di Giovanni, M.; Di Girolamo, T.; Di Lieto, A.; Di Pace, S.; Di Palma, I.; Di Virgilio, A.; Dolique, V.; Donovan, F.; Dooley, K. L.; Doravari, S.; Douglas, R.; Downes, T. P.; Drago, M.; Drever, R. W. P.; Driggers, J. C.; Ducrot, M.; Dwyer, S. E.; Edo, T. B.; Edwards, M. C.; Effler, A.; Eggenstein, H.-B.; Ehrens, P.; Eichholz, J.; Eikenberry, S. S.; Engels, W.; Essick, R. C.; Etienne, Z.; Etzel, T.; Evans, M.; Evans, T. M.; Everett, R.; Factourovich, M.; Fafone, V.; Fair, H.; Fairhurst, S.; Fan, X.; Fang, Q.; Farinon, S.; Farr, B.; Farr, W. M.; Fauchon-Jones, E.; Favata, M.; Fays, M.; Fehrmann, H.; Fejer, M. M.; Fenyvesi, E.; Ferrante, I.; Ferreira, E. C.; Ferrini, F.; Fidecaro, F.; Fiori, I.; Fiorucci, D.; Fisher, R. P.; Flaminio, R.; Fletcher, M.; Fournier, J.-D.; Frasca, S.; Frasconi, F.; Frei, Z.; Freise, A.; Frey, R.; Frey, V.; Fritschel, P.; Frolov, V. V.; Fulda, P.; Fyffe, M.; Gabbard, H. A. G.; Gaebel, S.; Gair, J. R.; Gammaitoni, L.; Gaonkar, S. G.; Garufi, F.; Gaur, G.; Gehrels, N.; Gemme, G.; Geng, P.; Genin, E.; Gennai, A.; George, J.; Gergely, L.; Germain, V.; Ghosh, Abhirup; Ghosh, Archisman; Ghosh, S.; Giaime, J. A.; Giardina, K. D.; Giazotto, A.; Gill, K.; Glaefke, A.; Goetz, E.; Goetz, R.; Gondan, L.; González, G.; Gonzalez Castro, J. M.; Gopakumar, A.; Gordon, N. A.; Gorodetsky, M. L.; Gossan, S. E.; Gosselin, M.; Gouaty, R.; Grado, A.; Graef, C.; Graff, P. B.; Granata, M.; Grant, A.; Gras, S.; Gray, C.; Greco, G.; Green, A. C.; Groot, P.; Grote, H.; Grunewald, S.; Guidi, G. M.; Guo, X.; Gupta, A.; Gupta, M. K.; Gushwa, K. E.; Gustafson, E. K.; Gustafson, R.; Hacker, J. J.; Hall, B. R.; Hall, E. D.; Hammond, G.; Haney, M.; Hanke, M. M.; Hanks, J.; Hanna, C.; Hannam, M. D.; Hanson, J.; Hardwick, T.; Harms, J.; Harry, G. M.; Harry, I. W.; Hart, M. J.; Hartman, M. T.; Haster, C.-J.; Haughian, K.; Healy, J.; Heidmann, A.; Heintze, M. C.; Heitmann, H.; Hello, P.; Hemming, G.; Hendry, M.; Heng, I. S.; Hennig, J.; Henry, J.; Heptonstall, A. W.; Heurs, M.; Hild, S.; Hoak, D.; Hofman, D.; Holt, K.; Holz, D. E.; Hopkins, P.; Hough, J.; Houston, E. A.; Howell, E. J.; Hu, Y. M.; Huang, S.; Huerta, E. A.; Huet, D.; Hughey, B.; Husa, S.; Huttner, S. H.; Huynh-Dinh, T.; Indik, N.; Ingram, D. R.; Inta, R.; Isa, H. N.; Isac, J.-M.; Isi, M.; Isogai, T.; Iyer, B. R.; Izumi, K.; Jacqmin, T.; Jang, H.; Jani, K.; Jaranowski, P.; Jawahar, S.; Jian, L.; Jiménez-Forteza, F.; Johnson, W. W.; Johnson-McDaniel, N. K.; Jones, D. I.; Jones, R.; Jonker, R. J. G.; Ju, L.; K, Haris; Kalaghatgi, C. V.; Kalogera, V.; Kandhasamy, S.; Kang, G.; Kanner, J. B.; Kapadia, S. J.; Karki, S.; Karvinen, K. S.; Kasprzack, M.; Katsavounidis, E.; Katzman, W.; Kaufer, S.; Kaur, T.; Kawabe, K.; Kéfélian, F.; Kehl, M. S.; Keitel, D.; Kelley, D. B.; Kells, W.; Kennedy, R.; Key, J. S.; Khalili, F. Y.; Khan, I.; Khan, S.; Khan, Z.; Khazanov, E. A.; Kijbunchoo, N.; Kim, Chi-Woong; Kim, Chunglee; Kim, J.; Kim, K.; Kim, N.; Kim, W.; Kim, Y.-M.; Kimbrell, S. J.; King, E. J.; King, P. J.; Kissel, J. S.; Klein, B.; Kleybolte, L.; Klimenko, S.; Koehlenbeck, S. M.; Koley, S.; Kondrashov, V.; Kontos, A.; Korobko, M.; Korth, W. Z.; Kowalska, I.; Kozak, D. B.; Kringel, V.; Królak, A.; Krueger, C.; Kuehn, G.; Kumar, P.; Kumar, R.; Kuo, L.; Kutynia, A.; Lackey, B. D.; Landry, M.; Lange, J.; Lantz, B.; Lasky, P. D.; Laxen, M.; Lazzarini, A.; Lazzaro, C.; Leaci, P.; Leavey, S.; Lebigot, E. O.; Lee, C. H.; Lee, H. K.; Lee, H. M.; Lee, K.; Lenon, A.; Leonardi, M.; Leong, J. R.; Leroy, N.; Letendre, N.; Levin, Y.; Lewis, J. B.; Li, T. G. F.; Libson, A.; Littenberg, T. B.; Lockerbie, N. A.; Lombardi, A. L.; London, L. T.; Lord, J. E.; Lorenzini, M.; Loriette, V.; Lormand, M.; Losurdo, G.; Lough, J. D.; Lousto, C. O.; Lovelace, G.; Lück, H.; Lundgren, A. P.; Lynch, R.; Ma, Y.; Machenschalk, B.; MacInnis, M.; Macleod, D. M.; Magaña-Sandoval, F.; Magaña Zertuche, L.; Magee, R. M.; Majorana, E.; Maksimovic, I.; Malvezzi, V.; Man, N.; Mandic, V.; Mangano, V.; Mansell, G. L.; Manske, M.; Mantovani, M.; Marchesoni, F.; Marion, F.; Márka, S.; Márka, Z.; Markosyan, A. S.; Maros, E.; Martelli, F.; Martellini, L.; Martin, I. W.; Martynov, D. V.; Marx, J. N.; Mason, K.; Masserot, A.; Massinger, T. J.; Masso-Reid, M.; Mastrogiovanni, S.; Matichard, F.; Matone, L.; Mavalvala, N.; Mazumder, N.; McCarthy, R.; McClelland, D. E.; McCormick, S.; McGuire, S. C.; McIntyre, G.; McIver, J.; McManus, D. J.; McRae, T.; McWilliams, S. T.; Meacher, D.; Meadors, G. D.; Meidam, J.; Melatos, A.; Mendell, G.; Mercer, R. A.; Merilh, E. L.; Merzougui, M.; Meshkov, S.; Messenger, C.; Messick, C.; Metzdorff, R.; Meyers, P. M.; Mezzani, F.; Miao, H.; Michel, C.; Middleton, H.; Mikhailov, E. E.; Milano, L.; Miller, A. L.; Miller, A.; Miller, B. B.; Miller, J.; Millhouse, M.; Minenkov, Y.; Ming, J.; Mirshekari, S.; Mishra, C.; Mitra, S.; Mitrofanov, V. P.; Mitselmakher, G.; Mittleman, R.; Moggi, A.; Mohan, M.; Mohapatra, S. R. P.; Montani, M.; Moore, B. C.; Moore, C. J.; Moraru, D.; Moreno, G.; Morriss, S. R.; Mossavi, K.; Mours, B.; Mow-Lowry, C. M.; Mueller, G.; Muir, A. W.; Mukherjee, Arunava; Mukherjee, D.; Mukherjee, S.; Mukund, N.; Mullavey, A.; Munch, J.; Murphy, D. J.; Murray, P. G.; Mytidis, A.; Nardecchia, I.; Naticchioni, L.; Nayak, R. K.; Nedkova, K.; Nelemans, G.; Nelson, T. J. N.; Neri, M.; Neunzert, A.; Newton, G.; Nguyen, T. T.; Nielsen, A. B.; Nissanke, S.; Nitz, A.; Nocera, F.; Nolting, D.; Normandin, M. E. N.; Nuttall, L. K.; Oberling, J.; Ochsner, E.; O'Dell, J.; Oelker, E.; Ogin, G. H.; Oh, J. J.; Oh, S. H.; Ohme, F.; Oliver, M.; Oppermann, P.; Oram, Richard J.; O'Reilly, B.; O'Shaughnessy, R.; Ottaway, D. J.; Overmier, H.; Owen, B. J.; Pai, A.; Pai, S. A.; Palamos, J. R.; Palashov, O.; Palomba, C.; Pal-Singh, A.; Pan, H.; Pankow, C.; Pannarale, F.; Pant, B. C.; Paoletti, F.; Paoli, A.; Papa, M. A.; Paris, H. R.; Parker, W.; Pascucci, D.; Pasqualetti, A.; Passaquieti, R.; Passuello, D.; Patricelli, B.; Patrick, Z.; Pearlstone, B. L.; Pedraza, M.; Pedurand, R.; Pekowsky, L.; Pele, A.; Penn, S.; Perreca, A.; Perri, L. M.; Pfeiffer, H. P.; Phelps, M.; Piccinni, O. J.; Pichot, M.; Piergiovanni, F.; Pierro, V.; Pillant, G.; Pinard, L.; Pinto, I. M.; Pitkin, M.; Poe, M.; Poggiani, R.; Popolizio, P.; Post, A.; Powell, J.; Prasad, J.; Predoi, V.; Prestegard, T.; Price, L. R.; Prijatelj, M.; Principe, M.; Privitera, S.; Prix, R.; Prodi, G. A.; Prokhorov, L.; Puncken, O.; Punturo, M.; Puppo, P.; Pürrer, M.; Qi, H.; Qin, J.; Qiu, S.; Quetschke, V.; Quintero, E. A.; Quitzow-James, R.; Raab, F. J.; Rabeling, D. S.; Radkins, H.; Raffai, P.; Raja, S.; Rajan, C.; Rakhmanov, M.; Rapagnani, P.; Raymond, V.; Razzano, M.; Re, V.; Read, J.; Reed, C. M.; Regimbau, T.; Rei, L.; Reid, S.; Reitze, D. H.; Rew, H.; Reyes, S. D.; Ricci, F.; Riles, K.; Rizzo, M.; Robertson, N. A.; Robie, R.; Robinet, F.; Rocchi, A.; Rolland, L.; Rollins, J. G.; Roma, V. J.; Romano, R.; Romanov, G.; Romie, J. H.; Rosińska, D.; Rowan, S.; Rüdiger, A.; Ruggi, P.; Ryan, K.; Sachdev, S.; Sadecki, T.; Sadeghian, L.; Sakellariadou, M.; Salconi, L.; Saleem, M.; Salemi, F.; Samajdar, A.; Sammut, L.; Sanchez, E. J.; Sandberg, V.; Sandeen, B.; Sanders, J. R.; Sassolas, B.; Sathyaprakash, B. S.; Saulson, P. R.; Sauter, O. E. S.; Savage, R. L.; Sawadsky, A.; Schale, P.; Schilling, R.; Schmidt, J.; Schmidt, P.; Schnabel, R.; Schofield, R. M. S.; Schönbeck, A.; Schreiber, E.; Schuette, D.; Schutz, B. F.; Scott, J.; Scott, S. M.; Sellers, D.; Sengupta, A. S.; Sentenac, D.; Sequino, V.; Sergeev, A.; Setyawati, Y.; Shaddock, D. A.; Shaffer, T.; Shahriar, M. S.; Shaltev, M.; Shapiro, B.; Shawhan, P.; Sheperd, A.; Shoemaker, D. H.; Shoemaker, D. M.; Siellez, K.; Siemens, X.; Sieniawska, M.; Sigg, D.; Silva, A. D.; Singer, A.; Singer, L. P.; Singh, A.; Singh, R.; Singhal, A.; Sintes, A. M.; Slagmolen, B. J. J.; Smith, J. R.; Smith, N. D.; Smith, R. J. E.; Son, E. J.; Sorazu, B.; Sorrentino, F.; Souradeep, T.; Srivastava, A. K.; Staley, A.; Steinke, M.; Steinlechner, J.; Steinlechner, S.; Steinmeyer, D.; Stephens, B. C.; Stevenson, S. P.; Stone, R.; Strain, K. A.; Straniero, N.; Stratta, G.; Strauss, N. A.; Strigin, S.; Sturani, R.; Stuver, A. L.; Summerscales, T. Z.; Sun, L.; Sunil, S.; Sutton, P. J.; Swinkels, B. L.; Szczepańczyk, M. J.; Tacca, M.; Talukder, D.; Tanner, D. B.; Tápai, M.; Tarabrin, S. P.; Taracchini, A.; Taylor, R.; Theeg, T.; Thirugnanasambandam, M. P.; Thomas, E. G.; Thomas, M.; Thomas, P.; Thorne, K. A.; Thorne, K. S.; Thrane, E.; Tiwari, S.; Tiwari, V.; Tokmakov, K. V.; Toland, K.; Tomlinson, C.; Tonelli, M.; Tornasi, Z.; Torres, C. V.; Torrie, C. I.; Töyrä, D.; Travasso, F.; Traylor, G.; Trifirò, D.; Tringali, M. C.; Trozzo, L.; Tse, M.; Turconi, M.; Tuyenbayev, D.; Ugolini, D.; Unnikrishnan, C. S.; Urban, A. L.; Usman, S. A.; Vahlbruch, H.; Vajente, G.; Valdes, G.; Vallisneri, M.; van Bakel, N.; van Beuzekom, M.; van den Brand, J. F. J.; Van Den Broeck, C.; Vander-Hyde, D. C.; van der Schaaf, L.; van der Sluys, M. V.; van Heijningen, J. V.; Vano-Vinuales, A.; van Veggel, A. A.; Vardaro, M.; Vass, S.; Vasúth, M.; Vaulin, R.; Vecchio, A.; Vedovato, G.; Veitch, J.; Veitch, P. J.; Venkateswara, K.; Verkindt, D.; Vetrano, F.; Viceré, A.; Vinciguerra, S.; Vine, D. J.; Vinet, J.-Y.; Vitale, S.; Vo, T.; Vocca, H.; Vorvick, C.; Voss, D. V.; Vousden, W. D.; Vyatchanin, S. P.; Wade, A. R.; Wade, L. E.; Wade, M.; Walker, M.; Wallace, L.; Walsh, S.; Wang, G.; Wang, H.; Wang, M.; Wang, X.; Wang, Y.; Ward, R. L.; Warner, J.; Was, M.; Weaver, B.; Wei, L.-W.; Weinert, M.; Weinstein, A. J.; Weiss, R.; Wen, L.; Weßels, P.; Westphal, T.; Wette, K.; Whelan, J. T.; Whiting, B. F.; Williams, R. D.; Williamson, A. R.; Willis, J. L.; Willke, B.; Wimmer, M. H.; Winkler, W.; Wipf, C. C.; Wittel, H.; Woan, G.; Woehler, J.; Worden, J.; Wright, J. L.; Wu, D. S.; Wu, G.; Yablon, J.; Yam, W.; Yamamoto, H.; Yancey, C. C.; Yu, H.; Yvert, M.; ZadroŻny, A.; Zangrando, L.; Zanolin, M.; Zendri, J.-P.; Zevin, M.; Zhang, L.; Zhang, M.; Zhang, Y.; Zhao, C.; Zhou, M.; Zhou, Z.; Zhu, X. J.; Zucker, M. E.; Zuraw, S. E.; Zweizig, J.; Boyle, M.; Brügmann, B.; Campanelli, M.; Chu, T.; Clark, M.; Haas, R.; Hemberger, D.; Hinder, I.; Kidder, L. E.; Kinsey, M.; Laguna, P.; Ossokine, S.; Pan, Y.; Röver, C.; Scheel, M.; Szilagyi, B.; Teukolsky, S.; Zlochower, Y.; LIGO Scientific Collaboration; Virgo Collaboration

2016-10-01

This paper presents updated estimates of source parameters for GW150914, a binary black-hole coalescence event detected by the Laser Interferometer Gravitational-wave Observatory (LIGO) in 2015 [Abbott et al. Phys. Rev. Lett. 116, 061102 (2016).]. Abbott et al. [Phys. Rev. Lett. 116, 241102 (2016).] presented parameter estimation of the source using a 13-dimensional, phenomenological precessing-spin model (precessing IMRPhenom) and an 11-dimensional nonprecessing effective-one-body (EOB) model calibrated to numerical-relativity simulations, which forces spin alignment (nonprecessing EOBNR). Here, we present new results that include a 15-dimensional precessing-spin waveform model (precessing EOBNR) developed within the EOB formalism. We find good agreement with the parameters estimated previously [Abbott et al. Phys. Rev. Lett. 116, 241102 (2016).], and we quote updated component masses of 35-3+5 M⊙ and 3 0-4+3 M⊙ (where errors correspond to 90% symmetric credible intervals). We also present slightly tighter constraints on the dimensionless spin magnitudes of the two black holes, with a primary spin estimate <0.65 and a secondary spin estimate <0.75 at 90% probability. Abbott et al. [Phys. Rev. Lett. 116, 241102 (2016).] estimated the systematic parameter-extraction errors due to waveform-model uncertainty by combining the posterior probability densities of precessing IMRPhenom and nonprecessing EOBNR. Here, we find that the two precessing-spin models are in closer agreement, suggesting that these systematic errors are smaller than previously quoted.

Domino model for geomagnetic field reversals.

PubMed

Mori, N; Schmitt, D; Wicht, J; Ferriz-Mas, A; Mouri, H; Nakamichi, A; Morikawa, M

2013-01-01

We solve the equations of motion of a one-dimensional planar Heisenberg (or Vaks-Larkin) model consisting of a system of interacting macrospins aligned along a ring. Each spin has unit length and is described by its angle with respect to the rotational axis. The orientation of the spins can vary in time due to spin-spin interaction and random forcing. We statistically describe the behavior of the sum of all spins for different parameters. The term "domino model" in the title refers to the interaction among the spins. We compare the model results with geomagnetic field reversals and dynamo simulations and find strikingly similar behavior. The aggregate of all spins keeps the same direction for a long time and, once in a while, begins flipping to change the orientation by almost 180 degrees (mimicking a geomagnetic reversal) or to move back to the original direction (mimicking an excursion). Most of the time the spins are aligned or antialigned and deviate only slightly with respect to the rotational axis (mimicking the secular variation of the geomagnetic pole with respect to the geographic pole). Reversals are fast compared to the times in between and they occur at random times, both in the model and in the case of the Earth's magnetic field.

Spin vectors in the Koronis family: III. (832) Karin

NASA Astrophysics Data System (ADS)

Slivan, Stephen M.; Molnar, Lawrence A.

2012-08-01

Studies of asteroid families constrain models of asteroid collisions and evolution processes, and the Karin cluster within the Koronis family is among the youngest families known (Nesvorný, D., Bottke, Jr., W.F., Dones, L., Levison, H.F. [2002]. Nature 417, 720-722). (832) Karin itself is by far the largest member of the Karin cluster, thus knowledge of Karin's spin vector is important to constrain family formation and evolution models that include spin, and to test whether its spin properties are consistent with the Karin cluster being a very young family. We observed rotation lightcurves of Karin during its four consecutive apparitions in 2006-2009, and combined the new observations with previously published lightcurves to determine its spin vector orientation and preliminary model shape. Karin is a prograde rotator with a period of (18.352 ± 0.003) h, spin obliquity near (42 ± 5)°, and pole ecliptic longitude near either (52 ± 5)° or (230 ± 5)°. The spin vector and shape results for Karin will constrain models of family formation that include spin properties; in the meantime we briefly discuss Karin's own spin in the context of those of other members of the Karin cluster and the parent body's siblings in the Koronis family.

Spin and model determination of Z‧ - boson in lepton pair production at CERN LHC

NASA Astrophysics Data System (ADS)

Tsytrinov, A. V.; Pankov, A. A.; Serenkova, I. A.; Bednyakov, V. A.

2017-12-01

Many new physics models predict production of heavy resonances in Drell-Yan channel and can be observed at the CERN LHC. If a new resonance is discovered as a peak in the dilepton invariant mass distribution at the LHC, the identification of its spin and couplings can be done by measuring production rates and angular distributions of the decay products. Here we discuss the spin-1 identification of Z‧-boson for a set of representative models (SSM, E6, LR, and ALR) against the spin-2 RS graviton resonance and a spin-0 sneutrino resonance with the same mass and producing the same number of events under the resonance peak. We use the center-edge asymmetry for spin identification, as well as the total dilepton production cross section for the distinguishing the considered Z‧-boson models from one another.

Summary of flight tests to determine the spin and controllability characteristics of a remotely piloted, large-scale (3/8) fighter airplane model

NASA Technical Reports Server (NTRS)

Holleman, E. C.

1976-01-01

An unpowered, large, dynamically scaled airplane model was test flown by remote pilot to investigate the stability and controllability of the configuration at high angles of attack. The configuration proved to be departure/spin resistant; however, spins were obtained by using techniques developed on a flight support simulator. Spin modes at high and medium high angles of attack were identified, and recovery techniques were investigated. A flight support simulation of the airplane model mechanized with low speed wind tunnel data over an angle of attack range of + or - 90 deg. and an angle of sideslip range of + or - 40 deg. provided insight into the effects of altitude, stability, aerodynamic damping, and the operation of the augmented flight control system on spins. Aerodynamic derivatives determined from flight maneuvers were used to correlate model controllability with two proposed departure/spin design criteria.

Negativity as the entanglement measure to probe the Kondo regime in the spin-chain Kondo model

NASA Astrophysics Data System (ADS)

Bayat, Abolfazl; Sodano, Pasquale; Bose, Sougato

2010-02-01

We study the entanglement of an impurity at one end of a spin chain with a block of spins using negativity as a true measure of entanglement to characterize the unique features of the gapless Kondo regime in the spin-chain Kondo model. For this spin chain in the Kondo regime we determine—with a true entanglement measure—the spatial extent of the Kondo screening cloud, we propose an ansatz for its ground state and demonstrate that the impurity spin is indeed maximally entangled with the cloud. To better evidence the peculiarities of the Kondo regime, we carry a parallel analysis of the entanglement properties of the Kondo spin-chain model in the gapped dimerized regime. Our study shows how a genuine entanglement measure stemming from quantum information theory can fully characterize also nonperturbative regimes accessible to certain condensed matter systems.

Feynman propagator for spin foam quantum gravity.

PubMed

Oriti, Daniele

2005-03-25

We link the notion causality with the orientation of the spin foam 2-complex. We show that all current spin foam models are orientation independent. Using the technology of evolution kernels for quantum fields on Lie groups, we construct a generalized version of spin foam models, introducing an extra proper time variable. We prove that different ranges of integration for this variable lead to different classes of spin foam models: the usual ones, interpreted as the quantum gravity analogue of the Hadamard function of quantum field theory (QFT) or as inner products between quantum gravity states; and a new class of causal models, the quantum gravity analogue of the Feynman propagator in QFT, nontrivial function of the orientation data, and implying a notion of "timeless ordering".

Spin-selective electronic reconstruction in quantum ferromagnets: A view from the spin-asymmetric Hubbard model

NASA Astrophysics Data System (ADS)

Faúndez, J.; Jorge, T. N.; Craco, L.

2018-03-01

Using the tight-binding treatment for the spin-asymmetric Hubbard model we explore the effect of electronic interactions in the ferromagnetic, partially filled Lieb lattice. As a key result we demonstrate the formation of correlation satellites in the minority spin channel. In addition, we consider the role played by transverse-field spin fluctuations in metallic ferromagnets. We quantify the degree of electronic demagnetization, showing that the half-metallic state is rather robust to local spin flips. Not being restricted to the case of a partially filled Lieb lattice, our findings are expected to advance the general understanding of spin-selective electronic reconstruction in strongly correlated quantum ferromagnets.

Magnetoelectric Effect in a Spin-State Transition System

NASA Astrophysics Data System (ADS)

Naka, Makoto; Mizoguchi, Eriko; Nasu, Joji; Ishihara, Sumio

2018-06-01

Magnetic, dielectric, and magnetoelectric properties in a spin-state transition system are examined, motivated by the recent discovery of multiferroic behavior in a cobalt oxide. We construct an effective model Hamiltonian on the basis of the two-orbital Hubbard model, in which the spin-state degrees of freedom in magnetic ions couple with ferroelectric-type lattice distortions. A phase transition occurs from the high-temperature low-spin phase to the low-temperature high-spin ferroelectric phase with an accompanying increase in spin entropy. The calculated results are consistent with the experimental pressure-temperature phase diagram. We predict the magnetic-field induced electric polarization in the low-spin paraelectric phase near the ferroelectric phase boundary.

Spin-orbit-torque-induced skyrmion dynamics for different types of spin-orbit coupling

NASA Astrophysics Data System (ADS)

Lee, Seung-Jae; Kim, Kyoung-Whan; Lee, Hyun-Woo; Lee, Kyung-Jin

2018-06-01

We investigate current-induced skyrmion dynamics in the presence of Dzyaloshinskii-Moriya interaction and spin-orbit spin-transfer torque corresponding to various types of spin-orbit coupling. We determine the symmetries of Dzyaloshinskii-Moriya interaction and spin-orbit spin-transfer torque based on linear spin-orbit coupling model. We find that like interfacial Dzyaloshinskii-Moriya interaction (Rashba spin-orbit coupling) and bulk Dzyaloshinskii-Moriya interaction (Weyl spin-orbit coupling), Dresselhaus spin-orbit coupling also has a possibility for stabilizing skyrmion and current-induced skyrmion dynamics.

On the exact solvability of the anisotropic central spin model: An operator approach

NASA Astrophysics Data System (ADS)

Wu, Ning

2018-07-01

Using an operator approach based on a commutator scheme that has been previously applied to Richardson's reduced BCS model and the inhomogeneous Dicke model, we obtain general exact solvability requirements for an anisotropic central spin model with XXZ-type hyperfine coupling between the central spin and the spin bath, without any prior knowledge of integrability of the model. We outline basic steps of the usage of the operators approach, and pedagogically summarize them into two Lemmas and two Constraints. Through a step-by-step construction of the eigen-problem, we show that the condition gj‧2 - gj2 = c naturally arises for the model to be exactly solvable, where c is a constant independent of the bath-spin index j, and {gj } and { gj‧ } are the longitudinal and transverse hyperfine interactions, respectively. The obtained conditions and the resulting Bethe ansatz equations are consistent with that in previous literature.

U.S. Navy Fault-Tolerant Microcomputer.

DTIC Science & Technology

1982-07-01

105 8929 SEPULVEDA BLVD. LOS ANGELES, CALIFORNIA 90045 To: DEFENSE TECHNICAL INFORMATION CENTER Fal-ae Technoog Corporation MILITARY STANDARD FAULT...maintainability. Com- puter errors at any significant level can be disastrous in terms of human injury, aborted missions, loss of critical information and...employed to resolve the question "who checks the checker?" The IOC votes on information received from the bus and outputs the maiority decision. Thus no

Making Microscopic Cubes Of Boron

NASA Technical Reports Server (NTRS)

Faulkner, Joseph M.

1993-01-01

Production of finely divided cubes of boron involves vacuum-deposition technology and requires making of template. Template supports pattern of checkered squares 25 micrometers on side, which are etched 25 micrometers into template material. Template coasted uniformly with paralyene or some similar vacuum coating with low coefficient of adhesion. Intended application to solid rocket fuels, explosives, and pyrotechnics; process used for other applications, from manufacture of pharmaceuticals to processing of nuclear materials.

A Study on Run Time Assurance for Complex Cyber Physical Systems

DTIC Science & Technology

2013-04-18

safety verification approach was applied to synchronization of distributed local clocks of the nodes on a CAN bus by Jiang et al. [36]. The class of...mode of interaction between the instrumented system and the checker, we distin- guish between synchronous and asynchronous monitoring. In synchronous ...occurred. Synchronous monitoring may deliver a higher degree of assurance than the asynchronous one, because it can block a dangerous action. However

Effects of Online Translation on Morphosyntactic and Lexical-Pragmatic Accuracy in Essay Writing in Spanish as a Foreign Language

ERIC Educational Resources Information Center

Fredholm, Kent

2014-01-01

The use of online translation (OT) is increasing as more pupils receive laptops from their schools. This study investigates OT use in two groups of Swedish pupils (ages 17-18) studying Spanish as an L3: one group (A) having free Internet access and the spelling and grammar checker of Microsoft Word, the other group (B) using printed dictionaries…

AIDE - Advanced Intrusion Detection Environment

DOE Office of Scientific and Technical Information (OSTI.GOV)

Smith, Cathy L.

2013-04-28

Would you like to know when someone has dropped an undesirable executable binary on our system? What about something less malicious such as a software installation by a user? What about the user who decides to install a newer version of mod_perl or PHP on your web server without letting you know beforehand? Or even something as simple as when an undocumented config file change is made by another member of the admin group? Do you even want to know about all the changes that happen on a daily basis on your server? The purpose of an intrusion detection systemmore » (IDS) is to detect unauthorized, possibly malicious activity. The purpose of a host-based IDS, or file integrity checker, is check for unauthorized changes to key system files, binaries, libraries, and directories on the system. AIDE is an Open Source file and directory integrity checker. AIDE will let you know when a file or directory has been added, deleted, modified. It is included with the Red Hat Enterprise 6. It is available for other Linux distros. This is a case study describing the process of configuring AIDE on an out of the box RHEL6 installation. Its goal is to illustrate the thinking and the process by which a useful AIDE configuration is built.« less

Correlation between near infrared spectroscopy and electrical techniques in measuring skin moisture content

NASA Astrophysics Data System (ADS)

Mohamad, M.; Sabbri, A. R. M.; Mat Jafri, M. Z.; Omar, A. F.

2014-11-01

Near infrared (NIR) spectroscopy technique serves as an important tool for the measurement of moisture content of skin owing to the advantages it has over the other techniques. The purpose of the study is to develop a correlation between NIR spectrometer with electrical conventional techniques for skin moisture measurement. A non-invasive measurement of moisture content of skin was performed on different part of human face and hand under control environment (temperature 21 ± 1 °C, relative humidity 45 ± 5 %). Ten healthy volunteers age between 21-25 (male and female) participated in this study. The moisture content of skin was measured using DermaLab® USB Moisture Module, Scalar Moisture Checker and NIR spectroscopy (NIRQuest). Higher correlation was observed between NIRQuest and Dermalab moisture probe with a coefficient of determination (R2) above 70 % for all the subjects. However, the value of R2 between NIRQuest and Moisture Checker was observed to be lower with the R2 values ranges from 51.6 to 94.4 %. The correlation of NIR spectroscopy technique successfully developed for measuring moisture content of the skin. The analysis of this correlation can help to establish novel instruments based on an optical system in clinical used especially in the dermatology field.

Electrical control of spin dynamics in finite one-dimensional systems

NASA Astrophysics Data System (ADS)

Pertsova, A.; Stamenova, M.; Sanvito, S.

2011-10-01

We investigate the possibility of the electrical control of spin transfer in monoatomic chains incorporating spin impurities. Our theoretical framework is the mixed quantum-classical (Ehrenfest) description of the spin dynamics, in the spirit of the s-d model, where the itinerant electrons are described by a tight-binding model while localized spins are treated classically. Our main focus is on the dynamical exchange interaction between two well-separated spins. This can be quantified by the transfer of excitations in the form of transverse spin oscillations. We systematically study the effect of an electrostatic gate bias Vg on the interconnecting channel and we map out the long-range dynamical spin transfer as a function of Vg. We identify regions of Vg giving rise to significant amplification of the spin transmission at low frequencies and relate this to the electronic structure of the channel.

Coarse graining flow of spin foam intertwiners

NASA Astrophysics Data System (ADS)

Dittrich, Bianca; Schnetter, Erik; Seth, Cameron J.; Steinhaus, Sebastian

2016-12-01

Simplicity constraints play a crucial role in the construction of spin foam models, yet their effective behavior on larger scales is scarcely explored. In this article we introduce intertwiner and spin net models for the quantum group SU (2 )k×SU (2 )k, which implement the simplicity constraints analogous to four-dimensional Euclidean spin foam models, namely the Barrett-Crane (BC) and the Engle-Pereira-Rovelli-Livine/Freidel-Krasnov (EPRL/FK) model. These models are numerically coarse grained via tensor network renormalization, allowing us to trace the flow of simplicity constraints to larger scales. In order to perform these simulations we have substantially adapted tensor network algorithms, which we discuss in detail as they can be of use in other contexts. The BC and the EPRL/FK model behave very differently under coarse graining: While the unique BC intertwiner model is a fixed point and therefore constitutes a two-dimensional topological phase, BC spin net models flow away from the initial simplicity constraints and converge to several different topological phases. Most of these phases correspond to decoupling spin foam vertices; however we find also a new phase in which this is not the case, and in which a nontrivial version of the simplicity constraints holds. The coarse graining flow of the BC spin net models indicates furthermore that the transitions between these phases are not of second order. The EPRL/FK model by contrast reveals a far more intricate and complex dynamics. We observe an immediate flow away from the original simplicity constraints; however, with the truncation employed here, the models generically do not converge to a fixed point. The results show that the imposition of simplicity constraints can indeed lead to interesting and also very complex dynamics. Thus we need to further develop coarse graining tools to efficiently study the large scale behavior of spin foam models, in particular for the EPRL/FK model.

Parallelized traveling cluster approximation to study numerically spin-fermion models on large lattices

NASA Astrophysics Data System (ADS)

Mukherjee, Anamitra; Patel, Niravkumar D.; Bishop, Chris; Dagotto, Elbio

2015-06-01

Lattice spin-fermion models are important to study correlated systems where quantum dynamics allows for a separation between slow and fast degrees of freedom. The fast degrees of freedom are treated quantum mechanically while the slow variables, generically referred to as the "spins," are treated classically. At present, exact diagonalization coupled with classical Monte Carlo (ED + MC) is extensively used to solve numerically a general class of lattice spin-fermion problems. In this common setup, the classical variables (spins) are treated via the standard MC method while the fermion problem is solved by exact diagonalization. The "traveling cluster approximation" (TCA) is a real space variant of the ED + MC method that allows to solve spin-fermion problems on lattice sizes with up to 103 sites. In this publication, we present a novel reorganization of the TCA algorithm in a manner that can be efficiently parallelized. This allows us to solve generic spin-fermion models easily on 104 lattice sites and with some effort on 105 lattice sites, representing the record lattice sizes studied for this family of models.

Universal scheme for finite-probability perfect transfer of arbitrary multispin states through spin chains

DOE Office of Scientific and Technical Information (OSTI.GOV)

Man, Zhong-Xiao, E-mail: zxman@mail.qfnu.edu.cn; An, Nguyen Ba, E-mail: nban@iop.vast.ac.vn; Xia, Yun-Jie, E-mail: yjxia@mail.qfnu.edu.cn

In combination with the theories of open system and quantum recovering measurement, we propose a quantum state transfer scheme using spin chains by performing two sequential operations: a projective measurement on the spins of ‘environment’ followed by suitably designed quantum recovering measurements on the spins of interest. The scheme allows perfect transfer of arbitrary multispin states through multiple parallel spin chains with finite probability. Our scheme is universal in the sense that it is state-independent and applicable to any model possessing spin–spin interactions. We also present possible methods to implement the required measurements taking into account the current experimental technologies.more » As applications, we consider two typical models for which the probabilities of perfect state transfer are found to be reasonably high at optimally chosen moments during the time evolution. - Highlights: • Scheme that can achieve perfect quantum state transfer is devised. • The scheme is state-independent and applicable to any spin-interaction models. • The scheme allows perfect transfer of arbitrary multispin states. • Applications to two typical models are considered in detail.« less

An Investigation of the Free-Spinning and Recovery Characteristics of a 1/24-Scale Model of the Grumman F11F-1 Airplane with Alternate Nose Configurations with and without Wing Fuel Tanks, TED No. NACA AD 395

NASA Technical Reports Server (NTRS)

Bowman, James S., Jr.

1958-01-01

A supplementary investigation has been conducted in the langley 20-foot free-spinning tunnel on a l/24-scale model of the Grumman F11F-1 airplane to determine the spin and recovery characteristics with alternate nose configurations, the production version and the elongated APS-67 version, with and without empty and full wing tanks. When spins were obtained with either alternate nose configuration, they were oscillatory and recovery characteristics were considered unsatisfactory on the basis of the fact that very slow recoveries were indicated to be possible. The simultaneous extension of canards near the nose of the model with rudder reversal was effective in rapidly terminating the spin. The addition of empty wing tanks had little effect on the developed spin and recovery characteristics. The model did not spin erect with full wing tanks. For optimum recovery from inverted spins, the rudder should be reversed to 22O against the spin and simultaneously the flaperons should be moved with the developed spin; the stick should be held at or moved to full forward longitudinally. The minimum size parachute required to insure satisfactory recoveries in an emergency was found to be 12 feet in diameter (laid out flat) with a drag coefficient of 0.64 (based on the laid-out-flat diameter) and a towline length of 32 feet.

Improved Analysis of GW150914 Using a Fully Spin-Precessing Waveform Model

NASA Technical Reports Server (NTRS)

Abbott, B. P.; Abbott, R.; Abbott, T. D.; Abernathy, M. R.; Acernese, F.; Ackley, K.; Adams, C.; Adams, T.; Addesso, P.; Camp, J. B.;

Modeling and formal analysis of urban road traffic

NASA Astrophysics Data System (ADS)

Avram, Camelia; Machado, José; Aştilean, Adina

2013-10-01

Modern life in cities leads to complex urban traffic road and, sometimes, to go from one point to another, in a city, is a hard and very complex task. The use of assisted systems for helping drivers on their task of reaching the desired destination is being common, mainly systems like GPS location systems or other similar systems. The main gap of those systems is that they are not able to assist drivers when some unexpected changes occur, like accidents, or another unexpected situations. In this context, it would be desirable to have a dynamic system to inform the drivers, about everything that is happening "online". This work is inserted in this context and the work presented here is one part of a bigger project that has, as main goal, to be a dynamic system for assisting drivers under hard conditions of urban road traffic. In this paper is modeled, and formally analyzed, the intersection of four street segments, in order to take some considerations about this subject. This paper presents the model of the considered system, using timed automata formalism. The validation and verification of the road traffic model it is realized using UPPAAL model-checker.

On Secure Implementation of an IHE XUA-Based Protocol for Authenticating Healthcare Professionals

NASA Astrophysics Data System (ADS)

Masi, Massimiliano; Pugliese, Rosario; Tiezzi, Francesco

The importance of the Electronic Health Record (EHR) has been addressed in recent years by governments and institutions.Many large scale projects have been funded with the aim to allow healthcare professionals to consult patients data. Properties such as confidentiality, authentication and authorization are the key for the success for these projects. The Integrating the Healthcare Enterprise (IHE) initiative promotes the coordinated use of established standards for authenticated and secure EHR exchanges among clinics and hospitals. In particular, the IHE integration profile named XUA permits to attest user identities by relying on SAML assertions, i.e. XML documents containing authentication statements. In this paper, we provide a formal model for the secure issuance of such an assertion. We first specify the scenario using the process calculus COWS and then analyse it using the model checker CMC. Our analysis reveals a potential flaw in the XUA profile when using a SAML assertion in an unprotected network. We then suggest a solution for this flaw, and model check and implement this solution to show that it is secure and feasible.

Local nature of impurity induced spin-orbit torques

NASA Astrophysics Data System (ADS)

Nikolaev, Sergey; Kalitsov, Alan; Chshiev, Mairbec; Mryasov, Oleg

Spin-orbit torques are of a great interest due to their potential applications for spin electronics. Generally, it originates from strong spin orbit coupling of heavy 4d/5d elements and its mechanism is usually attributed either to the Spin Hall effect or Rashba spin-orbit coupling. We have developed a quantum-mechanical approach based on the non-equilibrium Green's function formalism and tight binding Hamiltonian model to study spin-orbit torques and extended our theory for the case of extrinsic spin-orbit coupling induced by impurities. For the sake of simplicity, we consider a magnetic material on a two dimensional lattice with a single non-magnetic impurity. However, our model can be easily extended for three dimensional layered heterostructures. Based on our calculations, we present the detailed analysis of the origin of local spin-orbit torques and persistent charge currents around the impurity, that give rise to spin-orbit torques even in equilibrium and explain the existence of anisotropy.

Flight investigation of the effect of tail configuration on stall, spin, and recovery characteristics of a low-wing general aviation research airplane

NASA Technical Reports Server (NTRS)

Stough, H. Paul, III; Patton, James M., Jr.; Sliwa, Steven M.

1987-01-01

Flight tests were performed to investigate the stall, spin, and recovery characteristics of a low-wing, single-engine, light airplane with four interchangeable tail configurations. The four tail configurations were evaluated for effects of varying mass distribution, center-of-gravity position, and control inputs. The airplane tended to roll-off at the stall. Variations in tail configuration produced spins ranging from 40 deg to 60 deg angle of attack and turn rates of about 145 to 208 deg/sec. Some unrecoverable flat spins were encountered which required use of the airplane spin chute for recovery. For recoverable spins, antispin rudder followed by forward wheel with ailerons centered provided the quickest spin recovery. The moderate spin modes agreed very well with those predicted from spin-tunnel model tests, however, the flat spin was at a lower angle of attack and a slower rotation rate than indicated by the model tests.

Accuracy of binary black hole waveform models for aligned-spin binaries

NASA Astrophysics Data System (ADS)

Kumar, Prayush; Chu, Tony; Fong, Heather; Pfeiffer, Harald P.; Boyle, Michael; Hemberger, Daniel A.; Kidder, Lawrence E.; Scheel, Mark A.; Szilagyi, Bela

2016-05-01

Coalescing binary black holes are among the primary science targets for second generation ground-based gravitational wave detectors. Reliable gravitational waveform models are central to detection of such systems and subsequent parameter estimation. This paper performs a comprehensive analysis of the accuracy of recent waveform models for binary black holes with aligned spins, utilizing a new set of 84 high-accuracy numerical relativity simulations. Our analysis covers comparable mass binaries (mass-ratio 1 ≤q ≤3 ), and samples independently both black hole spins up to a dimensionless spin magnitude of 0.9 for equal-mass binaries and 0.85 for unequal mass binaries. Furthermore, we focus on the high-mass regime (total mass ≳50 M⊙ ). The two most recent waveform models considered (PhenomD and SEOBNRv2) both perform very well for signal detection, losing less than 0.5% of the recoverable signal-to-noise ratio ρ , except that SEOBNRv2's efficiency drops slightly for both black hole spins aligned at large magnitude. For parameter estimation, modeling inaccuracies of the SEOBNRv2 model are found to be smaller than systematic uncertainties for moderately strong GW events up to roughly ρ ≲15 . PhenomD's modeling errors are found to be smaller than SEOBNRv2's, and are generally irrelevant for ρ ≲20 . Both models' accuracy deteriorates with increased mass ratio, and when at least one black hole spin is large and aligned. The SEOBNRv2 model shows a pronounced disagreement with the numerical relativity simulation in the merger phase, for unequal masses and simultaneously both black hole spins very large and aligned. Two older waveform models (PhenomC and SEOBNRv1) are found to be distinctly less accurate than the more recent PhenomD and SEOBNRv2 models. Finally, we quantify the bias expected from all four waveform models during parameter estimation for several recovered binary parameters: chirp mass, mass ratio, and effective spin.

Thermally Generated Spin Signals in a Nondegenerate Silicon Spin Valve

NASA Astrophysics Data System (ADS)

Yamashita, Naoto; Ando, Yuichiro; Koike, Hayato; Miwa, Shinji; Suzuki, Yoshishige; Shiraishi, Masashi

2018-05-01

Thermally generated spin signals are observed in a nondegenerate Si spin valve. The spin-dependent Seebeck effect is used for thermal spin-signal generation. A thermal gradient of about 200 mK at the interface of Fe and Si enables the generation of a spin voltage of 8 μ V at room temperature. A simple expansion of the conventional spin-drift-diffusion model that takes into account the spin-dependent Seebeck effect shows that semiconductor materials are more promising for thermal spin-signal generation comparing than metallic materials, and thus enable efficient heat recycling in semiconductor spin devices.

Emergent Chiral Spin State in the Mott Phase of a Bosonic Kane-Mele-Hubbard Model

NASA Astrophysics Data System (ADS)

Plekhanov, Kirill; Vasić, Ivana; Petrescu, Alexandru; Nirwan, Rajbir; Roux, Guillaume; Hofstetter, Walter; Le Hur, Karyn

2018-04-01

Recently, the frustrated X Y model for spins 1 /2 on the honeycomb lattice has attracted a lot of attention in relation with the possibility to realize a chiral spin liquid state. This model is relevant to the physics of some quantum magnets. Using the flexibility of ultracold atom setups, we propose an alternative way to realize this model through the Mott regime of the bosonic Kane-Mele-Hubbard model. The phase diagram of this model is derived using bosonic dynamical mean-field theory. Focusing on the Mott phase, we investigate its magnetic properties as a function of frustration. We do find an emergent chiral spin state in the intermediate frustration regime. Using exact diagonalization we study more closely the physics of the effective frustrated X Y model and the properties of the chiral spin state. This gapped phase displays a chiral order, breaking time-reversal and parity symmetry, but is not topologically ordered (the Chern number is zero).

Long-time predictability in disordered spin systems following a deep quench

NASA Astrophysics Data System (ADS)

Ye, J.; Gheissari, R.; Machta, J.; Newman, C. M.; Stein, D. L.

2017-04-01

We study the problem of predictability, or "nature vs nurture," in several disordered Ising spin systems evolving at zero temperature from a random initial state: How much does the final state depend on the information contained in the initial state, and how much depends on the detailed history of the system? Our numerical studies of the "dynamical order parameter" in Edwards-Anderson Ising spin glasses and random ferromagnets indicate that the influence of the initial state decays as dimension increases. Similarly, this same order parameter for the Sherrington-Kirkpatrick infinite-range spin glass indicates that this information decays as the number of spins increases. Based on these results, we conjecture that the influence of the initial state on the final state decays to zero in finite-dimensional random-bond spin systems as dimension goes to infinity, regardless of the presence of frustration. We also study the rate at which spins "freeze out" to a final state as a function of dimensionality and number of spins; here the results indicate that the number of "active" spins at long times increases with dimension (for short-range systems) or number of spins (for infinite-range systems). We provide theoretical arguments to support these conjectures, and also study analytically several mean-field models: the random energy model, the uniform Curie-Weiss ferromagnet, and the disordered Curie-Weiss ferromagnet. We find that for these models, the information contained in the initial state does not decay in the thermodynamic limit—in fact, it fully determines the final state. Unlike in short-range models, the presence of frustration in mean-field models dramatically alters the dynamical behavior with respect to the issue of predictability.

Long-time predictability in disordered spin systems following a deep quench.

PubMed

Ye, J; Gheissari, R; Machta, J; Newman, C M; Stein, D L

2017-04-01

We study the problem of predictability, or "nature vs nurture," in several disordered Ising spin systems evolving at zero temperature from a random initial state: How much does the final state depend on the information contained in the initial state, and how much depends on the detailed history of the system? Our numerical studies of the "dynamical order parameter" in Edwards-Anderson Ising spin glasses and random ferromagnets indicate that the influence of the initial state decays as dimension increases. Similarly, this same order parameter for the Sherrington-Kirkpatrick infinite-range spin glass indicates that this information decays as the number of spins increases. Based on these results, we conjecture that the influence of the initial state on the final state decays to zero in finite-dimensional random-bond spin systems as dimension goes to infinity, regardless of the presence of frustration. We also study the rate at which spins "freeze out" to a final state as a function of dimensionality and number of spins; here the results indicate that the number of "active" spins at long times increases with dimension (for short-range systems) or number of spins (for infinite-range systems). We provide theoretical arguments to support these conjectures, and also study analytically several mean-field models: the random energy model, the uniform Curie-Weiss ferromagnet, and the disordered Curie-Weiss ferromagnet. We find that for these models, the information contained in the initial state does not decay in the thermodynamic limit-in fact, it fully determines the final state. Unlike in short-range models, the presence of frustration in mean-field models dramatically alters the dynamical behavior with respect to the issue of predictability.

Quantum gap and spin-wave excitations in the Kitaev model on a triangular lattice

NASA Astrophysics Data System (ADS)

Avella, Adolfo; Di Ciolo, Andrea; Jackeli, George

2018-05-01

We study the effects of quantum fluctuations on the dynamical generation of a gap and on the evolution of the spin-wave spectra of a frustrated magnet on a triangular lattice with bond-dependent Ising couplings, analog of the Kitaev honeycomb model. The quantum fluctuations lift the subextensive degeneracy of the classical ground-state manifold by a quantum order-by-disorder mechanism. Nearest-neighbor chains remain decoupled and the surviving discrete degeneracy of the ground state is protected by a hidden model symmetry. We show how the four-spin interaction, emergent from the fluctuations, generates a spin gap shifting the nodal lines of the linear spin-wave spectrum to finite energies.

Spin-electron acoustic soliton and exchange interaction in separate spin evolution quantum plasmas

DOE Office of Scientific and Technical Information (OSTI.GOV)

Andreev, Pavel A., E-mail: andreevpa@physics.msu.ru

Separate spin evolution quantum hydrodynamics is generalized to include the Coulomb exchange interaction, which is considered as interaction between the spin-down electrons being in quantum states occupied by one electron. The generalized model is applied to study the non-linear spin-electron acoustic waves. Existence of the spin-electron acoustic soliton is demonstrated. Contributions of concentration, spin polarization, and exchange interaction to the properties of the spin electron acoustic soliton are studied.

A model of spin crossover in manganese(III) compounds: effects of intra- and intercenter interactions.

PubMed

Klokishner, Sophia I; Roman, Marianna A; Reu, Oleg S

2011-11-21

A microscopic approach to the problem of cooperative spin crossover in the [MnL2]NO3 crystal, which contains Mn(III) ions as structural units, is elaborated on, and the main mechanisms governing this effect are revealed. The proposed model also takes into account the splitting of the low-spin 3T1 (t(2)(4)) and high-spin 5E (t(2)(3)e) terms by the low-symmetry crystal field. The low-spin → high-spin transition has been considered as a cooperative phenomenon driven by interaction of the electronic shells of the Mn(III) ions with the all-around full-symmetric deformation that is extended over the crystal lattice via the acoustic phonon field. The model well explains the observed thermal dependencies of the magnetic susceptibility and the effective magnetic moment.

Constraining the noise-free distribution of halo spin parameters

NASA Astrophysics Data System (ADS)

Benson, Andrew J.

2017-11-01

Any measurement made using an N-body simulation is subject to noise due to the finite number of particles used to sample the dark matter distribution function, and the lack of structure below the simulation resolution. This noise can be particularly significant when attempting to measure intrinsically small quantities, such as halo spin. In this work, we develop a model to describe the effects of particle noise on halo spin parameters. This model is calibrated using N-body simulations in which the particle noise can be treated as a Poisson process on the underlying dark matter distribution function, and we demonstrate that this calibrated model reproduces measurements of halo spin parameter error distributions previously measured in N-body convergence studies. Utilizing this model, along with previous measurements of the distribution of halo spin parameters in N-body simulations, we place constraints on the noise-free distribution of halo spins. We find that the noise-free median spin is 3 per cent lower than that measured directly from the N-body simulation, corresponding to a shift of approximately 40 times the statistical uncertainty in this measurement arising purely from halo counting statistics. We also show that measurement of the spin of an individual halo to 10 per cent precision requires at least 4 × 104 particles in the halo - for haloes containing 200 particles, the fractional error on spins measured for individual haloes is of order unity. N-body simulations should be viewed as the results of a statistical experiment applied to a model of dark matter structure formation. When viewed in this way, it is clear that determination of any quantity from such a simulation should be made through forward modelling of the effects of particle noise.

Renormalization Group Studies and Monte Carlo Simulation for Quantum Spin Systems.

NASA Astrophysics Data System (ADS)

Pan, Ching-Yan

We have discussed the extended application of various real space renormalization group methods to the quantum spin systems. At finite temperature, we extended both the reliability and range of application of the decimation renormalization group method (DRG) for calculating the thermal and magnetic properties of low-dimensional quantum spin chains, in which we have proposed general models of the three-state Potts model and the general Heisenberg model. Some interesting finite-temperature behavior of the models has been obtained. We also proposed a general formula for the critical properties of the n-dimensional q-state Potts model by using a modified migdal-Kadanoff approach which is in very good agreement with all available results for general q and d. For high-spin systems, we have investigated the famous Haldane's prediction by using a modified block renormalization group approach in spin -1over2, spin-1 and spin-3 over2 cases. Our result supports Haldane's prediction and a novel property of the spin-1 Heisenberg antiferromagnet has been predicted. A modified quantum monte Carlo simulation approach has been developed in this study which we use to treat quantum interacting problems (we only work on quantum spin systems in this study) without the "negative sign problem". We also obtain with the Monte Carlo approach the numerical derivative directly. Furthermore, using this approach we have obtained the energy spectrum and the thermodynamic properties of the antiferromagnetic q-state Potts model, and have studied the q-color problem with the result which supports Mattis' recent conjecture of entropy for the n -dimensional q-state Potts antiferromagnet. We also find a general solution for the q-color problem in d dimensions.

Exploratory study of the effects of wing-leading-edge modifications on the stall/spin behavior of a light general aviation airplane

NASA Technical Reports Server (NTRS)

1979-01-01

Configurations with full-span and segmented leading-edge flaps and full-span and segmented leading-edge droop were tested. Studies were conducted with wind-tunnel models, with an outdoor radio-controlled model, and with a full-scale airplane. Results show that wing-leading-edge modifications can produce large effects on stall/spin characteristics, particularly on spin resistance. One outboard wing-leading-edge modification tested significantly improved lateral stability at stall, spin resistance, and developed spin characteristics.

Lieb-Robinson bounds for spin-boson lattice models and trapped ions.

PubMed

Jünemann, J; Cadarso, A; Pérez-García, D; Bermudez, A; García-Ripoll, J J

2013-12-06

We derive a Lieb-Robinson bound for the propagation of spin correlations in a model of spins interacting through a bosonic lattice field, which satisfies a Lieb-Robinson bound in the absence of spin-boson couplings. We apply these bounds to a system of trapped ions and find that the propagation of spin correlations, as mediated by the phonons of the ion crystal, can be faster than the regimes currently explored in experiments. We propose a scheme to test the bounds by measuring retarded correlation functions via the crystal fluorescence.

Deficiency of the bulk spin Hall effect model for spin-orbit torques in magnetic-insulator/heavy-metal heterostructures

NASA Astrophysics Data System (ADS)

Li, Junxue; Yu, Guoqiang; Tang, Chi; Liu, Yizhou; Shi, Zhong; Liu, Yawen; Navabi, Aryan; Aldosary, Mohammed; Shao, Qiming; Wang, Kang L.; Lake, Roger; Shi, Jing

2017-06-01

Electrical currents in a magnetic-insulator/heavy-metal heterostructure can induce two simultaneous effects, namely, spin Hall magnetoresistance (SMR) on the heavy-metal side and spin-orbit torques (SOTs) on the magnetic-insulator side. Within the framework of a pure spin current model based on the bulk spin Hall effect (SHE), the ratio of the spin Hall-induced anomalous Hall effect (SH-AHE) to SMR should be equal to the ratio of the fieldlike torque (FLT) to the dampinglike torque (DLT). We perform a quantitative study of SMR, SH-AHE, and SOTs in a series of thulium iron garnet/platinum or T m3F e5O12/Pt heterostructures with different T m3F e5O12 thicknesses, where T m3F e5O12 is a ferrimagnetic insulator with perpendicular magnetic anisotropy. We find the ratio between the measured effective fields of FLT and DLT is at least two times larger than the ratio of the SH-AHE to SMR. In addition, the bulk SHE model grossly underestimates the spin-torque efficiency of FLT. Our results reveal deficiencies of the bulk SHE model and also address the importance of interfacial effects such as the Rashba and magnetic proximity effects in magnetic-insulator/heavy-metal heterostructures.

Spin-dependence of the electron scattering cross section by a magnetic layer system and the magneto-resistance

DOE Office of Scientific and Technical Information (OSTI.GOV)

Wang, J.T.; Tang, F.; Brown, W.D.

1998-12-20

The authors present a theoretical model for calculating the spin-dependent cross section of the scattering of electrons by a magnetic layer system. The model demonstrates that the cross sections of the scattering are different for spin up and spin down electrons. The model assumes that the electrical resistivity in a conductor is proportional to the scattering cross section of the electron in it. It is believed to support the two channel mechanism in interpreting magneto-resistance (MR). Based on the model without considering the scattering due to the interfacial roughness and the spin flipping scattering, the authors have established a relationshipmore » between MR and the square of the magnetic moment in the bulk sample without considering the scattering due to the interfacial roughness and the spin flipping scattering. It can also qualitatively explain the MR difference between the current in plane (CIP) and current perpendicular to the plane (CPP) configurations. The predictions by the model agree well with the experimental findings.« less

Hydrodynamic description of spin Calogero-Sutherland model

NASA Astrophysics Data System (ADS)

Abanov, Alexander; Kulkarni, Manas; Franchini, Fabio

2009-03-01

We study a non-linear collective field theory for an integrable spin-Calogero-Sutherland model. The hydrodynamic description of this SU(2) model in terms of charge density, charge velocity and spin currents is used to study non-perturbative solutions (solitons) and examine their correspondence with known quantum numbers of elementary excitations [1]. A conventional linear bosonization or harmonic approximation is not sufficient to describe, for example, the physics of spin-charge (non)separation. Therefore, we need this new collective bosonic field description that captures the effects of the band curvature. In the strong coupling limit [2] this model reduces to integrable SU(2) Haldane-Shastry model. We study a non-linear coupling of left and right spin currents which form a Kac-Moody algebra. Our quantum hydrodynamic description for the spin case is an extension for the one found in the spinless version in [3].[3pt] [1] Y. Kato,T. Yamamoto, and M. Arikawa, J. Phys. Soc. Jpn. 66, 1954-1961 (1997).[0pt] [2] A. Polychronakos, Phys Rev Lett. 70,2329-2331(1993).[0pt] [3] A.G.Abanov and P.B. Wiegmann, Phys Rev Lett 95, 076402(2005)

Mechanical design of a rotary balance system for NASA. Langley Research Center's vertical spin tunnel

NASA Technical Reports Server (NTRS)

Allred, J. W.; Fleck, V. J.

1992-01-01

A new lightweight Rotary Balance System is presently being fabricated and installed as part of a major upgrade to the existing 20 Foot Vertical Spin Tunnel. This upgrade to improve model testing productivity of the only free spinning vertical wind tunnel includes a modern fan/drive and tunnel control system, an updated video recording system, and the new rotary balance system. The rotary balance is a mechanical apparatus which enables the measurement of aerodynamic force and moment data under spinning conditions (100 rpm). This data is used in spin analysis and is vital to the implementation of large amplitude maneuvering simulations required for all new high performance aircraft. The new rotary balance system described in this report will permit greater test efficiency and improved data accuracy. Rotary Balance testing with the model enclosed in a tare bag can also be performed to obtain resulting model forces from the spinning operation. The rotary balance system will be stored against the tunnel sidewall during free flight model testing.

Entanglement in the Anisotropic Kondo Necklace Model

NASA Astrophysics Data System (ADS)

Mendoza-Arenas, J. J.; Franco, R.; Silva-Valencia, J.

We study the entanglement in the one-dimensional Kondo necklace model with exact diagonalization, calculating the concurrence as a function of the Kondo coupling J and an anisotropy η in the interaction between conduction spins, and we review some results previously obtained in the limiting cases η = 0 and 1. We observe that as J increases, localized and conduction spins get more entangled, while neighboring conduction spins diminish their concurrence; localized spins require a minimum concurrence between conduction spins to be entangled. The anisotropy η diminishes the entanglement for neighboring spins when it increases, driving the system to the Ising limit η = 1 where conduction spins are not entangled. We observe that the concurrence does not give information about the quantum phase transition in the anisotropic Kondo necklace model (between a Kondo singlet and an antiferromagnetic state), but calculating the von Neumann block entropy with the density matrix renormalization group in a chain of 100 sites for the Ising limit indicates that this quantity is useful for locating the quantum critical point.

Spin transport in lateral structures with semiconducting channel

NASA Astrophysics Data System (ADS)

Zainuddin, Abu Naser

Spintronics is an emerging field of electronics with the potential to be used in future integrated circuits. Spintronic devices are already making their mark in storage technologies in recent times and there are proposals for using spintronic effects in logic technologies as well. So far, major improvement in spintronic effects, for example, the `spin-valve' effect, is being achieved in metals or insulators as channel materials. But not much progress is made in semiconductors owing to the difficulty in injecting spins into them, which has only very recently been overcome with the combined efforts of many research groups around the world. The key motivations for semiconductor spintronics are their ease in integration with the existing semiconductor technology along with the gate controllability. At present semiconductor based spintronic devices are mostly lateral and are showing a very poor performance compared to their metal or insulator based vertical counterparts. The objective of this thesis is to analyze these devices based on spin-transport models and simulations. At first a lateral spin-valve device is modeled with the spin-diffusion equation based semiclassical approach. Identifying the important issues regarding the device performance, a compact circuit equivalent model is presented which would help to improve the device design. It is found that the regions outside the current path also have a significant influence on the device performance under certain conditions, which is ordinarily neglected when only charge transport is considered. Next, a modified spin-valve structure is studied where the spin signal is controlled with a gate in between the injecting and detecting contacts. The gate is used to modulate the rashba spin-orbit coupling of the channel which, in turn, modulates the spin-valve signal. The idea of gate controlled spin manipulation was originally proposed by Datta and Das back in 1990 and is called 'Datta-Das' effect. In this thesis, we have extended the model described in the original proposal to include the influence of channel dimensions on the nature of electron flow and the contact dimensions on the magnitude and phase of the spin-valve signal. In order to capture the spin-orbit effect a non-equilibrium Green's function (NEGF) based quantum transport model for spin-valve device have been developed which is also explained with simple theoretical treatment based on stationary phase approximation. The model is also compared against a recent experiment that demonstrated such gate modulated spin-valve effect. This thesis also evaluates the possibility of gate controlled magnetization reversal or spin-torque effect as a means to validate this, so called, 'Datta-Das' effect on a more solid footing. Finally, the scope for utilizing topological insulator material in semiconductor spintronics is discussed as a possible future work for this thesis.

Electrons in strong electromagnetic fields: spin effects and radiation reaction (Conference Presentation)

NASA Astrophysics Data System (ADS)

Bauke, Heiko; Wen, Meng; Keitel, Christoph H.

2017-05-01

Various different classical models of electrons including their spin degree of freedom are commonly applied to describe the coupled dynamics of relativistic electron motion and spin precession in strong electromagnetic fields. The spin dynamics is usually governed by the Thomas-Bargmann-Michel-Telegdi equation [1, 2] in these models, while the electron's orbital motion follows the (modified) Lorentz force and a spin-dependent Stern-Gerlach force. Various classical models can lead to different or even contradicting predictions how the spin degree of freedom modifies the electron's orbital motion when the electron moves in strong electromagnetic fields. This discrepancy is rooted in the model-specific energy dependency of the spin induced relativistic Stern-Gerlach force acting on the electron. The Frenkel model [3, 4] and the classical Foldy-Wouthuysen model 5 are compared exemplarily against each other and against the quantum mechanical Dirac equation in order to identify parameter regimes where these classical models make different predictions [6, 7]. Our theoretical results allow for experimental tests of these models. In the setup of the longitudinal Stern-Gerlach effect, the Frenkel model and classical Foldy-Wouthuysen model lead in the relativistic limit to qualitatively different spin effects on the electron trajectory. Furthermore, it is demonstrated that in tightly focused beams in the near infrared the effect of the Stern-Gerlach force of the Frenkel model becomes sufficiently large to be potentially detectable in an experiment. Among the classical spin models, the Frenkel model is certainly prominent for its long history and its wide application. Our results, however, suggest that the classical Foldy-Wouthuysen model is superior as it is qualitatively in better agreement with the quantum mechanical Dirac equation. In ultra strong laser setups at parameter regimes where effects of the Stern-Gerlach force become relevant also radiation reaction effects are expected to set in. We incorporate radiation reaction classically via the Landau-Lifshitz equation and demonstrate that although radiation reaction effects can have a significant effect on the electron trajectory, the Frenkel model and the classical Foldy-Wouthuysen model remain distinguishable also if radiation reaction effects are taken into account. Our calculations are also suitable to verify the Landau-Lifshitz equation for the radiation reaction of electrons and other spin one-half particles. 1. Thomas, L. H., "I. The kinematics of an electron with an axis," The London, Edinburgh, and Dublin Philosophical Magazine and Journal of Science 3(13), 1-22 (1927). 2. Bargmann, V., Michel, L., and Telegdi, V. L., "Precession of the polarization of particles moving in a homogeneous electromagnetic field," Phys. Rev. Lett. 2(10), 435-436 (1959). 3. Frenkel, J., "Die Elektrodynamik des rotierenden Elektrons," Z. Phys. 37(4-5), 243-262 (1926). 4. Frenkel, J., "Spinning electrons," Nature (London) 117(2949), 653-654 (1926). 5. Silenko, A. J., "Foldy-Wouthyusen transformation and semiclassical limit for relativistic particles in strong external fields," Phys. Rev. A 77(1), 012116 (2008). 6. Wen, M., Bauke, H., and Keitel, C. H., "Identifying the Stern-Gerlach force of classical electron dynamics," Sci. Rep. 6, 31624 (2016). 7. Wen, M., Keitel, C. H., and Bauke, H., "Spin one-half particles in strong electromagnetic fields: spin effects and radiation reaction," arXiv:1610.08951 (2016).

TESTING WIND AS AN EXPLANATION FOR THE SPIN PROBLEM IN THE CONTINUUM-FITTING METHOD

DOE Office of Scientific and Technical Information (OSTI.GOV)

You, Bei; Czerny, Bożena; Sobolewska, Małgosia

2016-04-20

The continuum-fitting method is one of the two most advanced methods of determining the black hole spin in accreting X-ray binary systems. There are, however, still some unresolved issues with the underlying disk models. One of these issues manifests as an apparent decrease in spin for increasing source luminosity. Here, we perform a few simple tests to establish whether outflows from the disk close to the inner radius can address this problem. We employ four different parametric models to describe the wind and compare these to the apparent decrease in spin with luminosity measured in the sources LMC X-3 andmore » GRS 1915+105. Wind models in which parameters do not explicitly depend on the accretion rate cannot reproduce the spin measurements. Models with mass accretion rate dependent outflows, however, have spectra that emulate the observed ones. The assumption of a wind thus effectively removes the artifact of spin decrease. This solution is not unique; the same conclusion can be obtained using a truncated inner disk model. To distinguish among the valid models, we will need high-resolution X-ray data and a realistic description of the Comptonization in the wind.« less

Tester Detects Steady-Short Or Intermittent-Open Circuits

NASA Technical Reports Server (NTRS)

Anderson, Bobby L.

1990-01-01

Momentary open circuits or steady short circuits trigger buzzer. Simple, portable, lightweight testing circuit sounds long-duration alarm when it detects steady short circuit or momentary open circuit in coaxial cable or other two-conductor transmission line. Tester sensitive to discontinuities lasting 10 microseconds or longer. Used extensively for detecting intermittent open shorts in accelerometer and extensometer cables. Also used as ordinary buzzer-type continuity checker to detect steady short or open circuits.

New name can sharpen a hospital's image--or diffuse checkered past.

PubMed

Burns, J

1992-06-22

Hospitals change their names for a variety of reasons. Some seek a new identity that conveys a wider range of services; others need a new moniker as a result of a merger; still others hope a change can help the facility erase past problems. Whatever the case may be, a hospital's decision to change its name has evolved from a mere technical formality to a competitive, and often costly, marketing strategy.

CAN YOU MAKE A PICTURE TO SUGGEST, A MANUAL OF IDEAS AND MATERIALS FOR A CONTEMPORARY CLASSROOM MATH RESEARCH CENTER.

ERIC Educational Resources Information Center

BUCKS COUNTY SCHOOL STUDY COUNCIL

A MATH RESEARCH CENTER MAY BE SET UP IN A CORNER OF A ROOM, PERFERABLY WITH A CHALK BOARD. CHILDREN ARE ABLE TO CREATE MANY OF THE GAMES, CHARTS AND STORIES TO BE USED IN SUCH A CENTER. THE CENTER MAY BE SUPPLEMENTED WITH BOOKS, GAMES, BLOCKS, POPPIT BEADS, COUNTERS, CHECKERS, AND NUMBER LINE CHARTS. ATTENTION IS GIVEN TO A WIDE VARIETY OF…

Implementation of a Loosely-Coupled Lockstep Approach in the Xilinx Zynq-7000 All Programmable SoC for High Consequence Applications

DTIC Science & Technology

2017-03-01

Implementation of a Loosely-Coupled Lockstep Approach in the Xilinx Zynq-7000 All Programmable SoC™ for High Consequence Applications Ryan D...sandia.gov Abstract: For high consequence applications requiring information assurance, the architecture of the Xilinx Zynq- 7000 All Programmable ...transaction checker residing in the Programmable Logic portion of the Zynq device will be discussed along with implementation results and latency

Green Flight Challenge

NASA Image and Video Library

2011-09-28

CAFE Foundation Hanger Boss Mike Fenn waves the speed competition checkered flag for the PhoEnix aircraft during the 2011 Green Flight Challenge, sponsored by Google, at the Charles M. Schulz Sonoma County Airport in Santa Rosa, Calif. on Thursday, Sept. 29, 2011. NASA and the Comparative Aircraft Flight Efficiency (CAFE) Foundation are having the challenge with the goal to advance technologies in fuel efficiency and reduced emissions with cleaner renewable fuels and electric aircraft. Photo Credit: (NASA/Bill Ingalls)

Green Flight Challenge

NASA Image and Video Library

2011-09-28

CAFE Foundation Hanger Boss Mike Fenn waves the speed competition checkered flag for the EcoEagle aircraft during the 2011 Green Flight Challenge, sponsored by Google, at the Charles M. Schulz Sonoma County Airport in Santa Rosa, Calif. on Thursday, Sept. 29, 2011. NASA and the Comparative Aircraft Flight Efficiency (CAFE) Foundation are having the challenge with the goal to advance technologies in fuel efficiency and reduced emissions with cleaner renewable fuels and electric aircraft. Photo Credit: (NASA/Bill Ingalls)

Green Flight Challenge

NASA Image and Video Library

2011-09-28

CAFE Foundation Hanger Boss Mike Fenn waves the speed competition checkered flag for the e-Genius aircraft during the 2011 Green Flight Challenge, sponsored by Google, at the Charles M. Schulz Sonoma County Airport in Santa Rosa, Calif. on Thursday, Sept. 29, 2011. NASA and the Comparative Aircraft Flight Efficiency (CAFE) Foundation are having the challenge with the goal to advance technologies in fuel efficiency and reduced emissions with cleaner renewable fuels and electric aircraft. Photo Credit: (NASA/Bill Ingalls)

Spin supercurrent and effect of quantum phase transition in the two-dimensional XY model

NASA Astrophysics Data System (ADS)

Lima, L. S.

2018-04-01

We have verified the influence of quantum phase transition on spin transport in the spin-1 two-dimensional XY model on the square lattice, with easy plane, single ion and exchange anisotropy. We analyze the effect of the phase transition from the Néel phase to the paramagnetic phase on the AC spin conductivity. Our results show a bit influence of the quantum phase transition on the conductivity. We also obtain a conventional spin transport for ω > 0 and an ideal spin transport in the limit of DC conductivity and therefore, a superfluid spin transport for the DC current in this limit. We have made the diagrammatic expansion for the Green-function with objective to include the effect exciton-exciton scattering on the results.

Quantum Correlation in the XY Spin Model with Anisotropic Three-Site Interaction

NASA Astrophysics Data System (ADS)

Wang, Yao; Chai, Bing-Bing; Guo, Jin-Liang

2018-05-01

We investigate pairwise entanglement and quantum discord (QD) in the XY spin model with anisotropic three-site interaction at zero and finite temperatures. For both the nearest-neighbor spins and the next nearest-neighbor spins, special attention is paid to the dependence of entanglement and QD on the anisotropic parameter δ induced by the next nearest-neighbor spins. We show that the behavior of QD differs in many ways from entanglement under the influences of the anisotropic three-site interaction at finite temperatures. More important, comparing the effects of δ on the entanglement and QD, we find the anisotropic three-site interaction plays an important role in the quantum correlations at zero and finite temperatures. It is found that δ can strengthen the quantum correlation for both the nearest-neighbor spins and the next nearest-neighbor spins, especially for the nearest-neighbor spins at low temperature.

Matrix-assisted relaxation in Fe(phen)2(NCS)2 spin-crossover microparticles, experimental and theoretical investigations

NASA Astrophysics Data System (ADS)

Enachescu, Cristian; Tanasa, Radu; Stancu, Alexandru; Tissot, Antoine; Laisney, Jérôme; Boillot, Marie-Laure

2016-07-01

In this study, we present the influence of the embedding matrix on the relaxation of Fe(phen)2(NCS)2 (phen = 1,10-phenanthroline) spin-transition microparticles as revealed by experiments and provide an explanation within the framework of an elastic model based on a Monte-Carlo method. Experiments show that the shape of the high-spin → low-spin relaxation curves is drastically changed when the particles are dispersed in glycerol. This effect was considered in the model by means of interactions between the microparticles and the matrix. A faster start of the relaxation for microparticles embedded in glycerol is due to an initial positive local pressure acting on the edge spin-crossover molecules from the matrix side. This local pressure diminishes and eventually becomes negative during relaxation, as an effect of the decrease of the volume of spin-crossover microparticles from high-spin to low-spin.

The energy source of the most energetic giant outbursts in MS 0735 + 7421

NASA Astrophysics Data System (ADS)

Li, Shuang-Liang

2013-02-01

In this work, we investigate the power source of the most energetic giant outbursts in MS 0735 + 7421, which released ~ 1062 erg of energy. Due to the very high mean jet power in the cavities (P jet/L Edd ~ 0.02), we produce several jet formation models based on a relativistic thin disk model, i.e., general BP + BZ mechanisms (model A), Livio's (model B) and Meier's (model C) model, to explain the giant outbursts in AGNs. It is found that the energy provided by both model B and model C are inadequate for an initial black hole spin a 0 ~ 0.1, only model A can explain the most violent outbursts in MS 0735 + 7421. But if the initial black hole spin a 0 ~ 0.95, model B can also blow up the cavity. The final spin of the black hole is found to be very high in spite of the initial spin.

Spin Seebeck effect in a metal-single-molecule-magnet-metal junction

NASA Astrophysics Data System (ADS)

Niu, Pengbin; Liu, Lixiang; Su, Xiaoqiang; Dong, Lijuan; Luo, Hong-Gang

2018-01-01

We investigate the nonlinear regime of temperature-driven spin-related currents through a single molecular magnet (SMM), which is connected with two metal electrodes. Under a large spin approximation, the SMM is simplified to a natural two-channel model possessing spin-opposite configuration and Coulomb interaction. We find that in temperature-driven case the system can generate spin-polarized currents. More interestingly, at electron-hole symmetry point, the competition of the two channels induces a temperature-driven pure spin current. This device demonstrates that temperature-driven SMM junction shows some results different from the usual quantum dot model, which may be useful in the future design of thermal-based molecular spintronic devices.

Ground-state phase diagram in the Kugel-Khomskii model with finite spin-orbit interactions

NASA Astrophysics Data System (ADS)

Koga, Akihisa; Nakauchi, Shiryu; Nasu, Joji

2018-05-01

We study ground-state properties in the Kugel-Khomskii model on the two-dimensional honeycomb lattice. Using the cluster mean-field approximations, we deal with the exchange and spin-orbit couplings on an equal footing. We then discuss the stability of the ferromagnetically ordered states against the nonmagnetic state, which is adiabatically connected to the quantum spin liquid state realized in a strong spin-orbit coupling limit.

Understanding asteroid collisional history through experimental and numerical studies

NASA Technical Reports Server (NTRS)

Davis, Donald R.; Ryan, Eileen V.; Weidenschilling, S. J.

1991-01-01

Asteroids can lose angular momentum due to so called splash effect, the analog to the drain effect for cratering impacts. Numerical code with the splash effect incorporated was applied to study the simultaneous evolution of asteroid sized and spins. Results are presented on the spin changes of asteroids due to various physical effects that are incorporated in the described model. The goal was to understand the interplay between the evolution of sizes and spins over a wide and plausible range of model parameters. A single starting population was used both for size distribution and the spin distribution of asteroids and the changes in the spins were calculated over solar system history for different model parameters. It is shown that there is a strong coupling between the size and spin evolution, that the observed relative spindown of asteroids approximately 100 km diameter is likely to be the result of the angular momentum splash effect.

Understanding asteroid collisional history through experimental and numerical studies

NASA Astrophysics Data System (ADS)

Davis, Donald R.; Ryan, Eileen V.; Weidenschilling, S. J.

1991-06-01

Asteroids can lose angular momentum due to so called splash effect, the analog to the drain effect for cratering impacts. Numerical code with the splash effect incorporated was applied to study the simultaneous evolution of asteroid sized and spins. Results are presented on the spin changes of asteroids due to various physical effects that are incorporated in the described model. The goal was to understand the interplay between the evolution of sizes and spins over a wide and plausible range of model parameters. A single starting population was used both for size distribution and the spin distribution of asteroids and the changes in the spins were calculated over solar system history for different model parameters. It is shown that there is a strong coupling between the size and spin evolution, that the observed relative spindown of asteroids approximately 100 km diameter is likely to be the result of the angular momentum splash effect.

FAST TRACK COMMUNICATION: Spin waves in the (0, π) and (0, π, π) ordered SDW states of the t-t' Hubbard model: application to doped iron pnictides

NASA Astrophysics Data System (ADS)

Raghuvanshi, Nimisha; Singh, Avinash

2010-10-01

Spin waves in the (0, π) and (0, π, π) ordered spin-density-wave (SDW) states of the t-t' Hubbard model are investigated at finite doping. In the presence of small t', these composite ferro-antiferromagnetic (F-AF) states are found to be strongly stabilized at finite hole doping due to enhanced carrier-induced ferromagnetic spin couplings as in metallic ferromagnets. Anisotropic spin-wave velocities, a spin-wave energy scale of around 200 meV, reduced magnetic moment and rapid suppression of magnetic order with electron doping x (corresponding to F substitution of O atoms in LaO1 - xFxFeAs or Ni substitution of Fe atoms in BaFe2 - xNixAs2) obtained in this model are in agreement with observed magnetic properties of doped iron pnictides.

Spin-splitting calculation for zincblende semiconductors using an atomic bond-orbital model.

PubMed

Kao, Hsiu-Fen; Lo, Ikai; Chiang, Jih-Chen; Chen, Chun-Nan; Wang, Wan-Tsang; Hsu, Yu-Chi; Ren, Chung-Yuan; Lee, Meng-En; Wu, Chieh-Lung; Gau, Ming-Hong

2012-10-17

We develop a 16-band atomic bond-orbital model (16ABOM) to compute the spin splitting induced by bulk inversion asymmetry in zincblende materials. This model is derived from the linear combination of atomic-orbital (LCAO) scheme such that the characteristics of the real atomic orbitals can be preserved to calculate the spin splitting. The Hamiltonian of 16ABOM is based on a similarity transformation performed on the nearest-neighbor LCAO Hamiltonian with a second-order Taylor expansion k at the Γ point. The spin-splitting energies in bulk zincblende semiconductors, GaAs and InSb, are calculated, and the results agree with the LCAO and first-principles calculations. However, we find that the spin-orbit coupling between bonding and antibonding p-like states, evaluated by the 16ABOM, dominates the spin splitting of the lowest conduction bands in the zincblende materials.

Frustrated Magnetism of Dipolar Molecules on a Square Optical Lattice: Prediction of a Quantum Paramagnetic Ground State

NASA Astrophysics Data System (ADS)

Zou, Haiyuan; Zhao, Erhai; Liu, W. Vincent

2017-08-01

Motivated by the experimental realization of quantum spin models of polar molecule KRb in optical lattices, we analyze the spin 1 /2 dipolar Heisenberg model with competing anisotropic, long-range exchange interactions. We show that, by tilting the orientation of dipoles using an external electric field, the dipolar spin system on square lattice comes close to a maximally frustrated region similar, but not identical, to that of the J1-J2 model. This provides a simple yet powerful route to potentially realize a quantum spin liquid without the need for a triangular or kagome lattice. The ground state phase diagrams obtained from Schwinger-boson and spin-wave theories consistently show a spin disordered region between the Néel, stripe, and spiral phase. The existence of a finite quantum paramagnetic region is further confirmed by an unbiased variational ansatz based on tensor network states and a tensor renormalization group.

Spin-neurons: A possible path to energy-efficient neuromorphic computers

NASA Astrophysics Data System (ADS)

Sharad, Mrigank; Fan, Deliang; Roy, Kaushik

2013-12-01

Recent years have witnessed growing interest in the field of brain-inspired computing based on neural-network architectures. In order to translate the related algorithmic models into powerful, yet energy-efficient cognitive-computing hardware, computing-devices beyond CMOS may need to be explored. The suitability of such devices to this field of computing would strongly depend upon how closely their physical characteristics match with the essential computing primitives employed in such models. In this work, we discuss the rationale of applying emerging spin-torque devices for bio-inspired computing. Recent spin-torque experiments have shown the path to low-current, low-voltage, and high-speed magnetization switching in nano-scale magnetic devices. Such magneto-metallic, current-mode spin-torque switches can mimic the analog summing and "thresholding" operation of an artificial neuron with high energy-efficiency. Comparison with CMOS-based analog circuit-model of a neuron shows that "spin-neurons" (spin based circuit model of neurons) can achieve more than two orders of magnitude lower energy and beyond three orders of magnitude reduction in energy-delay product. The application of spin-neurons can therefore be an attractive option for neuromorphic computers of future.

Parallelized traveling cluster approximation to study numerically spin-fermion models on large lattices

DOE PAGES

Mukherjee, Anamitra; Patel, Niravkumar D.; Bishop, Chris; ...

2015-06-08

Lattice spin-fermion models are quite important to study correlated systems where quantum dynamics allows for a separation between slow and fast degrees of freedom. The fast degrees of freedom are treated quantum mechanically while the slow variables, generically referred to as the “spins,” are treated classically. At present, exact diagonalization coupled with classical Monte Carlo (ED + MC) is extensively used to solve numerically a general class of lattice spin-fermion problems. In this common setup, the classical variables (spins) are treated via the standard MC method while the fermion problem is solved by exact diagonalization. The “traveling cluster approximation” (TCA)more » is a real space variant of the ED + MC method that allows to solve spin-fermion problems on lattice sizes with up to 10 3 sites. In this paper, we present a novel reorganization of the TCA algorithm in a manner that can be efficiently parallelized. Finally, this allows us to solve generic spin-fermion models easily on 10 4 lattice sites and with some effort on 10 5 lattice sites, representing the record lattice sizes studied for this family of models.« less

Spin-neurons: A possible path to energy-efficient neuromorphic computers

DOE Office of Scientific and Technical Information (OSTI.GOV)

Sharad, Mrigank; Fan, Deliang; Roy, Kaushik

Recent years have witnessed growing interest in the field of brain-inspired computing based on neural-network architectures. In order to translate the related algorithmic models into powerful, yet energy-efficient cognitive-computing hardware, computing-devices beyond CMOS may need to be explored. The suitability of such devices to this field of computing would strongly depend upon how closely their physical characteristics match with the essential computing primitives employed in such models. In this work, we discuss the rationale of applying emerging spin-torque devices for bio-inspired computing. Recent spin-torque experiments have shown the path to low-current, low-voltage, and high-speed magnetization switching in nano-scale magnetic devices.more » Such magneto-metallic, current-mode spin-torque switches can mimic the analog summing and “thresholding” operation of an artificial neuron with high energy-efficiency. Comparison with CMOS-based analog circuit-model of a neuron shows that “spin-neurons” (spin based circuit model of neurons) can achieve more than two orders of magnitude lower energy and beyond three orders of magnitude reduction in energy-delay product. The application of spin-neurons can therefore be an attractive option for neuromorphic computers of future.« less

Parallelized traveling cluster approximation to study numerically spin-fermion models on large lattices

DOE Office of Scientific and Technical Information (OSTI.GOV)

Mukherjee, Anamitra; Patel, Niravkumar D.; Bishop, Chris

Lattice spin-fermion models are quite important to study correlated systems where quantum dynamics allows for a separation between slow and fast degrees of freedom. The fast degrees of freedom are treated quantum mechanically while the slow variables, generically referred to as the “spins,” are treated classically. At present, exact diagonalization coupled with classical Monte Carlo (ED + MC) is extensively used to solve numerically a general class of lattice spin-fermion problems. In this common setup, the classical variables (spins) are treated via the standard MC method while the fermion problem is solved by exact diagonalization. The “traveling cluster approximation” (TCA)more » is a real space variant of the ED + MC method that allows to solve spin-fermion problems on lattice sizes with up to 10 3 sites. In this paper, we present a novel reorganization of the TCA algorithm in a manner that can be efficiently parallelized. Finally, this allows us to solve generic spin-fermion models easily on 10 4 lattice sites and with some effort on 10 5 lattice sites, representing the record lattice sizes studied for this family of models.« less

Critical behavior of a quantum chain with four-spin interactions in the presence of longitudinal and transverse magnetic fields.

PubMed

Boechat, B; Florencio, J; Saguia, A; de Alcantara Bonfim, O F

2014-03-01

We study the ground-state properties of a spin-1/2 model on a chain containing four-spin Ising-like interactions in the presence of both transverse and longitudinal magnetic fields. We use entanglement entropy and finite-size scaling methods to obtain the phase diagrams of the model. Our numerical calculations reveal a rich variety of phases and the existence of multicritical points in the system. We identify phases with both ferromagnetic and antiferromagnetic orderings. We also find periodically modulated orderings formed by a cluster of like spins followed by another cluster of opposite like spins. The quantum phases in the model are found to be separated by either first- or second-order transition lines.

Three-dimensional vortex-bright solitons in a spin-orbit-coupled spin-1 condensate

NASA Astrophysics Data System (ADS)

Gautam, Sandeep; Adhikari, S. K.

2018-01-01

We demonstrate stable and metastable vortex-bright solitons in a three-dimensional spin-orbit-coupled three-component hyperfine spin-1 Bose-Einstein condensate (BEC) using numerical solution and variational approximation of a mean-field model. The spin-orbit coupling provides attraction to form vortex-bright solitons in both attractive and repulsive spinor BECs. The ground state of these vortex-bright solitons is axially symmetric for weak polar interaction. For a sufficiently strong ferromagnetic interaction, we observe the emergence of a fully asymmetric vortex-bright soliton as the ground state. We also numerically investigate moving solitons. The present mean-field model is not Galilean invariant, and we use a Galilean-transformed mean-field model for generating the moving solitons.

Solvent removal during synthetic and Nephila fiber spinning.

PubMed

Kojic, Nikola; Kojic, Milos; Gudlavalleti, Sauri; McKinley, Gareth

2004-01-01

The process by which spiders make their mechanically superior fiber involves removal of solvent (water) from a concentrated protein solution while the solution flows through a progressively narrowing spinning canal. Our aim was to determine a possible mechanism of spider water removal by using a computational model. To develop appropriate computational techniques for modeling of solvent removal during fiber spinning, a study was first performed using a synthetic solution. In particular, the effect of solvent removal during elongational flow (also exhibited in the spinning canal of the spider) on fiber mechanical properties was examined. The study establishes a model for solvent removal during dry spinning of synthetic fibers, assuming that internal diffusion governs solvent removal and that convective resistance is small. A variable internal solvent diffusion coefficient, dependent on solvent concentration, is also taken into account in the model. An experimental setup for dry (air) spinning was used to make fibers whose diameter was on the order of those made by spiders (approximately 1 microm). Two fibers of different thickness, corresponding to different spinning conditions, were numerically modeled for solvent removal and then mechanically tested. These tests showed that the thinner fiber, which lost more solvent under elongational flow, had 5-fold better mechanical properties (elastic modulus of 100 MPa and toughness of 15 MJ/m3) than the thicker fiber. Even though the mechanical properties were far from those of dragline spider silk (modulus of 10 GPa and toughness of 150 MJ/m3), the experimental methodology and numerical principles developed for the synthetic case proved to be valuable when establishing a model for the Nephila spinning process. In this model, an assumption of rapid convective water removal at the spinning canal wall was made, with internal diffusion of water through the fiber as the governing process. Then the diffusion coefficient of water through the initial spinning solution, obtained ex vivo from the Nephila clavipes major ampullate gland, was determined and incorporated into the numerical procedure, along with the wall boundary conditions and canal geometry. Also, a typical fiber reeling speed during web making, as well as the assumption of a dry exiting fiber, were included in the model. The results show that a cross-section of spinning solution (dope), which is initially 70% water, spends 19 s in the spinning canal in order to emerge dry. While the dope cross-section traverses the canal, its velocity increases from 0.37 mm/s at the entrance to 12.5 mm/s at the canal exit. The obtained results thus indicate that simple diffusion, along with the dry wall boundary condition, is a viable mechanism for water removal during typical Nephila fiber spinning.

Ground-state ordering of the J1-J2 model on the simple cubic and body-centered cubic lattices

NASA Astrophysics Data System (ADS)

Farnell, D. J. J.; Götze, O.; Richter, J.

2016-06-01

The J1-J2 Heisenberg model is a "canonical" model in the field of quantum magnetism in order to study the interplay between frustration and quantum fluctuations as well as quantum phase transitions driven by frustration. Here we apply the coupled cluster method (CCM) to study the spin-half J1-J2 model with antiferromagnetic nearest-neighbor bonds J1>0 and next-nearest-neighbor bonds J2>0 for the simple cubic (sc) and body-centered cubic (bcc) lattices. In particular, we wish to study the ground-state ordering of these systems as a function of the frustration parameter p =z2J2/z1J1 , where z1 (z2) is the number of nearest (next-nearest) neighbors. We wish to determine the positions of the phase transitions using the CCM and we aim to resolve the nature of the phase transition points. We consider the ground-state energy, order parameters, spin-spin correlation functions, as well as the spin stiffness in order to determine the ground-state phase diagrams of these models. We find a direct first-order phase transition at a value of p =0.528 from a state of nearest-neighbor Néel order to next-nearest-neighbor Néel order for the bcc lattice. For the sc lattice the situation is more subtle. CCM results for the energy, the order parameter, the spin-spin correlation functions, and the spin stiffness indicate that there is no direct first-order transition between ground-state phases with magnetic long-range order, rather it is more likely that two phases with antiferromagnetic long range are separated by a narrow region of a spin-liquid-like quantum phase around p =0.55 . Thus the strong frustration present in the J1-J2 Heisenberg model on the sc lattice may open a window for an unconventional quantum ground state in this three-dimensional spin model.

Two-nucleon high-spin states, the Bansal-French model and the crude shell model

NASA Astrophysics Data System (ADS)

Chan, Tsan Ung

1987-08-01

Recent data on two-nucleon stretched high-spin states agree well with the crude shell model predictions. For two-neutron high-spin states, the A and T linear dependence of B2n in the Bansal-French model can be deduced from the A and T linear dependence of Bn and the crude shell model. 7-2 states in some Zn and Ge even nuclei might be two-proton states. This hypothesis should be confirmed by two-proton transfer reaction.

The bilinear-biquadratic model on the complete graph

NASA Astrophysics Data System (ADS)

Jakab, Dávid; Szirmai, Gergely; Zimborás, Zoltán

2018-03-01

We study the spin-1 bilinear-biquadratic model on the complete graph of N sites, i.e. when each spin is interacting with every other spin with the same strength. Because of its complete permutation invariance, this Hamiltonian can be rewritten as the linear combination of the quadratic Casimir operators of \

Constraints on Exotic Spin-Dependent Interactions Between Matter and Antimatter from Antiprotonic Helium Spectroscopy

NASA Astrophysics Data System (ADS)

Ficek, Filip; Fadeev, Pavel; Flambaum, Victor V.; Jackson Kimball, Derek F.; Kozlov, Mikhail G.; Stadnik, Yevgeny V.; Budker, Dmitry

2018-05-01

Heretofore undiscovered spin-0 or spin-1 bosons can mediate exotic spin-dependent interactions between standard model particles. Here, we carry out the first search for semileptonic spin-dependent interactions between matter and antimatter. We compare theoretical calculations and spectroscopic measurements of the hyperfine structure of antiprotonic helium to constrain exotic spin- and velocity-dependent interactions between electrons and antiprotons.

Constraints on Exotic Spin-Dependent Interactions Between Matter and Antimatter from Antiprotonic Helium Spectroscopy.

PubMed

Ficek, Filip; Fadeev, Pavel; Flambaum, Victor V; Jackson Kimball, Derek F; Kozlov, Mikhail G; Stadnik, Yevgeny V; Budker, Dmitry

2018-05-04

Heretofore undiscovered spin-0 or spin-1 bosons can mediate exotic spin-dependent interactions between standard model particles. Here, we carry out the first search for semileptonic spin-dependent interactions between matter and antimatter. We compare theoretical calculations and spectroscopic measurements of the hyperfine structure of antiprotonic helium to constrain exotic spin- and velocity-dependent interactions between electrons and antiprotons.

Effective S =2 antiferromagnetic spin chain in the salt (o -MePy-V)FeCl4

NASA Astrophysics Data System (ADS)

Iwasaki, Y.; Kida, T.; Hagiwara, M.; Kawakami, T.; Hosokoshi, Y.; Tamekuni, Y.; Yamaguchi, H.

2018-02-01

We present a model compound for the S =2 antiferromagnetic (AF) spin chain composed of the salt (o -MePy-V ) FeCl4 . Ab initio molecular-orbital calculations indicate the formation of a partially stacked two-dimensional (2D) spin model comprising five types of exchange interactions between S =1 /2 and S =5 /2 spins, which locate on verdazyl radical and Fe ion, respectively. The magnetic properties of the synthesized crystals indicate that the dominant interaction between the S =1 /2 and S =5 /2 spins stabilizes an S =2 spin in the low-temperature region, and an effective S =2 AF chain is formed for T ≪10 K and H <4 T. We explain the magnetization curve and electron-spin-resonance modes quantitatively based on the S =2 AF chain. At higher fields above quantitatively 4 T, the magnetization curve assumes two-thirds of the full saturation value for fields between 4 and 20 T, and approaches saturation at ˜40 T. The spin model in the high-field region can be considered as a quasi-2D S =1 /2 honeycomb lattice under an effective internal field caused by the fully polarized S =5 /2 spin.

Explaining LIGO's observations via isolated binary evolution with natal kicks

NASA Astrophysics Data System (ADS)

Wysocki, Daniel; Gerosa, Davide; O'Shaughnessy, Richard; Belczynski, Krzysztof; Gladysz, Wojciech; Berti, Emanuele; Kesden, Michael; Holz, Daniel E.

2018-02-01

We compare binary evolution models with different assumptions about black-hole natal kicks to the first gravitational-wave observations performed by the LIGO detectors. Our comparisons attempt to reconcile merger rate, masses, spins, and spin-orbit misalignments of all current observations with state-of-the-art formation scenarios of binary black holes formed in isolation. We estimate that black holes (BHs) should receive natal kicks at birth of the order of σ ≃200 (50 ) km /s if tidal processes do (not) realign stellar spins. Our estimate is driven by two simple factors. The natal kick dispersion σ is bounded from above because large kicks disrupt too many binaries (reducing the merger rate below the observed value). Conversely, the natal kick distribution is bounded from below because modest kicks are needed to produce a range of spin-orbit misalignments. A distribution of misalignments increases our models' compatibility with LIGO's observations, if all BHs are likely to have natal spins. Unlike related work which adopts a concrete BH natal spin prescription, we explore a range of possible BH natal spin distributions. Within the context of our models, for all of the choices of σ used here and within the context of one simple fiducial parameterized spin distribution, observations favor low BH natal spin.

Spatiotemporal Access Model Based on Reputation for the Sensing Layer of the IoT

PubMed Central

Guo, Yunchuan; Yin, Lihua; Li, Chao

2014-01-01

Access control is a key technology in providing security in the Internet of Things (IoT). The mainstream security approach proposed for the sensing layer of the IoT concentrates only on authentication while ignoring the more general models. Unreliable communications and resource constraints make the traditional access control techniques barely meet the requirements of the sensing layer of the IoT. In this paper, we propose a model that combines space and time with reputation to control access to the information within the sensing layer of the IoT. This model is called spatiotemporal access control based on reputation (STRAC). STRAC uses a lattice-based approach to decrease the size of policy bases. To solve the problem caused by unreliable communications, we propose both nondeterministic authorizations and stochastic authorizations. To more precisely manage the reputation of nodes, we propose two new mechanisms to update the reputation of nodes. These new approaches are the authority-based update mechanism (AUM) and the election-based update mechanism (EUM). We show how the model checker UPPAAL can be used to analyze the spatiotemporal access control model of an application. Finally, we also implement a prototype system to demonstrate the efficiency of our model. PMID:25177731

Spin-Tunnel Investigation of a 1/20-Scale Model of the Northrop F-5E Airplane

NASA Technical Reports Server (NTRS)

Scher, Stanley H.; White, William L.

1977-01-01

An investigation has been conducted in the Langley spin tunnel to determine the spin and recovery characteristics of a 1/20-scale model of the Northrop F-5E airplane. The investigation included erect and inverted spins, a range of center-of- gravity locations and moments of inertia, symmetric and asymmetric store loadings, and a determination of the parachute size required for emergency spin recovery. The effects of increased elevator trailing-edge-up deflections, of leading-edge and trailing-edge flap deflections, and of simulating the geometry of large external stores were also determined.

Photon energy dependence of photo-induced inverse spin-Hall effect in Pt/GaAs and Pt/Ge

DOE Office of Scientific and Technical Information (OSTI.GOV)

Isella, Giovanni, E-mail: giovanni.isella@polimi.it; Bottegoni, Federico; Ferrari, Alberto

2015-06-08

We report the photon energy dependence of photo-induced inverse spin Hall effect (ISHE) in Pt/GaAs and Pt/Ge Schottky junctions. The experimental results are compared with a spin drift-diffusion model, which highlights the role played by the different spin lifetime in the two semiconductors, in determining the energy dependence of the ISHE signal detected in the Pt layer. The good qualitative agreement between experiments and modelling indicates that photo-induced ISHE can be used as a tool to characterize spin lifetime in semiconductors.

Separated spin-up and spin-down quantum hydrodynamics of degenerated electrons: Spin-electron acoustic wave appearance.

PubMed

Andreev, Pavel A

2015-03-01

The quantum hydrodynamic (QHD) model of charged spin-1/2 particles contains physical quantities defined for all particles of a species including particles with spin-up and with spin-down. Different populations of states with different spin directions are included in the spin density (the magnetization). In this paper I derive a QHD model, which separately describes spin-up electrons and spin-down electrons. Hence electrons with different projections of spins on the preferable direction are considered as two different species of particles. It is shown that the numbers of particles with different spin directions do not conserve. Hence the continuity equations contain sources of particles. These sources are caused by the interactions of the spins with the magnetic field. Terms of similar nature arise in the Euler equation. The z projection of the spin density is no longer an independent variable. It is proportional to the difference between the concentrations of the electrons with spin-up and the electrons with spin-down. The propagation of waves in the magnetized plasmas of degenerate electrons is considered. Two regimes for the ion dynamics, the motionless ions and the motion of the degenerate ions as the single species with no account of the spin dynamics, are considered. It is shown that this form of the QHD equations gives all solutions obtained from the traditional form of QHD equations with no distinction of spin-up and spin-down states. But it also reveals a soundlike solution called the spin-electron acoustic wave. Coincidence of most solutions is expected since this derivation was started with the same basic equation: the Pauli equation. Solutions arise due to the different Fermi pressures for the spin-up electrons and the spin-down electrons in the magnetic field. The results are applied to degenerate electron gas of paramagnetic and ferromagnetic metals in the external magnetic field. The dispersion of the spin-electron acoustic waves in the partially spin-polarized degenerate neutron matter are also considered.

The Checkerboard Model of the Nucleus

NASA Astrophysics Data System (ADS)

Lach, Theodore

2015-04-01

The Checker Board Model (CBM) of the nucleus and the associated extended standard model predicts that nature has 5 generations of quarks not 3 and that Nucleus is 2 dimensional. The CBM theory began with an insight into the structure of the He nucleus around the year 1989. Details of how this theory evolved which took many years, and is found on my web site (http://checkerboard.dnsalias.net) or in the following references One independent check of this model is that the wavelength of the ``up'' quark orbiting inside the proton at 84.8123% the speed of light (around the ``dn'' quark in the center of the proton) turns out to be exactly one de Broglie wavelength something determined after the mass and speed of the up quark were determined by other means. This theory explains the mass of the proton and neutron and their magnetic moments and this along with the beautiful symmetric 2D structure of the He nucleus led to the evolution of this theory. When this theory was first presented at Argonne in 1996, it was the first time that anyone had predicted the quarks orbited inside the proton at relativistic speeds and it was met with skepticism.

Special Relativity at the Quantum Scale

PubMed Central

Lam, Pui K.

2014-01-01

It has been suggested that the space-time structure as described by the theory of special relativity is a macroscopic manifestation of a more fundamental quantum structure (pre-geometry). Efforts to quantify this idea have come mainly from the area of abstract quantum logic theory. Here we present a preliminary attempt to develop a quantum formulation of special relativity based on a model that retains some geometric attributes. Our model is Feynman's “checker-board” trajectory for a 1-D relativistic free particle. We use this model to guide us in identifying (1) the quantum version of the postulates of special relativity and (2) the appropriate quantum “coordinates”. This model possesses a useful feature that it admits an interpretation both in terms of paths in space-time and in terms of quantum states. Based on the quantum version of the postulates, we derive a transformation rule for velocity. This rule reduces to the Einstein's velocity-addition formula in the macroscopic limit and reveals an interesting aspect of time. The 3-D case, time-dilation effect, and invariant interval are also discussed in term of this new formulation. This is a preliminary investigation; some results are derived, while others are interesting observations at this point. PMID:25531675

Special relativity at the quantum scale.

PubMed

Lam, Pui K

2014-01-01

It has been suggested that the space-time structure as described by the theory of special relativity is a macroscopic manifestation of a more fundamental quantum structure (pre-geometry). Efforts to quantify this idea have come mainly from the area of abstract quantum logic theory. Here we present a preliminary attempt to develop a quantum formulation of special relativity based on a model that retains some geometric attributes. Our model is Feynman's "checker-board" trajectory for a 1-D relativistic free particle. We use this model to guide us in identifying (1) the quantum version of the postulates of special relativity and (2) the appropriate quantum "coordinates". This model possesses a useful feature that it admits an interpretation both in terms of paths in space-time and in terms of quantum states. Based on the quantum version of the postulates, we derive a transformation rule for velocity. This rule reduces to the Einstein's velocity-addition formula in the macroscopic limit and reveals an interesting aspect of time. The 3-D case, time-dilation effect, and invariant interval are also discussed in term of this new formulation. This is a preliminary investigation; some results are derived, while others are interesting observations at this point.

Dynamical Reduction of the Dimensionality of Exchange Interactions and the "Spin-Liquid" Phase of κ-(BEDT-TTF)_{2}X.

PubMed

Powell, B J; Kenny, E P; Merino, J

2017-08-25

We show that the anisotropy of the effective spin model for the dimer Mott insulator phase of κ-(BEDT-TTF)_{2}X salts is dramatically different from that of the underlying tight-binding model. Intradimer quantum interference results in a model of coupled spin chains, where frustrated interchain interactions suppress long-range magnetic order. Thus, we argue, the "spin liquid" phase observed in some of these materials is a remnant of the Tomonaga-Luttinger physics of a single chain. This is consistent with previous experiments and resolves some outstanding puzzles.

Spin-orbit coupling, electron transport and pairing instabilities in two-dimensional square structures

DOE Office of Scientific and Technical Information (OSTI.GOV)

Kocharian, Armen N.; Fernando, Gayanath W.; Fang, Kun

Rashba spin-orbit effects and electron correlations in the two-dimensional cylindrical lattices of square geometries are assessed using mesoscopic two-, three- and four-leg ladder structures. Here the electron transport properties are systematically calculated by including the spin-orbit coupling in tight binding and Hubbard models threaded by a magnetic flux. These results highlight important aspects of possible symmetry breaking mechanisms in square ladder geometries driven by the combined effect of a magnetic gauge field spin-orbit interaction and temperature. The observed persistent current, spin and charge polarizations in the presence of spin-orbit coupling are driven by separation of electron and hole charges andmore » opposite spins in real-space. The modeled spin-flip processes on the pairing mechanism induced by the spin-orbit coupling in assembled nanostructures (as arrays of clusters) engineered in various two-dimensional multi-leg structures provide an ideal playground for understanding spatial charge and spin density inhomogeneities leading to electron pairing and spontaneous phase separation instabilities in unconventional superconductors. Such studies also fall under the scope of current challenging problems in superconductivity and magnetism, topological insulators and spin dependent transport associated with numerous interfaces and heterostructures.« less

Investigation of Incipient Spin Characteristics of a 1/35-Scale Model of the Convair F-102A Airplane, Coord. No. AF-AM-79

NASA Technical Reports Server (NTRS)

Healy, Frederick M.

1958-01-01

Incipient spin characteristics have been investigated on a l/35-scale dynamic model of the Convair F-10% airplane. The model was launched by a catapult apparatus into free flight with various control settings, and the motions obtained were photographed. The model was ballasted for the combat loading. All tests were made with the speed brakes and landing gear retracted, and engine effects were not simulated. The results of the investigation indicated that the model would enter motions apparently simulating entry phases of spins when the elevators were deflected full up. Deflecting the rudder had little effect on the direction of the motion obtained, but when ailerons were deflected the model always rotated in a direction opposite to the aileron setting (that is, the model entered a right spin with the stick to the left). The ailerons were very influential in initiating spin entry, and the pilot should avoid, as far as possible, the use of ailerons in low-speed flight.

SPIN EVOLUTION OF ACCRETING YOUNG STARS. I. EFFECT OF MAGNETIC STAR-DISK COUPLING

DOE Office of Scientific and Technical Information (OSTI.GOV)

Matt, Sean P.; Greene, Thomas P.; Pinzon, Giovanni

2010-05-10

We present a model for the rotational evolution of a young, solar mass star interacting with an accretion disk. The model incorporates a description of the angular momentum transfer between the star and the disk due to a magnetic connection, and includes changes in the star's mass and radius and a decreasing accretion rate. The model also includes, for the first time in a spin evolution model, the opening of the stellar magnetic field lines, as expected to arise from twisting via star-disk differential rotation. In order to isolate the effect that this has on the star-disk interaction torques, wemore » neglect the influence of torques that may arise from open field regions connected to the star or disk. For a range of magnetic field strengths, accretion rates, and initial spin rates, we compute the stellar spin rates of pre-main-sequence stars as they evolve on the Hayashi track to an age of 3 Myr. How much the field opening affects the spin depends on the strength of the coupling of the magnetic field to the disk. For the relatively strong coupling (i.e., high magnetic Reynolds number) expected in real systems, all models predict spin periods of less than {approx}3 days, in the age range of 1-3 Myr. Furthermore, these systems typically do not reach an equilibrium spin rate within 3 Myr, so that the spin at any given time depends upon the choice of initial spin rate. This corroborates earlier suggestions that, in order to explain the full range of observed rotation periods of approximately 1-10 days, additional processes, such as the angular momentum loss from powerful stellar winds, are necessary.« less

Quantum-critical theory of the spin-fermion model and its application to cuprates: normal state analysis

NASA Astrophysics Data System (ADS)

Abanov, Ar.; Chubukov, Andrey V.; Schmalian, J.

2003-03-01

We present the full analysis of the normal state properties of the spin-fermion model near the antiferromagnetic instability in two dimensions. The model describes low-energy fermions interacting with their own collective spin fluctuations, which soften at the antiferromagnetic transition. We argue that in 2D, the system has two typical energies-an effective spin-fermion interaction bar g and an energy ysf below which the system behaves as a Fermi liquid. The ratio of the two determines the dimensionless coupling constant for spin-fermion interaction lambda (2) alpha /line g /omega _{sf} . We show that u scales with the spin correlation length and diverges at criticality. This divergence implies that the conventional perturbative expansion breaks down. We develop a novel approach to the problem-the expansion in either the inverse number of hot spots in the Brillouin zone, or the inverse number of fermionic flavours-which allows us to explicitly account for all terms which diverge as powers of u, and treat the remaining, O(logu) terms in the RG formalism. We apply this technique to study the properties of the spin-fermion model in various frequency and temperature regimes. We present the results for the fermionic spectral function, spin susceptibility, optical conductivity and other observables. We compare our results in detail with the normal state data for the cuprates, and argue that the spin-fermion model is capable of explaining the anomalous normal state properties of the high Tc materials. We also show that the conventional Ӓ theory of the quantum-critical behaviour is inapplicable in 2D due to the singularity of the Ӓ vertex.