Infants' Understanding of Object Weight: Relations with Action Experience and Strength

Thesis (Ph.D.)--University of Washington, 2016-06

Variation talk: Articulating meaning in statistics

Little is known about the way that teachers articulate notions of variation in their own words. The study reported here was conducted with 17 prospective secondary math and science teachers enrolled in a preservice teacher education course which engaged them in statistical inquiry of testing data. This qualitative study examines how these preservice teachers articulated notions of variation as they compared two distributions. Although the teachers made use of tandard statistical language, they also expressed rich views of variation through nonstandard terminology. This paper details the statistical language used by the rospective teachers, categorizing both standard and nonstandard expressions. Their nonstandard language revealed strong relationships between expressions of variation and expressions of distribution. Implications and the benefits of nonstandard language in statistics are outlined.

Procedures and parameters in the real-time program refinement calculus

The real-time refinement calculus is a formal method for the systematic derivation of real-time programs from real-time specifications in a style similar to the non-real-time refinement calculi of Back and Morgan. In this paper we extend the real-time refinement calculus with procedures and provide refinement rules for refining real-time specifications to procedure calls. A real-time specification can include constraints on, not only what outputs are produced, but also when they are produced. The derived programs can also include time constraints oil when certain points in the program must be reached; these are expressed in the form of deadline commands. Such programs are machine independent. An important consequence of the approach taken is that, not only are the specifications machine independent, but the whole refinement process is machine independent. To implement the machine independent code on a target machine one has a separate task of showing that the compiled machine code will reach all its deadlines before they expire. For real-time programs, externally observable input and output variables are essential. These differ from local variables in that their values are observable over the duration of the execution of the program. Hence procedures require input and output parameter mechanisms that are references to the actual parameters so that changes to external inputs are observable within the procedure and changes to output parameters are externally observable. In addition, we allow value and result parameters. These may be auxiliary parameters, which are used for reasoning about the correctness of real-time programs as well as in the expression of timing deadlines, but do not lead to any code being generated for them by a compiler. (c) 2006 Elsevier B.V. All rights reserved.

Toddler subtraction with large sets: further evidence for an analog-magnitude representation of number

Two experiments were conducted to test the hypothesis that toddlers have access to an analog-magnitude number representation that supports numerical reasoning about relatively large numbers. Three-year-olds were presented with subtraction problems in which initial set size and proportions subtracted were systematically varied. Two sets of cookies were presented and then covered The experimenter visibly subtracted cookies from the hidden sets, and the children were asked to choose which of the resulting sets had more. In Experiment 1, performance was above chance when high proportions of objects (3 versus 6) were subtracted from large sets (of 9) and for the subset of older participants (older than 3 years, 5 months; n = 15), performance was also above chance when high proportions (10 versus 20) were subtracted from the very large sets (of 30). In Experiment 2, which was conducted exclusively with older 3-year-olds and incorporated an important methodological control, the pattern of results for the subtraction tasks was replicated In both experiments, success on the tasks was not related to counting ability. The results of these experiments support the hypothesis that young children have access to an analog-magnitude system for representing large approximate quantities, as performance on these subtraction tasks showed a Webers Law signature, and was independent of conventional number knowledge.

Using context and preferences to implement self-adapting pervasive computing applications

Applications that exploit contextual information in order to adapt their behaviour to dynamically changing operating environments and user requirements are increasingly being explored as part of the vision of pervasive or ubiquitous computing. Despite recent advances in infrastructure to support these applications through the acquisition, interpretation and dissemination of context data from sensors, they remain prohibitively difficult to develop and have made little penetration beyond the laboratory. This situation persists largely due to a lack of appropriately high-level abstractions for describing, reasoning about and exploiting context information as a basis for adaptation. In this paper, we present our efforts to address this challenge, focusing on our novel approach involving the use of preference information as a basis for making flexible adaptation decisions. We also discuss our experiences in applying our conceptual and software frameworks for context and preference modelling to a case study involving the development of an adaptive communication application.

Formal change impact analyses for emulated control software

Processor emulators are a software tool for allowing legacy computer programs to be executed on a modern processor. In the past emulators have been used in trivial applications such as maintenance of video games. Now, however, processor emulation is being applied to safety-critical control systems, including military avionics. These applications demand utmost guarantees of correctness, but no verification techniques exist for proving that an emulated system preserves the original system’s functional and timing properties. Here we show how this can be done by combining concepts previously used for reasoning about real-time program compilation, coupled with an understanding of the new and old software architectures. In particular, we show how both the old and new systems can be given a common semantics, thus allowing their behaviours to be compared directly.

An experiment in the design of distributed programs

This paper describes an experiment in the design of distributed programs. It is based on the theory of Owicki and Gries extended with rules for reasoning about message passing. The experiment is designed to test the effectiveness of the extended theory for designing distributed programs.

Continuous action system refinement

Action systems are a framework for reasoning about discrete reactive systems. Back, Petre and Porres have extended these action systems to continuous action systems, which can be. used to model hybrid systems. In this paper we define a refinement relation, and develop practical data refinement rules for continuous action systems. The meaning of continuous action systems is expressed in terms of a mapping from continuous action systems to action systems. First, we present a new mapping from continuous act ion systems to action systems, such that Back's definition of trace refinement is correct with respect to it. Second, we present a stream semantics that is compatible with the trace semantics, but is preferable to it because it is more general. Although action system trace refinement rules are applicable to continuous action systems with a stream semantics, they are not complete. Finally, we introduce a new data refinement rule that is valid with respect to the stream semantics and can be used to prove refinements that are not possible in the trace semantics, and we analyse the completeness of our new rule in conjunction with the existing trace refinement rules.

Axiomatisation of an Interval Calculus for Theorem Proving

We provide an axiomatisation of the Timed Interval Calculus, a set-theoretic notation for expressing properties of time intervals. We implement the axiomatisation in the Ergo theorem prover in order to allow the machine-checked proof of laws for reasoning about predicates expressed using interval operators. These laws can be then used in the machine-assisted verification of real-time applications.

A TEOLOGIA DO COMPROMISSO NO PENSAMENTO DE ELLEN G. WHITE: UMA PERSPECTIVA DA LIBERDADE CRISTÃ

Este trabalho de pesquisa faz uma abordagem não exaustiva acerca da temática da liberdade na perspectiva da teóloga cristã protestante norte-americana Ellen G. White, partindo do estudo de sua pessoa e dos contextos geopolítico e sociocultural nos quais viveu, avançando ainda para uma noção de sua produção literária e a importância da sistematização de seu pensamento para uma compreensão de sua tratativa quanto ao tema proposto. Toma-se como critério de análise a organização de seu pensamento em três linhas de raciocínios teológicos chamadas, respectivamente, Teologia Integral, Teologia do Compromisso e Teologia do Discipulado, as quais, combinadas, constituem sua perspectiva teológica de liberdade. Mostra-se que a primeira linha justifica as razões da liberdade, a segunda explica como ela ocorre no ser humano, e a terceira propõe o roteiro de sua exteriorização positiva para a humanidade. Segue-se, então, examinando os conceitos, fundamentos, características e desdobramentos temáticos de cada um dos elementos constituintes dos roteiros teológicos mencionados, evidenciando os teólogos que mais influenciaram a autora e apontando as aproximações de sua perspectiva à de teólogos que lhe são posteriores. Em conclusão, propõe-se, na perspectiva da autora, liberdade como expressão significante de uma vida comprometida com o servir em amor de forma piedosa. Liberdade é, assim, uma condição experimentada por aqueles que creem e se submetem a Deus, experimentando uma vida de permanente amor e serviço abnegado ao próximo, realidade testemunhada na prática da genuína piedade cristã. E, por último, desafia-se o leitor à urgente percepção, crítica e reação proativa equilibrada em relação às ideologias humanistas de matriz antropocêntrica exclusiva, mostrando-as como principais fundamentos dos equívocos (pós)modernos de liberdade. Diante dessa realidade, propõe-se a reumanização da ideia de liberdade numa perspectiva teocêntrica por meio do retorno a Deus e à Sua Palavra, empreendimento para o qual a proposta de Ellen G. White se mostra um potencial Teo-humanizador de considerável valor, capaz de possibilitar inclusive o desenvolvimento harmônico da integralidade humana.

A formal methodology for the verification of concurrent systems

There is an increasing emphasis on the use of software to control safety critical plants for a wide area of applications. The importance of ensuring the correct operation of such potentially hazardous systems points to an emphasis on the verification of the system relative to a suitably secure specification. However, the process of verification is often made more complex by the concurrency and real-time considerations which are inherent in many applications. A response to this is the use of formal methods for the specification and verification of safety critical control systems. These provide a mathematical representation of a system which permits reasoning about its properties. This thesis investigates the use of the formal method Communicating Sequential Processes (CSP) for the verification of a safety critical control application. CSP is a discrete event based process algebra which has a compositional axiomatic semantics that supports verification by formal proof. The application is an industrial case study which concerns the concurrent control of a real-time high speed mechanism. It is seen from the case study that the axiomatic verification method employed is complex. It requires the user to have a relatively comprehensive understanding of the nature of the proof system and the application. By making a series of observations the thesis notes that CSP possesses the scope to support a more procedural approach to verification in the form of testing. This thesis investigates the technique of testing and proposes the method of Ideal Test Sets. By exploiting the underlying structure of the CSP semantic model it is shown that for certain processes and specifications the obligation of verification can be reduced to that of testing the specification over a finite subset of the behaviours of the process.

Intelligent execution monitoring and error analysis in planning involving processes

An intelligent agent, operating in an external world which cannot be fully described in its internal world model, must be able to monitor the success of a previously generated plan and to respond to any errors which may have occurred. The process of error analysis requires the ability to reason in an expert fashion about time and about processes occurring in the world. Reasoning about time is needed to deal with causality. Reasoning about processes is needed since the direct effects of a plan action can be completely specified when the plan is generated, but the indirect effects cannot. For example, the action `open tap' leads with certainty to `tap open', whereas whether there will be a fluid flow and how long it might last is more difficult to predict. The majority of existing planning systems cannot handle these kinds of reasoning, thus limiting their usefulness. This thesis argues that both kinds of reasoning require a complex internal representation of the world. The use of Qualitative Process Theory and an interval-based representation of time are proposed as a representation scheme for such a world model. The planning system which was constructed has been tested on a set of realistic planning scenarios. It is shown that even simple planning problems, such as making a cup of coffee, require extensive reasoning if they are to be carried out successfully. The final Chapter concludes that the planning system described does allow the correct solution of planning problems involving complex side effects, which planners up to now have been unable to solve.

Supporting decision-making for self-adaptive systems:from goal models to dynamic decision networks

Context/Motivation - Different modeling techniques have been used to model requirements and decision-making of self-adaptive systems (SASs). Specifically, goal models have been prolific in supporting decision-making depending on partial and total fulfilment of functional (goals) and non-functional requirements (softgoals). Different goalrealization strategies can have different effects on softgoals which are specified with weighted contribution-links. The final decision about what strategy to use is based, among other reasons, on a utility function that takes into account the weighted sum of the different effects on softgoals. Questions/Problems - One of the main challenges about decisionmaking in self-adaptive systems is to deal with uncertainty during runtime. New techniques are needed to systematically revise the current model when empirical evidence becomes available from the deployment. Principal ideas/results - In this paper we enrich the decision-making supported by goal models by using Dynamic Decision Networks (DDNs). Goal realization strategies and their impact on softgoals have a correspondence with decision alternatives and conditional probabilities and expected utilities in the DDNs respectively. Our novel approach allows the specification of preferences over the softgoals and supports reasoning about partial satisfaction of softgoals using probabilities. We report results of the application of the approach on two different cases. Our early results suggest the decision-making process of SASs can be improved by using DDNs. © 2013 Springer-Verlag.

A goal-based modeling approach to develop requirements of an adaptive system with environmental uncertainty

Dynamically adaptive systems (DASs) are intended to monitor the execution environment and then dynamically adapt their behavior in response to changing environmental conditions. The uncertainty of the execution environment is a major motivation for dynamic adaptation; it is impossible to know at development time all of the possible combinations of environmental conditions that will be encountered. To date, the work performed in requirements engineering for a DAS includes requirements monitoring and reasoning about the correctness of adaptations, where the DAS requirements are assumed to exist. This paper introduces a goal-based modeling approach to develop the requirements for a DAS, while explicitly factoring uncertainty into the process and resulting requirements. We introduce a variation of threat modeling to identify sources of uncertainty and demonstrate how the RELAX specification language can be used to specify more flexible requirements within a goal model to handle the uncertainty. © 2009 Springer Berlin Heidelberg.

Dynamic decision-making based on NFR for managing software variability and configuration selection

Due to dynamic variability, identifying the specific conditions under which non-functional requirements (NFRs) are satisfied may be only possible at runtime. Therefore, it is necessary to consider the dynamic treatment of relevant information during the requirements specifications. The associated data can be gathered by monitoring the execution of the application and its underlying environment to support reasoning about how the current application configuration is fulfilling the established requirements. This paper presents a dynamic decision-making infrastructure to support both NFRs representation and monitoring, and to reason about the degree of satisfaction of NFRs during runtime. The infrastructure is composed of: (i) an extended feature model aligned with a domain-specific language for representing NFRs to be monitored at runtime; (ii) a monitoring infrastructure to continuously assess NFRs at runtime; and (iii) a exible decision-making process to select the best available configuration based on the satisfaction degree of the NRFs. The evaluation of the approach has shown that it is able to choose application configurations that well fit user NFRs based on runtime information. The evaluation also revealed that the proposed infrastructure provided consistent indicators regarding the best application configurations that fit user NFRs. Finally, a benefit of our approach is that it allows us to quantify the level of satisfaction with respect to NFRs specification.