Reasoning about real-time repetitions: terminating and nonterminating

It is common for a real-time system to contain a nonterminating process monitoring an input and controlling an output. Hence, a real-time program development method needs to support nonterminating repetitions. In this paper we develop a general proof rule for reasoning about possibly nonterminating repetitions. The rule makes use of a Floyd-Hoare-style loop invariant that is maintained by each iteration of the repetition, a Jones-style relation between the pre- and post-states on each iteration, and a deadline specifying an upper bound on the starting time of each iteration. The general rule is proved correct with respect to a predicative semantics. In the case of a terminating repetition the rule reduces to the standard rule extended to handle real time. Other special cases include repetitions whose bodies are guaranteed to terminate, nonterminating repetitions with the constant true as a guard, and repetitions whose termination is guaranteed by the inclusion of a fixed deadline. (C) 2002 Elsevier Science B.V. All rights reserved.

A formal model of real-time program compilation

Program compilation can be formally defined as a sequence of equivalence-preserving transformations, or refinements, from high-level language programs to assembler code, Recent models also incorporate timing properties, but the resulting formalisms are intimidatingly complex. Here we take advantage of a new, simple model of real-time refinement, based on predicate transformer semantics, to present a straightforward compilation formalism that incorporates real-time constraints. (C) 2002 Elsevier Science B.V. All rights reserved.

A real symmetric Lanczos subspace implementation of quantum scattering using boundary inhomogeneities

We present an efficient and robust method for calculating state-to-state reaction probabilities utilising the Lanczos algorithm for a real symmetric Hamiltonian. The method recasts the time-independent Artificial Boundary Inhomogeneity technique recently introduced by Jang and Light (J. Chem. Phys. 102 (1995) 3262) into a tridiagonal (Lanczos) representation. The calculation proceeds at the cost of a single Lanczos propagation for each boundary inhomogeneity function and yields all state-to-state probabilities (elastic, inelastic and reactive) over an arbitrary energy range. The method is applied to the collinear H + H-2 reaction and the results demonstrate it is accurate and efficient in comparison with previous calculations. (C) 2002 Elsevier Science B.V. All rights reserved.

Chebyshev real wave packet propagation: H+O-2 (J=0) state-to-state reactive scattering calculations

In this paper we explore the relative performance of two recently developed wave packet methodologies for reactive scattering, namely the real wave packet Chebyshev domain propagation of Gray and Balint-Kurti [J. Chem. Phys. 108, 950 (1998)] and the Lanczos subspace wave packet approach of Smith [J. Chem. Phys. 116, 2354 (2002); Chem. Phys. Lett. 336, 149 (2001)]. In the former method, a modified Schrodinger equation is employed to propagate the real part of the wave packet via the well-known Chebyshev iteration. While the time-dependent wave packet from the modified Schrodinger equation is different from that obtained using the standard Schrodinger equation, time-to-energy Fourier transformation yields wave functions which differ only trivially by normalization. In the Lanczos subspace approach the linear system of equations defining the action of the Green operator may be solved via either time-dependent or time-independent methods, both of which are extremely efficient due to the simple tridiagonal structure of the Hamiltonian in the Lanczos representation. The two different wave packet methods are applied to three dimensional reactive scattering of H+O-2 (total J=0). State-to-state reaction probabilities, product state distributions, as well as initial-state-resolved cumulative reaction probabilities are examined. (C) 2002 American Institute of Physics.

Kinetics of baculovirus replication and release using real-time quantitative polymerase chain reaction

The study of viral-based processes is hampered by (a) their complex, transient nature, (b) the instability of products, and (c) the lack of accurate diagnostic assays. Here, we describe the use of real-time quantitative polymerase chain reaction to characterize baculoviral infection. Baculovirus DNA content doubles every 1.7 h from 6 h post-infection until replication is halted at the onset of budding. No dynamic equilibrium exists between replication and release, and the kinetics are independent of the cell density at the time of infection. No more than 16% of the intracellular virus copies bud from the cell. (C) 2002 John Wiley & Sons, Inc. Biotechnol Bioeng 77: 476-480, 2002; DOI 10.1002/bit.10126.

Exotic vs endemic biocontrol agents: Would the real stratiolaelaps miles (Berlese) (Acari : Mesostigmata : Laelapidae), please stand up?

The ability of introduced organisms to invade undisturbed native habitats is a major concern in conservation biology and has resulted in a re-evaluation of the introduction of exotic biocontrol agents, especially of generalist predators. One such agent is Stratiolaelaps miles (Berlese), a predatory mite described from Italy, known from throughout the Holarctic, and apparently accidentally introduced to other areas of the world, including Australia. Initial investigations revealed that putative S. miles could be found in both disturbed and relatively pristine habitats in Queensland, Australia. However, analysis of the mitochondrial DNA of five populations showed most to be highly divergent genetically. Subsequent morphological analysis established two species groups: the lamington-group from cool-temperate to subtropical rainforests in Eastern Australia and the more eurytopic miles-group with a cosmopolitan distribution. We describe two new species from each of these complexes (Stratiolaelaps womersleyi, Stratiolaelaps lamington; Stratiolaelaps marilyn, Stratiolaelaps lorna, respectively), and resurrect Stratiolaelaps scimitus (Womersley), a species which often appears to have been confused with S. miles. Additionally, the large genetic distances among morphologically homogenous species in the miles-group suggest that the apparently cosmopolitan S. miles may be composed of a suite of cryptic species of potentially varying utility in biological control. (C) 2002 Elsevier Science (USA). All rights reserved.

The variety of variables in automated real-time refinement

The refinement calculus is a well-established theory for deriving program code from specifications. Recent research has extended the theory to handle timing requirements, as well as functional ones, and we have developed an interactive programming tool based on these extensions. Through a number of case studies completed using the tool, this paper explains how the tool helps the programmer by supporting the many forms of variables needed in the theory. These include simple state variables as in the untimed calculus, trace variables that model the evolution of properties over time, auxiliary variables that exist only to support formal reasoning, subroutine parameters, and variables shared between parallel processes.

Sistema de controle de remanejamento e reserva t??cnica: siscort

O Sistema de Controle de Remanejamento e Reserva T??cnica (SISCORT) ?? uma tecnologia social in??dita na gest??o p??blica. ?? um inovador instrumento de gest??o no desenvolvimento de pol??ticas p??blicas voltadas para a melhoria da qualidade da educa????o. O SISCORT, por meio de suas consultas e cadastros dispon??veis, ?? ferramenta eficaz na concretiza????o das a????es propostas. Ele facilita, registra e controla o remanejamento dos livros adquiridos e distribu??dos em todas as escolas p??blicas de ensino fundamental, no ??mbito do maior programa do g??nero no mundo, o Programa Nacional do Livro Did??tico (PNLD). Acessando o SISCORT, no s??tio eletr??nico do FNDE, ?? poss??vel saber a quantidade de livros enviados para cada escola, por t??tulo, por s??rie e por componente curricular, permitindo que as escolas, ap??s informar o seu alunado real, saibam, automaticamente, se e onde h?? excesso ou escassez de livros, proporcionando mais transpar??ncia e maior controle social dos recursos p??blicos

Gerenciamento da rede de supervis??o da Eletronorte (GerenteSage)

Como solu????o unificadora da opera????o, em tempo real, de seus sistemas el??tricos, a Eletronorte utiliza, desde 1998, o Sistema Aberto de Gerenciamento de Energia (Sage), que habilita seus centros de opera????o a serem centros estrat??gicos de tratamento de informa????o. A import??ncia do Sage para a empresa reflete-se na relev??ncia da rede que comporta seus dados. Para garantir elevados graus de disponibilidade dos servi??os de supervis??o, foi implementada a ferramenta GerenteSage, que gerencia os recursos da rede e facilita o controle deles pelos administradores. Para essa ferramenta, foi definida uma interface web, a qual condiz com caracter??sticas atuais do mundo da inform??tica: a descentraliza????o do acesso ??s informa????es e a independ??ncia de plataforma para o usu??rio. Outro aspecto importante da metodologia de concep????o ?? a utiliza????o de sistemas e fontes livres. Como resultado, houve melhora na qualidade dos servi??os de rede e aumento da disponibilidade das informa????es de supervis??o

Novos desafios para a capacita????o de lideran??a de alto n??vel na gest??o p??blica e governan??a em um mundo globalizante

Este artigo aborda as mudan??as econ??micas, sociais, ambientais e comportamentais que est??o ocorrendo no planeta, visando a estabelecer um contexto que sirva de base para o tipo de capacita????o mais adequado para os n??veis gerenciais de governo. A partir de tr??s fatores interdependentes ??? globaliza????o, difus??o da democracia e impactos na governan??a ??? ?? proposta uma estrutura de capacita????o, focalizando 12 diferentes ??reas.

Pr??-equidade de g??nero: incorporando pol??ticas de a????o afirmativa no mundo do trabalho

A institui????o do Programa Pr??-equidade de G??nero ?? o reconhecimento p??blico da desigualdade de tratamento e de oportunidades, que ainda permanece entre mulheres e homens. A implementa????o ?? consolidada com a coloca????o em pr??tica dos planos de a????es firmados entre a Secretaria Especial de Pol??ticas para as Mulheres (SPM) e as organiza????es aderentes. A pesquisa explorat??ria teve como objetivo apresentar o programa e discuti-lo com base no modelo "policy cycle como aprendizado", de Silva e Melo (2000). Os resultados subsidiar??o pesquisa futura sobre a avalia????o do programa. Dentro da estrat??gia adotada, a coleta de dados ocorreu em documentos institucionais e dados bibliogr??ficos em mar??o de 2009, com o seguinte resultado: a avalia????o n??o trata de forma clara da efetividade e da sustentabilidade do programa. Este trabalho est?? dividido em seis partes: descri????o do m??todo utilizado; apresenta????o do Programa Pro-equidade de G??nero; avalia????o de suas duas primeiras edi????es; breve contextualiza????o das pol??ticas p??blicas no Brasil e o modelo "policy cicle como aprendizado"; rela????es entre o programa e o modelo; e considera????es finais.