An Adjustable Compliant Joint for Lower-Limb Exoskeletons

The field of exoskeletons and wearable devices for walking assistance and rehabilitation has advanced considerably over the past few years. Currently, commercial devices contain joints with stiff actuators that cannot adapt to unpredictable environments. These actuators consume more energy and may not be appropriate for human-machine interactions. Thus, adjustable compliant actuators are being cautiously incorporated into new exoskeletons and active orthoses. Some simulation-based studies have evaluated the benefits of incorporating compliant joints into such devices. Another reason that compliant actuators are desirable is that spasticity and spasmodic movements are common among patients with motor deficiencies; compliant actuators could efficiently absorb these perturbations and improve joint control. In this paper, we provide an overview of the requirements that must be fulfilled by these actuators while evaluating the behavior of leg joints in the locomotion cycle. A brief review of existing compliant actuators is conducted, and our proposed variable stiffness actuator prototype is presented and evaluated. The actuator prototype is implemented in an exoskeleton knee joint operated by a state machine that exploits the dynamics of the leg, resulting in a reduction in actuation energy demand and better adaptability to disturbances.

Aplicação de modelos de defeitos na geração de conjuntos de teste completos a partir de Sistemas de Transição com Entrada/Saída

O Teste Baseado em Modelos (TBM) emergiu como uma estratégia promissora para minimizar problemas relacionados à falta de tempo e recursos em teste de software e visa verificar se a implementação sob teste está em conformidade com sua especificação. Casos de teste são gerados automaticamente a partir de modelos comportamentais produzidos durante o ciclo de desenvolvimento de software. Entre as técnicas de modelagem existentes, Sistemas de Transição com Entrada/Saída (do inglês, Input/Output Transition Systems - IOTSs), são modelos amplamente utilizados no TBM por serem mais expressivos do que Máquinas de Estado Finito (MEFs). Apesar dos métodos existentes para geração de testes a partir de IOTSs, o problema da seleção de casos de testes é um tópico difícil e importante. Os métodos existentes para IOTS são não-determinísticos, ao contrário da teoria existente para MEFs, que fornece garantia de cobertura completa com base em um modelo de defeitos. Esta tese investiga a aplicação de modelos de defeitos em métodos determinísticos de geração de testes a partir de IOTSs. Foi proposto um método para geração de conjuntos de teste com base no método W para MEFs. O método gera conjuntos de teste de forma determinística além de satisfazer condições de suficiência de cobertura da especificação e de todos os defeitos do domínio de defeitos definido. Estudos empíricos avaliaram a aplicabilidade e eficácia do método proposto: resultados experimentais para analisar o custo de geração de conjuntos de teste utilizando IOTSs gerados aleatoriamente e um estudo de caso com especificações da indústria mostram a efetividade dos conjuntos gerados em relação ao método tradicional de Tretmans.

A diffusion approach to approximating preservation probabilities for gene duplicates

Consider a haploid population and, within its genome, a gene whose presence is vital for the survival of any individual. Each copy of this gene is subject to mutations which destroy its function. Suppose one member of the population somehow acquires a duplicate copy of the gene, where the duplicate is fully linked to the original gene's locus. Preservation is said to occur if eventually the entire population consists of individuals descended from this one which initially carried the duplicate. The system is modelled by a finite state-space Markov process which in turn is approximated by a diffusion process, whence an explicit expression for the probability of preservation is derived. The event of preservation can be compared to the fixation of a selectively neutral gene variant initially present in a single individual, the probability of which is the reciprocal of the population size. For very weak mutation, this and the probability of preservation are equal, while as mutation becomes stronger, the preservation probability tends to double this reciprocal. This is in excellent agreement with simulation studies.

On parameter estimation in population models

We describe methods for estimating the parameters of Markovian population processes in continuous time, thus increasing their utility in modelling real biological systems. A general approach, applicable to any finite-state continuous-time Markovian model, is presented, and this is specialised to a computationally more efficient method applicable to a class of models called density-dependent Markov population processes. We illustrate the versatility of both approaches by estimating the parameters of the stochastic SIS logistic model from simulated data. This model is also fitted to data from a population of Bay checkerspot butterfly (Euphydryas editha bayensis), allowing us to assess the viability of this population. (c) 2006 Elsevier Inc. All rights reserved.

Multi-threaded Communicating Agents in Qu-Prolog

In this tutorial paper we summarise the key features of the multi-threaded Qu-Prolog language for implementing multi-threaded communicating agent applications. Internal threads of an agent communicate using the shared dynamic database used as a generalisation of Linda tuple store. Threads in different agents, perhaps on different hosts, communicate using either a thread-to-thread store and forward communication system, or by a publish and subscribe mechanism in which messages are routed to their destinations based on content test subscriptions. We illustrate the features using an auction house application. This is fully distributed with multiple auctioneers and bidders which participate in simultaneous auctions. The application makes essential use of the three forms of inter-thread communication of Qu-Prolog. The agent bidding behaviour is specified graphically as a finite state automaton and its implementation is essentially the execution of its state transition function. The paper assumes familiarity with Prolog and the basic concepts of multi-agent systems.

Formal verification of ASM designs using the MDG tool

In this paper, we present a formal hardware verification framework linking ASM with MDG. ASM (Abstract State Machine) is a state based language for describing transition systems. MDG (Multiway Decision Graphs) provides symbolic representation of transition systems with support of abstract sorts and functions. We implemented a transformation tool that automatically generates MDG models from ASM specifications, then formal verification techniques provided by the MDG tool, such as model checking or equivalence checking, can be applied on the generated models. We support this work with a case study of an Island Tunnel Controller, which behavior and structure were specified in ASM then using our ASM-MDG tool successfully verified within the MDG tool.

COMPETÊNCIAS LEITORAS E ESCRITORAS NA EDUCAÇÃO BÁSICA DE SÃO PAULO, CIDADANIA E IDEOLOGIA: UMA ABORDAGEM HISTÓRICO-POLÍTICA EXPLORATÓRIA

Esta pesquisa de pós-graduação em nível de Mestrado em Educação, pela Universidade Metodista de São Paulo, esforça-se em promover uma reflexão acerca das políticas públicas, desde a Constituição do Império em 1824 até a Constituição de 1988, que impediram o analfabeto de votar em relação com as políticas educacionais que propunham erradicar o analfabetismo no país, analisando, como um caso específico, a ideologia do trabalho por competências na rede pública estadual de São Paulo. A base conceitual-analítica é dada por teorias marxistas francesas contemporâneas, em particular de Althusser, com relação ao Aparelho Ideológico de Estado e estudos de Baudelot e Establet, tendo como hipótese que a escola pública operou e ainda opera em função dos interesses burgueses de produção. Está dividida em cinco capítulos, estruturalmente adequadas da seguinte forma: Introdução que apresenta o referencial teórico usado para a construção da reflexão proposta, à luz dos estudos de Althusser, Baudelot e Establet e Saes; os capítulos 1 e 2 trazem o esforço da busca histórica e legal das Constituições Brasileiras, do Império até 1988, trazendo sempre um breve histórico das épocas em que elas foram promulgadas, a fim de subsidiar o estudo e apresentar que a proibição do voto do analfabeto sempre esteve presente nas constituições, até 1985 com a Emenda Constitucional que declarava o voto do analfabeto como facultativo , sempre atrelado à situação de competências leitoras e escritoras para o exercício pleno da cidadania; o terceiro capítulo apresenta o levantamento histórico sobre os dados de analfabetismo no Brasil desde os anos de 1900 até o último dado do IBGE nos anos 2000, trazendo um referencial explicativo baseado nos estudos de história da educação de ROMANELLI e na tese de doutoramento do professor da USP, Celso de Rui Beisiegel, o que possibilitou traçar um panorama das políticas públicas da educação consoantes aos acontecimentos políticos e históricos; o quarto capítulo apresenta a Proposta Curricular do Estado de São Paulo (SEE/SP, 2008), possibilitando um breve panorama sobre essa política pública de educação na referida rede e o quinto capítulo apresenta uma reflexão das teorias e dados apresentados, no esforço de refletir a situação do ensino por competências, no caso o das leitoras e escritoras, sempre presentes no enfoque social e econômico do país com um olhar crítico ao analfabetismo e as políticas públicas de educação.

Software Testing and Documenting Automation

This article describes some approaches to problem of testing and documenting automation in information systems with graphical user interface. Combination of data mining methods and theory of finite state machines is used for testing automation. Automated creation of software documentation is based on using metadata in documented system. Metadata is built on graph model. Described approaches improve performance and quality of testing and documenting processes.

INFRAWEBS BPEL-Based Editor for Creating the Semantic Web Services Description

INFRAWEBS project [INFRAWEBS] considers usage of semantics for the complete lifecycle of Semantic Web processes, which represent complex interactions between Semantic Web Services. One of the main initiatives in the Semantic Web is WSMO framework, aiming at describing the various aspects related to Semantic Web Services in order to enable the automation of Web Service discovery, composition, interoperation and invocation. In the paper the conceptual architecture for BPEL-based INFRAWEBS editor is proposed that is intended to construct a part of WSMO descriptions of the Semantic Web Services. The semantic description of Web Services has to cover Data, Functional, Execution and QoS semantics. The representation of Functional semantics can be achieved by adding the service functionality to the process description. The architecture relies on a functional (operational) semantics of the Business Process Execution Language for Web Services (BPEL4WS) and uses abstract state machine (ASM) paradigm. This allows describing the dynamic properties of the process descriptions in terms of partially ordered transition rules and transforming them to WSMO framework.

Automata–based Method for Solving Systems of Linear Constraints in {0,1}

We consider a finite state automata based method of solving a system of linear Diophantine equations with coefficients from the set {-1,0,1} and solutions in {0,1}.

Timed Transition Automata as Numerical Planning Domain

A general technique for transforming a timed finite state automaton into an equivalent automated planning domain based on a numerical parameter model is introduced. Timed transition automata have many applications in control systems and agents models; they are used to describe sequential processes, where actions are labelling by automaton transitions subject to temporal constraints. The language of timed words accepted by a timed automaton, the possible sequences of system or agent behaviour, can be described in term of an appropriate planning domain encapsulating the timed actions patterns and constraints. The time words recognition problem is then posed as a planning problem where the goal is to reach a final state by a sequence of actions, which corresponds to the timed symbols labeling the automaton transitions. The transformation is proved to be correct and complete and it is space/time linear on the automaton size. Experimental results shows that the performance of the planning domain obtained by transformation is scalable for real world applications. A major advantage of the planning based approach, beside of the solving the parsing problem, is to represent in a single automated reasoning framework problems of plan recognitions, plan synthesis and plan optimisation.

Weak Ergodicity of Mt /Mt /N /N + R Queue

2000 Mathematics Subject Classification: 60J27, 60K25.

A framework for transforming, analyzing, and realizing software designs in unified modeling language

Unified Modeling Language (UML) is the most comprehensive and widely accepted object-oriented modeling language due to its multi-paradigm modeling capabilities and easy to use graphical notations, with strong international organizational support and industrial production quality tool support. However, there is a lack of precise definition of the semantics of individual UML notations as well as the relationships among multiple UML models, which often introduces incomplete and inconsistent problems for software designs in UML, especially for complex systems. Furthermore, there is a lack of methodologies to ensure a correct implementation from a given UML design. The purpose of this investigation is to verify and validate software designs in UML, and to provide dependability assurance for the realization of a UML design.^ In my research, an approach is proposed to transform UML diagrams into a semantic domain, which is a formal component-based framework. The framework I proposed consists of components and interactions through message passing, which are modeled by two-layer algebraic high-level nets and transformation rules respectively. In the transformation approach, class diagrams, state machine diagrams and activity diagrams are transformed into component models, and transformation rules are extracted from interaction diagrams. By applying transformation rules to component models, a (sub)system model of one or more scenarios can be constructed. Various techniques such as model checking, Petri net analysis techniques can be adopted to check if UML designs are complete or consistent. A new component called property parser was developed and merged into the tool SAM Parser, which realize (sub)system models automatically. The property parser generates and weaves runtime monitoring code into system implementations automatically for dependability assurance. The framework in the investigation is creative and flexible since it not only can be explored to verify and validate UML designs, but also provides an approach to build models for various scenarios. As a result of my research, several kinds of previous ignored behavioral inconsistencies can be detected.^

Adding Run-Time Monitoring to UML-RT by Modifying the Papyrus-RT Code Generator

In Model-Driven Engineering (MDE), the developer creates a model using a language such as Unified Modeling Language (UML) or UML for Real-Time (UML-RT) and uses tools such as Papyrus or Papyrus-RT that generate code for them based on the model they create. Tracing allows developers to get insights such as which events occur and timing information into their own application as it runs. We try to add monitoring capabilities using Linux Trace Toolkit: next generation (LTTng) to models created in UML-RT using Papyrus-RT. The implementation requires changing the code generator to add tracing statements for the events that the user wants to monitor to the generated code. We also change the makefile to automate the build process and we create an Extensible Markup Language (XML) file that allows developers to view their traces visually using Trace Compass, an Eclipse-based trace viewing tool. Finally, we validate our results using three models we create and trace.

Predicting the metabolic energy costs of bipedalism using evolutionary robotics

To understand the evolution of bipedalism among the homnoids in an ecological context we need to be able to estimate theenerrgetic cost of locomotion in fossil forms. Ideally such an estimate would be based entirely on morphology since, except for the rare instances where footprints are preserved, this is hte only primary source of evidence available. In this paper we use evolutionary robotics techniques (genetic algoritms, pattern generators and mechanical modeling) to produce a biomimentic simulation of bipedalism based on human body dimensions. The mechnaical simulation is a seven-segment, two-dimensional model with motive force provided by tension generators representing the major muscle groups acting around the lower-limb joints. Metabolic energy costs are calculated from the muscel model, and bipedal gait is generated using a finite-state pattern generator whose parameters are produced using a genetic algorithm with locomotor economy (maximum distance for a fixed energy cost) as the fitness criterion. The model is validated by comparing the values it generates with those for modern humans. The result (maximum efficiency of 200 J m-1) is within 15% of the experimentally derived value, which is very encouraging and suggests that this is a useful analytic technique for investigating the locomotor behaviour of fossil forms. Initial work suggests that in the future this technique could be used to estimate other locomotor parameters such as top speed. In addition, the animations produced by this technique are qualitatively very convincing, which suggests that this may also be a useful technique for visualizing bipedal locomotion.