Polynomial function intervals for floating-point software verification

The focus of our work is the verification of tight functional properties of numerical programs, such as showing that a floating-point implementation of Riemann integration computes a close approximation of the exact integral. Programmers and engineers writing such programs will benefit from verification tools that support an expressive specification language and that are highly automated. Our work provides a new method for verification of numerical software, supporting a substantially more expressive language for specifications than other publicly available automated tools. The additional expressivity in the specification language is provided by two constructs. First, the specification can feature inclusions between interval arithmetic expressions. Second, the integral operator from classical analysis can be used in the specifications, where the integration bounds can be arbitrary expressions over real variables. To support our claim of expressivity, we outline the verification of four example programs, including the integration example mentioned earlier. A key component of our method is an algorithm for proving numerical theorems. This algorithm is based on automatic polynomial approximation of non-linear real and real-interval functions defined by expressions. The PolyPaver tool is our implementation of the algorithm and its source code is publicly available. In this paper we report on experiments using PolyPaver that indicate that the additional expressivity does not come at a performance cost when comparing with other publicly available state-of-the-art provers. We also include a scalability study that explores the limits of PolyPaver in proving tight functional specifications of progressively larger randomly generated programs. © 2014 Springer International Publishing Switzerland.

Integration Principles of Russian and Japanese Databases on Inorganic Materials

The methods and software for integration of databases (DBs) on inorganic material and substance properties have been developed. The information systems integration is based on known approaches combination: EII (Enterprise Information Integration) and EAI (Enterprise Application Integration). The metabase - special database that stores data on integrated DBs contents is an integrated system kernel. Proposed methods have been applied for DBs integrated system creation in the field of inorganic chemistry and materials science. Important developed integrated system feature is ability to include DBs that have been created by means of different DBMS using essentially various computer platforms: Sun (DB "Diagram") and Intel (other DBs) and diverse operating systems: Sun Solaris (DB "Diagram") and Microsoft Windows Server (other DBs).

Software Development for Distributed System of Russian Databases for Electronics Materials

Current state of Russian databases for substances and materials properties was considered. A brief review of integration methods of given information systems was prepared and a distributed databases integration approach based on metabase was proposed. Implementation details were mentioned on the posed database on electronics materials integration approach. An operating pilot version of given integrated information system implemented at IMET RAS was considered.

Facilitating intuitive-guided learning in a serious game through integration with a learning content management system

Increased global uptake of entertainment gaming has the potential to lead to high expectations of engagement and interactivity from users of technology-enhanced learning environments. Blended approaches to implementing game-based learning as part of distance or technology-enhanced education have led to demonstrations of the benefits they might bring, allowing learners to interact with immersive technologies as part of a broader, structured learning experience. In this article, we explore how the integration of a serious game can be extended to a learning content management system (LCMS) to support a blended and holistic approach, described as an 'intuitive-guided' method. Through a case study within the EU-Funded Adaptive Learning via Intuitive/Interactive, Collaborative and Emotional Systems (ALICE) project, a technical integration of a gaming engine with a proprietary LCMS is demonstrated, building upon earlier work and demonstrating how this approach might be realized. In particular, how this method can support an intuitive-guided approach to learning is considered, whereby the learner is given the potential to explore a non-linear environment whilst scaffolding and blending provide guidance ensuring targeted learning objectives are met. Through an evaluation of the developed prototype with 32 students aged 14-16 across two Italian schools, a varied response from learners is observed, coupled with a positive reception from tutors. The study demonstrates that challenges remain in providing high-fidelity content in a classroom environment, particularly as an increasing gap in technology availability between leisure and school times emerges.

Implementing an agent-based model with a spatial visual display in discrete-event simulation software

There has been an increasing interest in the use of agent-based simulation and some discussion of the relative merits of this approach as compared to discrete-event simulation. There are differing views on whether an agent-based simulation offers capabilities that discrete-event cannot provide or whether all agent-based applications can at least in theory be undertaken using a discrete-event approach. This paper presents a simple agent-based NetLogo model and corresponding discrete-event versions implemented in the widely used ARENA software. The two versions of the discrete-event model presented use a traditional process flow approach normally adopted in discrete-event simulation software and also an agent-based approach to the model build. In addition a real-time spatial visual display facility is provided using a spreadsheet platform controlled by VBA code embedded within the ARENA model. Initial findings from this investigation are that discrete-event simulation can indeed be used to implement agent-based models and with suitable integration elements such as VBA provide the spatial displays associated with agent-based software.

Segmental body composition determination through a bioelectrical very large scale integration (VLSI) system

The purpose of this investigation was to develop new techniques to generate segmental assessments of body composition based on Segmental Bioelectrical Impedance Analysis (SBIA). An equally important consideration was the design, simulation, development, and the software and hardware integration of the SBIA system. This integration was carried out with a Very Large Scale Integration (VLSI) Field Programmable Gate Array (FPGA) microcontroller that analyzed the measurements obtained from segments of the body, and provided full body and segmental Fat Free Mass (FFM) and Fat Mass (FM) percentages. Also, the issues related to the estimate of the body's composition in persons with spinal cord injury (SCI) were addressed and investigated. This investigation demonstrated that the SBIA methodology provided accurate segmental body composition measurements. Disabled individuals are expected to benefit from these SBIA evaluations, as they are non-invasive methods, suitable for paralyzed individuals. The SBIA VLSI system may replace bulky, non flexible electronic modules attached to human bodies. ^

Uma abordagem para evolução e reconciliação de linhas de produtos de software clonadas

Software product line engineering promotes large software reuse by developing a system family that shares a set of developed core features, and enables the selection and customization of a set of variabilities that distinguish each software product family from the others. In order to address the time-to-market, the software industry has been using the clone-and-own technique to create and manage new software products or product lines. Despite its advantages, the clone-and-own approach brings several difficulties for the evolution and reconciliation of the software product lines, especially because of the code conflicts generated by the simultaneous evolution of the original software product line, called Source, and its cloned products, called Target. This thesis proposes an approach to evolve and reconcile cloned products based on mining software repositories and code conflict analysis techniques. The approach provides support to the identification of different kinds of code conflicts – lexical, structural and semantics – that can occur during development task integration – bug correction, enhancements and new use cases – from the original evolved software product line to the cloned product line. We have also conducted an empirical study of characterization of the code conflicts produced during the evolution and merging of two large-scale web information system product lines. The results of our study demonstrate the approach potential to automatically or semi-automatically solve several existing code conflicts thus contributing to reduce the complexity and costs of the reconciliation of cloned software product lines.

Agent-K: An Integration of AOP & KQML

Postprint

D6.1 – Ecosystem Software Platform with Underlying Software Repository, Digital Library and Media Archive

The objective of D6.1 is to make the Ecosystem software platform with underlying Software Repository, Digital Library and Media Archive available to the degree, that the RAGE project can start collecting content in the form of software assets, and documents of various media types. This paper describes the current state of the Ecosystem as of month 12 of the project, and documents the structure of the Ecosystem, individual components, integration strategies, and overall approach. The deliverable itself is the deployment of the described components, which is now available to collect and curate content. Whilst this version is not yet feature complete, full realization is expected within the next few months. Following this development, WP6 will continue to add features driven by the business models to be defined by WP7 later on in the project.

The RAGE Software Asset Model and Metadata Model

Software assets are key output of the RAGE project and they can be used by applied game developers to enhance the pedagogical and educational value of their games. These software assets cover a broad spectrum of functionalities – from player analytics including emotion detection to intelligent adaptation and social gamification. In order to facilitate integration and interoperability, all of these assets adhere to a common model, which describes their properties through a set of metadata. In this paper the RAGE asset model and asset metadata model is presented, capturing the detail of assets and their potential usage within three distinct dimensions – technological, gaming and pedagogical. The paper highlights key issues and challenges in constructing the RAGE asset and asset metadata model and details the process and design of a flexible metadata editor that facilitates both adaptation and improvement of the asset metadata model.

Probabilistic Graphical Modelling for Software Product Lines: A Frameweork for Modeling and Reasoning under Uncertainty

This work provides a holistic investigation into the realm of feature modeling within software product lines. The work presented identifies limitations and challenges within the current feature modeling approaches. Those limitations include, but not limited to, the dearth of satisfactory cognitive presentation, inconveniency in scalable systems, inflexibility in adapting changes, nonexistence of predictability of models behavior, as well as the lack of probabilistic quantification of model’s implications and decision support for reasoning under uncertainty. The work in this thesis addresses these challenges by proposing a series of solutions. The first solution is the construction of a Bayesian Belief Feature Model, which is a novel modeling approach capable of quantifying the uncertainty measures in model parameters by a means of incorporating probabilistic modeling with a conventional modeling approach. The Bayesian Belief feature model presents a new enhanced feature modeling approach in terms of truth quantification and visual expressiveness. The second solution takes into consideration the unclear support for the reasoning under the uncertainty process, and the challenging constraint satisfaction problem in software product lines. This has been done through the development of a mathematical reasoner, which was designed to satisfy the model constraints by considering probability weight for all involved parameters and quantify the actual implications of the problem constraints. The developed Uncertain Constraint Satisfaction Problem approach has been tested and validated through a set of designated experiments. Profoundly stating, the main contributions of this thesis include the following: • Develop a framework for probabilistic graphical modeling to build the purported Bayesian belief feature model. • Extend the model to enhance visual expressiveness throughout the integration of colour degree variation; in which the colour varies with respect to the predefined probabilistic weights. • Enhance the constraints satisfaction problem by the uncertainty measuring of the parameters truth assumption. • Validate the developed approach against different experimental settings to determine its functionality and performance.

Medisuite + Iplate Integration EAFIT & Ilimitada S.A.

Force plate or pressure plate analysis came as an innovative tool to biomechanics and sport medicine -- This allows engineers, scientists and doctors to virtually reconstruct the way a person steps while running or walking using a measuring system and a computer -- With this information they can calculate and analyze a whole set of variables and factors that characterize the step -- Then they are able to make corrections and/or optimizations, designing appropriate shoes and insoles for the patient -- The idea is to study and understand all the hardware and software implications of this process and all the components involved, and then propose an alternative solution -- This solution should have at least similar performance to existing systems -- It should increase the accuracy and/or the sampling frequency to obtain better results -- By the end, there should be a working prototype of a pressure measuring system and a mathematical model to govern it -- The costs of the system have to be lower than most of the systems in the market

Ferramentas Web, Web 2.0 e software livre em EVT: estudo sobre a integração de ferramentas digitais no currículo da disciplina de educação visual e tecnológica

A utilização das TIC ocupam um lugar cada vez mais importante nas nossas escolas, marcado sobretudo pela evolução das tecnologias e pela utilização em contexto educativo de muitas ferramentas da Web 2.0. Esse facto é muito notório na disciplina de Educação Visual e Tecnológica, de carácter eminentemente prático, onde é permitido explorar várias ferramentas digitais para abordagem de conteúdos da disciplina e para a criação de produtos gráficos e plásticos. Com o aparecimento da Web 2.0 e a disponibilização de milhares de novas ferramentas digitais aos utilizadores da Internet, estimula-se um interesse cada vez maior na adoção de metodologias e estratégias com recurso a estes media e que suportem uma aprendizagem mais eficaz e motivadora para os alunos, articulando-se os suportes tradicionais de EVT com os novos media digitais. Neste contexto, o presente estudo é o resultado duma investigação-ação realizada no âmbito do Programa Doutoral em Multimédia em Educação da Universidade de Aveiro onde se implementou a integração de ferramentas da Web, Web 2.0 e Software Livre em contexto educativo na disciplina de EVT, na qual poderiam ser utilizadas tanto as técnicas tradicionais de realização mais usuais na disciplina como a integração e articulação com as ferramentas digitais, suportadas por software livre (e outros de utilização gratuita), a Web e a Web 2.0 para suporte ao ensino e aprendizagem dos diversos conteúdos e áreas de exploração da disciplina. Este estudo, desenhado em três ciclos, envolveu num primeiro momento a constituição de uma comunidade de prática de professores alargada, sendo criadas seis turmas de formação que reuniram um total de 112 professores que pretendiam integrar as ferramentas digitais em EVT. Para além da pesquisa, análise, seleção e catalogação destas 430 ferramentas digitais recenseadas, produziram-se 371 manuais de apoio à utilização das mesmas, sendo estes recursos disponibilizados no espaço do EVTdigital. Num segundo ciclo, decorrente da avaliação realizada, foi criada a distribuição EVTux para simplificar o acesso e utilização das ferramentas digitais em contexto de EVT. Finalmente, o terceiro ciclo, decorre da eliminação da disciplina de EVT do currículo do 2º ciclo do ensino básico e a sua substituição por duas novas disciplinas, tendo-se realizada a respetiva análise de conteúdo das metas curriculares e produzido a aplicação As ferramentas digitais do Mundo Visual, concebida para contextualizar e indexar as ferramentas digitais selecionadas para a nova disciplina de Educação Visual.Os resultados deste estudo apontam claramente para a possibilidade de integrar na disciplina de Educação Visual e Tecnológica (ou no presente momento, em Educação Visual) ferramentas digitais para abordagem aos conteúdos e áreas de exploração, bem como a possibilidade de se constituírem facilmente comunidades de prática (como foi o caso) que possam colaborar na catalogação destas ferramentas no contexto específico da disciplina e para a necessidade sentida pelos professores em obter informação e formação que os possa atualizar quanto à integração das TIC no currículo. Apresentam-se, ainda, as limitações deste estudo que passaram sobretudo pelo impacto negativo que a eliminação da disciplina provocou na motivação dos docentes e a sua consequente participação no decorrer de algumas fases do trabalho, e ainda da dificuldade de gestão de uma equipa de professores colaboradores tão numerosa e diversificada. Nesse sentido, são também apresentadas sugestões para estudos futuros.

A Binary Classifier for Test Case Feasibility Applied to Automatically Generated Tests of Event-Driven Software

Modern software application testing, such as the testing of software driven by graphical user interfaces (GUIs) or leveraging event-driven architectures in general, requires paying careful attention to context. Model-based testing (MBT) approaches first acquire a model of an application, then use the model to construct test cases covering relevant contexts. A major shortcoming of state-of-the-art automated model-based testing is that many test cases proposed by the model are not actually executable. These \textit{infeasible} test cases threaten the integrity of the entire model-based suite, and any coverage of contexts the suite aims to provide. In this research, I develop and evaluate a novel approach for classifying the feasibility of test cases. I identify a set of pertinent features for the classifier, and develop novel methods for extracting these features from the outputs of MBT tools. I use a supervised logistic regression approach to obtain a model of test case feasibility from a randomly selected training suite of test cases. I evaluate this approach with a set of experiments. The outcomes of this investigation are as follows: I confirm that infeasibility is prevalent in MBT, even for test suites designed to cover a relatively small number of unique contexts. I confirm that the frequency of infeasibility varies widely across applications. I develop and train a binary classifier for feasibility with average overall error, false positive, and false negative rates under 5\%. I find that unique event IDs are key features of the feasibility classifier, while model-specific event types are not. I construct three types of features from the event IDs associated with test cases, and evaluate the relative effectiveness of each within the classifier. To support this study, I also develop a number of tools and infrastructure components for scalable execution of automated jobs, which use state-of-the-art container and continuous integration technologies to enable parallel test execution and the persistence of all experimental artifacts.

Inductive Theorem Proving and Computer Algebra in the Mathweb Software Bus

Reasoning systems have reached a high degree of maturity in the last decade. However, even the most successful systems are usually not general purpose problem solvers but are typically specialised on problems in a certain domain. The MathWeb SOftware Bus (Mathweb-SB) is a system for combining reasoning specialists via a common osftware bus. We described the integration of the lambda-clam systems, a reasoning specialist for proofs by induction, into the MathWeb-SB. Due to this integration, lambda-clam now offers its theorem proving expertise to other systems in the MathWeb-SB. On the other hand, lambda-clam can use the services of any reasoning specialist already integrated. We focus on the latter and describe first experimnents on proving theorems by induction using the computational power of the MAPLE system within lambda-clam.