A theory for execution-time derivation in real-time programs

We provide an abstract command language for real-time programs and outline how a partial correctness semantics can be used to compute execution times. The notions of a timed command, refinement of a timed command, the command traversal condition, and the worst-case and best-case execution time of a command are formally introduced and investigated with the help of an underlying weakest liberal precondition semantics. The central result is a theory for the computation of worst-case and best-case execution times from the underlying semantics based on supremum and infimum calculations. The framework is applied to the analysis of a message transmitter program and its implementation. (c) 2005 Elsevier B.V. All rights reserved.

MACPROP:a revised program for the refinement of satellite orbital parameters

DUE TO COPYRIGHT RESTRICTIONS ONLY AVAILABLE FOR CONSULTATION AT ASTON UNIVERSITY LIBRARY AND INFORMATION SERVICES WITH PRIOR ARRANGEMENT

Characteristics of effective clinical and theory instructors as perceived by LPN to RN versus generic students in an associate degree nursing program

The purpose of this study was to compare the characteristics of effective clinical and theory instructors as perceived by LPN/RN versus generic students in an associate degree nursing program.^ Data were collected from 508 students during the 1996-7 academic year from three NLN accredited associate degree nursing programs. The researcher developed instrument consisted of three parts: (a) Whitehead Characteristics of Effective Clinical Instructor Rating Scale, (b) Whitehead Characteristics of Effective Theory Instructor Rating Scale, and (c) Demographic Data Sheet. The items were listed under five major categories identified in the review of the literature: (a) interpersonal relationships, (b) personality traits, (c) teaching practices, (d) knowledge and experience, and (e) evaluation procedures. The instrument was administered to LPN/RN students in their first semester and to generic students in the third semester of an associate degree nursing program.^ Data was analyzed using a one factor mutivariate analysis of variance (MANOVA). Further t tests were carried out to explore for possible differences between type of student and by group. Crosstabulations of the demographic data were analyzed.^ There were no significant differences found between the LPN/RN versus generic students on their perceptions of either effective theory or effective clinical instructor characteristics. There were significant differences between groups on several of the individual items. There was no significant interaction between group and ethnicity or group and age on the five major categories for either of the two instruments. There was a significant main effect of ethnicity on several of the individual items.^ The differences between the means and standard deviations on both instruments were small, suggesting that all of the characteristics listed for effective theory and clinical instructors were important to both groups of students. Effective teaching behaviors, as indicated on the survey instruments, should be taught to students in graduate teacher education programs. These behaviors should also be discussed by faculty coordinators supervising adjunct faculty. Nursing educators in associate degree nursing programs should understand theories of adult learning and implement instructional strategies to enhance minority student success. ^

Program for the Spring 2016 MARAC Meeting: Archival Confluence: Connecting Theory and Practice

Conference Program

Density functional theory and ab initio molecular dynamics study of NO adsorption on Pd(111) and Pt(111) surfaces

The origin of the unique geometry for nitric oxide (NO) adsorption on Pd(111) and Pt(111) surfaces as well as the effect of temperature were studied by density functional theory calculations and ab initio molecular dynamics at finite temperature. We found that at low coverage, the adsorption geometry is determined by electronic interactions, depending sensitively on the adsorption sites and coverages, and the effect of temperature on geometries is significant. At coverage of 0.25 monolayer (ML), adsorbed NO at hollow sites prefer an upright configuration, while NO adsorbed at top sites prefer a tilting configuration. With increase in the coverage up to 0.50 ML, the enhanced steric repulsion lead to the tilting of hollow NO. We found that the tilting was enhanced by the thermal effects. At coverage of 0.75 ML with p(2 x 2)-3NO(fcc+hcp+top) structure, we found that there was no preferential orientation for tilted top NO. The interplay of the orbital hybridization, thermal effects, steric repulsion, and their effects on the adsorption geometries were highlighted at the end.

Theory of nitride oxide adsorption on transition metal (111) surfaces: a first-principles investigation

In this work, we report a density functional theory study of nitric oxide (NO) adsorption on close-packed transition metal (TM) Rh(111), Ir(111), Pd(111) and Pt(111) surfaces in terms of adsorption sites, binding mechanism and charge transfer at a coverage of Theta(NO) = 0.25, 0.50, 0.75 monolayer (ML). Based on our study, an unified picture for the interaction between NO and TM(111) and site preference is established, and valuable insights are obtained. At low coverage (0.25 ML), we find that the interaction of NO/TM(111) is determined by an electron donation and back-donation process via the interplay between NO 5 sigma/2 pi* and TM d-bands. The extent of the donation and back-donation depends critically on the coordination number (adsorption sites) and TM d-band filling, and plays an essential role for NO adsorption on TM surfaces. DFT calculations shows that for TMs with high d-band filling such as Pd and Pt, hollow-site NO is energetically the most favorable, and top-site NO prefers to tilt away from the normal direction. While for TMs with low d-band filling (Rh and Ir), top-site NO perpendicular to the surfaces is energetically most favorable. Electronic structure analysis show that irrespective of the TM and adsorption site, there is a net charge transfer from the substrate to the adsorbate due to overwhelming back-donation from the TM substrate to the adsorbed NO molecules. The adsorption-induced change of the work function with respect to bare surfaces and dipole moment is however site dependent, and the work function increases for hollow-site NO, but decreases for top-site NO, because of differences in the charge redistribution. The interplay between the energetics, lateral interaction and charge transfer, which is element dependent, rationalizes the structural evolution of NO adsorption on TM(111) surfaces in the submonolayer regime.

DESIGN OF CONCRETE PLATFORMS OFFSHORE USING THE THREE-LAYER SHELL THEORY

The concrete offshore platforms, which are subjected a several loading combinations and, thus, requires an analysis more generic possible, can be designed using the concepts adopted to shell elements, but the resistance must be verify in particular cross-sections to shear forces. This work about design of shell elements will be make using the three-layer shell theory. The elements are subject to combined loading of membrane and plate, totalizing eight components of internal forces, which are three membrane forces, three moments (two out-of-plane bending moments and one in-plane, or torsion, moment) and two shear forces. The design method adopted, utilizing the iterative process proposed by Lourenco & Figueiras (1993) obtained from equations of equilibrium developed by Gupta (1896) , will be compared to results of experimentally tested shell elements found in the literature using the program DIANA.

The conserved quantity theory of causation and chance raising

In this paper I offer an 'integrating account' of singular causation, where the term 'integrating' refers to the following program for analysing causation. There are two intuitions about causation, both of which face serious counterexamples when used as the basis for an analysis of causation. The 'process' intuition, which says that causes and effects are linked by concrete processes, runs into trouble with cases of misconnections', where an event which serves to prevent another fails to do so on a particular occasion and yet the two events are linked by causal processes. The chance raising intuition, according to which causes raise the chance of their effects, easily accounts for misconnections but faces the problem of chance lowering causes, a problem easily accounted for by the process approach. The integrating program attempts to provide an analysis of singular causation by synthesising the two insights, so as to solve both problems. In this paper I show that extant versions of the integrating program due to Eells, Lewis, and Menzies fail to account for the chance-lowering counterexample. I offer a new diagnosis of the chance lowering case, and use that as a basis for an integrating account of causation which does solve both cases. In doing so, I accept various assumptions of the integrating program, in particular that there are no other problems with these two approaches. As an example of the process account, I focus on the recent CQ theory of Wesley Salmon (1997).

The rational reconstruction of the research program on classic rationalism: Locke and the empiricist approach

This article intends to rationally reconstruct Locke`s theory of knowledge as incorporated in a research program concerning the nature and structure of the theories and models of rationality. In previous articles we argued that the rationalist program can be subdivided into the classical rationalistic subprogram, which includes the knowledge theories of Descartes, Locke, Hume and Kant, the neoclassical subprogram, which includes the approaches of Duhem, Poincare and Mach, and the critical subprogram of Popper. The subdivision results from the different views of rationality proposed by each one of these subprograms, as well as from the tools made available by each one of them, containing theoretical instruments used to arrange, organize and develop the discussion on rationality, the main one of which is the structure of solution of problems. In this essay we intend to reconstruct the assumptions of Locke`s theory of knowledge, which in our view belongs to the classical rationalistic subprogram because it shares with it the thesis of the identity of (scientific) knowledge and certain knowledge.

Refining specifications to logic programs

The refinement calculus provides a framework for the stepwise development of imperative programs from specifications. In this paper we study a refinement calculus for deriving logic programs. Dealing with logic programs rather than imperative programs has the dual advantages that, due to the expressive power of logic programs, the final program is closer to the original specification, and each refinement step can achieve more. Together these reduce the overall number of derivation steps. We present a logic programming language extended with specification constructs (including general predicates, assertions, and types and invariants) to form a wide-spectrum language. General predicates allow non-executable properties to be included in specifications. Assertions, types and invariants make assumptions about the intended inputs of a procedure explicit, and can be used during refinement to optimize the constructed logic program. We provide a semantics for the extended logic programming language and derive a set of refinement laws. Finally we apply these to an example derivation.

Specification, refinement and verification of concurrent systems - An integration of Object-Z and CSP

This paper presents a method of formally specifying, refining and verifying concurrent systems which uses the object-oriented state-based specification language Object-Z together with the process algebra CSP. Object-Z provides a convenient way of modelling complex data structures needed to define the component processes of such systems, and CSP enables the concise specification of process interactions. The basis of the integration is a semantics of Object-Z classes identical to that of CSP processes. This allows classes specified in Object-Z to he used directly within the CSP part of the specification. In addition to specification, we also discuss refinement and verification in this model. The common semantic basis enables a unified method of refinement to be used, based upon CSP refinement. To enable state-based techniques to be used fur the Object-Z components of a specification we develop state-based refinement relations which are sound and complete with respect to CSP refinement. In addition, a verification method for static and dynamic properties is presented. The method allows us to verify properties of the CSP system specification in terms of its component Object-Z classes by using the laws of the the CSP operators together with the logic for Object-Z.

Three-dimensional structure of RTD-1, a cyclic antimicrobial defensin from rhesus macaque leukocytes

Most mammalian defensins are cationic peptides of 29-42 amino acids long, stabilized by three disulfide bonds. However, recently Tang et al. (1999, Science 286, 498-502) reported the isolation of a new defensin type found in the leukocytes of rhesus macaques. In contrast to all the other defensins found so far, rhesus theta defensin-1 (RTD-1) is composed of just 18 amino acids with the backbone cyclized through peptide bonds. Antibacterial activities of both the native cyclic peptide and a linear form were examined, showing that the cyclic form was 3-fold more active than the open chain analogue [Tang et al. (1999) Science 286, 498-502]. To elucidate the three-dimensional structure of RTD-1 and its open chain analogue, both peptides were synthesized using solid-phase peptide synthesis and tert-butyloxycarbonyl chemistry. The structures of both peptides in aqueous solution were determined from two-dimensional H-1 NMR data recorded at 500 and 750 MHz. Structural constraints consisting of interproton distances and dihedral angles were used as input for simulated-annealing calculations and water refinement with the program CNS. RTD-1 and its open chain analogue oRTD-1 adopt very similar structures in water. Both comprise an extended beta -hairpin structure with turns at one or both ends. The turns are well defined within themselves and seem to be flexible with respect to the extended regions of the molecules. Although the two strands of the beta -sheet are connected by three disulfide bonds, this region displays a degree of flexibility. The structural similarity of RTD-1 and its open chain analogue oRTD-1, as well as their comparable degree of flexibility, support the theory that the additional charges at the termini of the open chain analogue rather than overall differences in structure or flexibility are the cause for oRTD-1's lower antimicrobial activity. In contrast to numerous other antimicrobial peptides, RTD-1 does not display any amphiphilic character, even though surface models of RTD-1 exhibit a certain clustering of positive charges. Some amide protons of RTD-1 that should be solvent-exposed in monomeric beta -sheet structures show low-temperature coefficients, suggesting the possible presence of weak intermolecular hydrogen bonds.

A refinement calculus for logic programs

Existing refinement calculi provide frameworks for the stepwise development of imperative programs from specifications. This paper presents a refinement calculus for deriving logic programs. The calculus contains a wide-spectrum logic programming language, including executable constructs such as sequential conjunction, disjunction, and existential quantification, as well as specification constructs such as general predicates, assumptions and universal quantification. A declarative semantics is defined for this wide-spectrum language based on executions. Executions are partial functions from states to states, where a state is represented as a set of bindings. The semantics is used to define the meaning of programs and specifications, including parameters and recursion. To complete the calculus, a notion of correctness-preserving refinement over programs in the wide-spectrum language is defined and refinement laws for developing programs are introduced. The refinement calculus is illustrated using example derivations and prototype tool support is discussed.