Expansion-based algorithms for finding single pair shortest path on surface

Finding single pair shortest paths on surface is a fundamental problem in various domains, like Geographic Information Systems (GIS) 3D applications, robotic path planning system, and surface nearest neighbor query in spatial database, etc. Currently, to solve the problem, existing algorithms must traverse the entire polyhedral surface. With the rapid advance in areas like Global Positioning System (CPS), Computer Aided Design (CAD) systems and laser range scanner, surface models axe becoming more and more complex. It is not uncommon that a surface model contains millions of polygons. The single pair shortest path problem is getting harder and harder to solve. Based on the observation that the single pair shortest path is in the locality, we propose in this paper efficient methods by excluding part of the surface model without considering them in the search process. Three novel expansion-based algorithms are proposed, namely, Naive algorithm, Rectangle-based Algorithm and Ellipse-based Algorithm. Each algorithm uses a two-step approach to find the shortest path. (1) compute an initial local path. (2) use the value of this initial path to select a search region, in which the global shortest path exists. The search process terminates once the global optimum criteria are satisfied. By reducing the searching region, the performance is improved dramatically in most cases.

Integrating formal specification and software verification and validation

It is not surprising that students are unconvinced about the benefits of formal methods if we do not show them how these methods can be integrated with other activities in the software lifecycle. In this paper, we describe an approach to integrating formal specification with more traditional verification and validation techniques in a course that teaches formal specification and specification-based testing. This is accomplished through a series of assignments on a single software component that involves specifying the component in Object-Z, validating that specification using inspection and a specification animation tool, and then testing an implementation of the specification using test cases derived from the formal specification.

An automated failure mode and effect analysis based on high-level design specificication with behavior trees

Formal methods have significant benefits for developing safety critical systems, in that they allow for correctness proofs, model checking safety and liveness properties, deadlock checking, etc. However, formal methods do not scale very well and demand specialist skills, when developing real-world systems. For these reasons, development and analysis of large-scale safety critical systems will require effective integration of formal and informal methods. In this paper, we use such an integrative approach to automate Failure Modes and Effects Analysis (FMEA), a widely used system safety analysis technique, using a high-level graphical modelling notation (Behavior Trees) and model checking. We inject component failure modes into the Behavior Trees and translate the resulting Behavior Trees to SAL code. This enables us to model check if the system in the presence of these faults satisfies its safety properties, specified by temporal logic formulas. The benefit of this process is tool support that automates the tedious and error-prone aspects of FMEA.

Termination of real-time programs: Definitely, definitely not, or maybe

Real-time control programs are often used in contexts where (conceptually) they run forever. Repetitions within such programs (or their specifications) may either (i) be guaranteed to terminate, (ii) be guaranteed to never terminate (loop forever), or (iii) may possibly terminate. In dealing with real-time programs and their specifications, we need to be able to represent these possibilities, and define suitable refinement orderings. A refinement ordering based on Dijkstra's weakest precondition only copes with the first alternative. Weakest liberal preconditions allow one to constrain behaviour provided the program terminates, which copes with the third alternative to some extent. However, neither of these handles the case when a program does not terminate. To handle this case a refinement ordering based on relational semantics can be used. In this paper we explore these issues and the definition of loops for real-time programs as well as corresponding refinement laws.

Compositional class refinement in object-Z

Object-Z allows coupling constraints between classes which, on the one hand, facilitate specification at a high level of abstraction, but, on the other hand, make class refinement non-compositional. The consequence of this is that refinement is not practical for large Systems. This paper overcomes this limitation by introducing a methodology for compositional class refinement in Object-Z. The key step is an equivalence transformation of an arbitrary Object-Z specification to one in which introduced constraints prohibit non-compositional refinements. The methodology also allows the constraints which couple classes to be refined yielding an unrestricted approach to compositional class refinement.

Context-enhanced authentication for infrastructureless network environments

Infrastructureless networks are becoming more popular with the increased prevalence of wireless networking technology. A significant challenge faced by these infrastructureless networks is that of providing security. In this paper we examine the issue of authentication, a fundamental component of most security approaches, and show how it can be performed despite an absence of trusted infrastructure and limited or no existing trust relationship between network nodes. Our approach enables nodes to authenticate using a combination of contextual information, harvested from the environment, and traditional authentication factors (such as public key cryptography). Underlying our solution is a generic threshold signature scheme that enables distributed generation of digital certificates.

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.

3D protein structure matching by patch signatures

For determining functionality dependencies between two proteins, both represented as 3D structures, it is an essential condition that they have one or more matching structural regions called patches. As 3D structures for proteins are large, complex and constantly evolving, it is computationally expensive and very time-consuming to identify possible locations and sizes of patches for a given protein against a large protein database. In this paper, we address a vector space based representation for protein structures, where a patch is formed by the vectors within the region. Based on our previews work, a compact representation of the patch named patch signature is applied here. A similarity measure of two patches is then derived based on their signatures. To achieve fast patch matching in large protein databases, a match-and-expand strategy is proposed. Given a query patch, a set of small k-sized matching patches, called candidate patches, is generated in match stage. The candidate patches are further filtered by enlarging k in expand stage. Our extensive experimental results demonstrate encouraging performances with respect to this biologically critical but previously computationally prohibitive problem.

Compositional verification for object-Z

This paper presents a framework for compositional verification of Object-Z specifications. Its key feature is a proof rule based on decomposition of hierarchical Object-Z models. For each component in the hierarchy local properties are proven in a single proof step. However, we do not consider components in isolation. Instead, components are envisaged in the context of the referencing super-component and proof steps involve assumptions on properties of the sub-components. The framework is defined for Linear Temporal Logic (LTL)

Interfacing ASM with the MDG tool

In this paper we describe an approach to interface Abstract State Machines (ASM) with Multiway Decision Graphs (MDG) to enable tool support for the formal verification of ASM descriptions. ASM is a specification method for software and hardware providing a powerful means of modeling various kinds of systems. MDGs are decision diagrams based on abstract representation of data and axe used primarily for modeling hardware systems. The notions of ASM and MDG axe hence closely related to each other, making it appealing to link these two concepts. The proposed interface between ASM and MDG uses two steps: first, the ASM model is transformed into a flat, simple transition system as an intermediate model. Second, this intermediate model is transformed into the syntax of the input language of the MDG tool, MDG-HDL. We have successfully applied this transformation scheme on a case study, the Island Tunnel Controller, where we automatically generated the corresponding MDG-HDL models from ASM specifications.

COORDENADORES PEDAGÓGICOS: FORMADORES DE PROFESSORES OU SUPERVISORES DE AÇÕES POLÍTICO-PEDAGÓGICAS DA ESCOLA?

O sistema educacional vem sofrendo influência direta das modificações ocorridas na sociedade, que está cada vez mais exposta a uma gama de informações que nem sempre são transformadas em conhecimento. Essas transformações vão desde uma nova postura do professor em sala de aula até a própria função social da escola, que ainda não responde às necessidades da sociedade. Nesse novo cenário faz-se imprescindível um professor mais preparado para orientar o aluno, ajudando-o a interagir com o outro, a selecionar as informações a que está exposto e a transformá-las em conhecimento, bem como a interagir com seus semelhantes. É importante considerar que aprendizagem do aluno está diretamente relacionada aos métodos de ensino aos quais está submetido. E, para garantir tal aprendizagem é necessário haver uma equipe mais preparada, mais coesa, ciente do trabalho que está desenvolvendo. Por isso a parceria do trabalho entre a coordenação pedagógica e os professores se torna indispensável. Mas será que o coordenador tem esse olhar? Para saber como o coordenador pedagógico atua na formação continuada dos professores, a pesquisa foi desenvolvida com uma parte teórica e uma parte prática. No referencial teórico estão Álvaro Marchesi, Vitor Henrique Paro e José Carlos Libâneo, por sua grande contribuição na área da gestão; Antônio Nóvoa, Cleide Terzi, Laurinda Almeida e Vera Placco, por seus trabalhos sobre formação de professores e de coordenadores pedagógicos, além de dissertações de mestrado e teses de doutorado sobre o tema. Na parte prática a pesquisa se organiza na perspectiva da metodologia quali/quantitativa, com entrevistas com nove coordenadores pedagógicos. Como a ênfase da dissertação está na construção do perfil desse profissional, foram entrevistados coordenadores de diversos segmentos (Educação Infantil, Ensino Fundamental e Ensino Médio) de diferentes escolas (rede particular e pública). No aspecto quantitativo da pesquisa, foi aplicado um questionário a dezesseis professores, para saber da atuação do coordenador pedagógico no aspecto formador. Os resultados mostraram que o coordenador pedagógico também precisa de formação. Ele desempenha tarefas específicas e que não são tratadas nem nas universidades nem nos cursos de especialização; precisa haver a parceria entre o coordenador pedagógico e o diretor pedagógico, para juntos decidirem os caminhos a serem seguidos dentro da escola; precisa haver um olhar mais direcionado para a formação da equipe, com reuniões, encontros, leituras e atividades planejadas, intencionais; há necessidade de devolutivas aos professores com mais frequência, estar mais perto, mais atuante; o coordenador pedagógico precisa repensar o trabalho coletivo, dar a seus professores autonomia para atuarem, dentro do que for possível. Mesmo os coordenadores pedagógicos que não têm autonomia dentro da escola podem fazer algo para deixar o trabalho com a marca do seu direcionamento; somente com um trabalho de parceria será possível resolver os conflitos e as tensões existentes e fortalecer a liderança, a confiança de seus pares, o trabalho em equipe. Dessa forma, as limitações do trabalho pedagógico com certeza diminuirão.

A INFLUÊNCIA DAS PRÁTICAS PEDAGÓGICAS DOCENTES E DAS BARREIRAS DISCENTES SOBRE O DESENVOLVIMENTO DA CRIATIVIDADE DO FUTURO ADMINISTRADOR

As empresas que almejam garantir e melhorar sua posição dentro de em um mercado cada vez mais competitivo precisam estar sempre atualizadas e em constante evolução. Na busca contínua por essa evolução, investem em projetos de Pesquisa & Desenvolvimento (P&D) e em seu capital humano para promover a criatividade e a inovação organizacional. As pessoas têm papel fundamental no desenvolvimento da inovação, mas para que isso possa florescer de forma constante é preciso comprometimento e criatividade para a geração de ideias. Criatividade é pensar o novo; inovação é fazer acontecer. Porém, encontrar pessoas com essas qualidades nem sempre é tarefa fácil e muitas vezes é preciso estimular essas habilidades e características para que se tornem efetivamente criativas. Os cursos de graduação podem ser uma importante ferramenta para trabalhar esses aspectos, características e habilidades, usando métodos e práticas de ensino que auxiliem no desenvolvimento da criatividade, pois o ambiente ensino-aprendizagem pesa significativamente na formação das pessoas. O objetivo deste estudo é de identificar quais fatores têm maior influência sobre o desenvolvimento da criatividade em um curso de graduação em administração, analisando a influência das práticas pedagógicas dos docentes e as barreiras internas dos discentes. O referencial teórico se baseia principalmente nos trabalhos de Alencar, Fleith, Torrance e Wechsler. A pesquisa transversal de abordagem quantitativa teve como público-alvo os alunos do curso de Administração de uma universidade confessional da Grande São Paulo, que responderam 465 questionários compostos de três escalas. Para as práticas docentes foi adaptada a escala de Práticas Docentes em relação à Criatividade. Para as barreiras internas foi adaptada a escala de Barreiras da Criatividade Pessoal. Para a análise da percepção do desenvolvimento da criatividade foi construída e validada uma escala baseada no referencial de características de uma pessoa criativa. As análises estatísticas descritivas e fatoriais exploratórias foram realizadas no software Statistical Package for the Social Sciences (SPSS), enquanto as análises fatoriais confirmatórias e a mensuração da influência das práticas pedagógicas e das barreiras internas sobre a percepção do desenvolvimento da criatividade foram realizadas por modelagem de equação estrutural utilizando o algoritmo Partial Least Squares (PLS), no software Smart PLS 2.0. Os resultados apontaram que as práticas pedagógicas e as barreiras internas dos discentes explicam 40% da percepção de desenvolvimento da criatividade, sendo as práticas pedagógicas que exercem maior influencia. A pesquisa também apontou que o tipo de temática e o período em que o aluno está cursando não têm influência sobre nenhum dos três construtos, somente o professor influencia as práticas pedagógicas.

ANALISANDO A RELAÇÃO DOS VOLUMES DE EXPORTAÇÃO E DE IMPORTAÇÃO, PIB, TAXAS DE CÂMBIO E INFLAÇÃO NO PERÍODO DE 2004 A 2014. SÃO BERNARDO DO CAMPO 2015

As empresas que almejam garantir e melhorar sua posição dentro de em um mercado cada vez mais competitivo precisam estar sempre atualizadas e em constante evolução. Na busca contínua por essa evolução, investem em projetos de Pesquisa & Desenvolvimento (P&D) e em seu capital humano para promover a criatividade e a inovação organizacional. As pessoas têm papel fundamental no desenvolvimento da inovação, mas para que isso possa florescer de forma constante é preciso comprometimento e criatividade para a geração de ideias. Criatividade é pensar o novo; inovação é fazer acontecer. Porém, encontrar pessoas com essas qualidades nem sempre é tarefa fácil e muitas vezes é preciso estimular essas habilidades e características para que se tornem efetivamente criativas. Os cursos de graduação podem ser uma importante ferramenta para trabalhar esses aspectos, características e habilidades, usando métodos e práticas de ensino que auxiliem no desenvolvimento da criatividade, pois o ambiente ensino-aprendizagem pesa significativamente na formação das pessoas. O objetivo deste estudo é de identificar quais fatores têm maior influência sobre o desenvolvimento da criatividade em um curso de graduação em administração, analisando a influência das práticas pedagógicas dos docentes e as barreiras internas dos discentes. O referencial teórico se baseia principalmente nos trabalhos de Alencar, Fleith, Torrance e Wechsler. A pesquisa transversal de abordagem quantitativa teve como público-alvo os alunos do curso de Administração de uma universidade confessional da Grande São Paulo, que responderam 465 questionários compostos de três escalas. Para as práticas docentes foi adaptada a escala de Práticas Docentes em relação à Criatividade. Para as barreiras internas foi adaptada a escala de Barreiras da Criatividade Pessoal. Para a análise da percepção do desenvolvimento da criatividade foi construída e validada uma escala baseada no referencial de características de uma pessoa criativa. As análises estatísticas descritivas e fatoriais exploratórias foram realizadas no software Statistical Package for the Social Sciences (SPSS), enquanto as análises fatoriais confirmatórias e a mensuração da influência das práticas pedagógicas e das barreiras internas sobre a percepção do desenvolvimento da criatividade foram realizadas por modelagem de equação estrutural utilizando o algoritmo Partial Least Squares (PLS), no software Smart PLS 2.0. Os resultados apontaram que as práticas pedagógicas e as barreiras internas dos discentes explicam 40% da percepção de desenvolvimento da criatividade, sendo as práticas pedagógicas que exercem maior influencia. A pesquisa também apontou que o tipo de temática e o período em que o aluno está cursando não têm influência sobre nenhum dos três construtos, somente o professor influencia as práticas pedagógicas.

The nature of cognitive style and its relationship to educational performance

A survey is made of the literature relating to a number of dimensions of cognitive style, from which it is concluded that cognitive style has a strong theoretical potential as a predictor of academic performance. It is also noted that there have been few attempts to relate co gnitive style to academic performance, and that these have met with limited success. On the assumption that theories of individual differences should be congruent with theories of general functioning, an examination is made of the model of cognition presupposed by ,dimen sions of cognitive style. A central feature of this model is the distinction between cognitive content and cognitive structure. The origins of this distinction are traced back to the normative and experimental or quasi-experimental characteristics of research in psychology. The validity of the distinction is examined with reference to modern research findings, and the conclusion is drawn that the norma~ive experimental method is an increasingly inappropriate tool of research when applied to higher levels of cognitive functioning, as it cannot handle subject idiosyncracy or patterns of interaction. An examination of the presuppositions of educational research leads to the complementary conclusion that the research methods imply an oversimplified model of the educational situation. Two empirical studies are reported: (1) An experiment using conventional cognitive style dimensions as predictors of performance under two teaching methods (2) An attempt to predict individual differences in overall academic performance by means of a research technique which uses a questionnaire, intra-individual scoring, and an analysis of patterns of responses, and which attempts to take some account of subject idiosyncracy. The implifications of these studies for fUrther research are noted.