The European Declarative System, Database, and Languages

The EP2025 EDS project develops a highly parallel information server that supports established high-value interfaces. We describe the motivation for the project, the architecture of the system, and the design and application of its database and language subsystems. The Elipsys logic programming language, its advanced applications, EDS Lisp, and the Metal machine translation system are examined.

Example uses of a learning object

A self study course for learning to program using the C programming language has been developed. A Learning Object approach was used in the design of the course. One of the benefits of the Learning Object approach is that the learning material can be reused for different purposes. 'Me course developed is designed so that learners can choose the pedagogical approach most suited to their personal learning requirements. For all learning approaches a set of common Assessment Learning Objects (ALOs or tests) have been created. The design of formative assessments with ALOs can be carried out by the Instructional Designer grouping ALOs to correspond to a specific assessment intention. The course is non-credit earning, so there is no summative assessment, all assessment is formative. In this paper examples of ALOs and their uses is presented together with their uses as decided by the Instructional Designer and learner. Personalisation of the formative assessment of skills can be decided by the Instructional Designer or the learner using a repository of pre-designed ALOs. The process of combining ALOs can be carried out manually or in a semi-automated way using metadata that describes the ALO and the skill it is designed to assess.

Dynamic integrated system optimization and parameter estimation for discrete time optimal control of nonlinear systems

An algorithm for solving nonlinear discrete time optimal control problems with model-reality differences is presented. The technique uses Dynamic Integrated System Optimization and Parameter Estimation (DISOPE), which achieves the correct optimal solution in spite of deficiencies in the mathematical model employed in the optimization procedure. A version of the algorithm with a linear-quadratic model-based problem, implemented in the C+ + programming language, is developed and applied to illustrative simulation examples. An analysis of the optimality and convergence properties of the algorithm is also presented.

Predictive computed-torque control of a PUMA 560 manipulator robot

This paper describes the integration of constrained predictive control and computed-torque control, and its application on a six degree-of-freedom PUMA 560 manipulator arm. The real-time implementation was based on SIMULINK, with the predictive controller and the computed-torque control law implemented in the C programming language. The constrained predictive controller solved a quadratic programming problem at every sampling interval, which was as short as 10 ms, using a prediction horizon of 150 steps and an 18th order state space model.

Depth to mate and the 50-move rule

The most popular endgame tables (EGTs) documenting ‘DTM’ Depth to Mate in chess endgames are those of Eugene Nalimov but these do not recognise the FIDE 50-move rule ‘50mr’. This paper marks the creation by the first author of EGTs for sub-6-man (s6m) chess and beyond which give DTM as affected by the ply count pc. The results are put into the context of previous work recognising the 50mr and are compared with the original unmoderated DTM results. The work is also notable for being the first EGT generation work to use the functional programming language HASKELL.

Extraction of structured programs from specification proofs

We present a method using an extended logical system for obtaining programs from specifications written in a sublanguage of CASL. These programs are “correct” in the sense that they satisfy their specifications. The technique we use is to extract programs from proofs in formal logic by techniques due to Curry and Howard. The logical calculus, however, is novel because it adds structural rules corresponding to the standard ways of modifying specifications: translating (renaming), taking unions, and hiding signatures. Although programs extracted by the Curry-Howard process can be very cumbersome, we use a number of simplifications that ensure that the programs extracted are in a language close to a standard high-level programming language. We use this to produce an executable refinement of a given specification and we then provide a method for producing a program module that maximally respects the original structure of the specification. Throughout the paper we demonstrate the technique with a simple example.

Quantified Interference: Information Theory and Information Flow

The paper investigates which of Shannon’s measures (entropy, conditional entropy, mutual information) is the right one for the task of quantifying information flow in a programming language. We examine earlier relevant contributions from Denning, McLean and Gray and we propose and motivate a specific quantitative definition of information flow. We prove results relating equivalence relations, interference of program variables, independence of random variables and the flow of confidential information. Finally, we show how, in our setting, Shannon’s Perfect Secrecy theorem provides a sufficient condition to determine whether a program leaks confidential information.

A JML-Based strategy for incorporating formal specifications into the software development process

This thesis presents a JML-based strategy that incorporates formal specifications into the software development process of object-oriented programs. The strategy evolves functional requirements into a “semi-formal” requirements form, and then expressing them as JML formal specifications. The strategy is implemented as a formal-specification pseudo-phase that runs in parallel with the other phase of software development. What makes our strategy different from other software development strategies used in literature is the particular use of JML specifications we make all along the way from requirements to validation-and-verification.

Análise gráfica de estruturas porosas sobre a ótica da estereologia

In this work we developed a computer simulation program for physics porous structures based on programming language C + + using a Geforce 9600 GT with the PhysX chip, originally developed for video games. With this tool, the ability of physical interaction between simulated objects is enlarged, allowing to simulate a porous structure, for example, reservoir rocks and structures with high density. The initial procedure for developing the simulation is the construction of porous cubic structure consisting of spheres with a single size and with varying sizes. In addition, structures can also be simulated with various volume fractions. The results presented are divided into two parts: first, the ball shall be deemed as solid grains, ie the matrix phase represents the porosity, the second, the spheres are considered as pores. In this case the matrix phase represents the solid phase. The simulations in both cases are the same, but the simulated structures are intrinsically different. To validate the results presented by the program, simulations were performed by varying the amount of grain, the grain size distribution and void fraction in the structure. All results showed statistically reliable and consistent with those presented in the literature. The mean values and distributions of stereological parameters measured, such as intercept linear section of perimeter area, sectional area and mean free path are in agreement with the results obtained in the literature for the structures simulated. The results may help the understanding of real structures.

Um algoritmo híbrido para o problema de roteamento de veículos com frotas heterogêneas

This paper aims to propose a hybrid meta-heuristics for the Heterogeneous Fleet Vehicle Routing Problem (HVRP), which is a combinatorial optimization problem NP-hard, and is characterized by the use of a limited fleet consists of different vehicles with different capacities. The hybrid method developed makes use of a memetic algorithm associated with the component optimizer Vocabulary Building. The resulting hybrid meta-heuristic was implemented in the programming language C + + and computational experiments generated good results in relation to meta-heuristic applied in isolation, proving the efficiency of the proposed method.

Uma ferramenta de manipulação de pacotes para análise de protocolos de redes industriais baseados em TCP/IP

This work presents a packet manipulation tool developed to realize tests in industrial devices that implements TCP/IP-based communication protocols. The tool was developed in Python programming language, as a Scapy extension. This tool, named IndPM- Industrial Packet Manipulator, can realize vulnerability tests in devices of industrial networks, industrial protocol compliance tests, receive server replies and utilize the Python interpreter to build tests. The Modbus/TCP protocol was implemented as proof-of-concept. The DNP3 over TCP protocol was also implemented but tests could not be realized because of the lack of resources. The IndPM results with Modbus/TCP protocol show some implementation faults in a Programmable Logic Controller communication module frequently utilized in automation companies

Quantitative characterization of multi-phase materials by digital image processing

An automatic image processing and analysis technique has been developed for quantitative characterization of multi-phase materials. For the development of this technique is used the Khoros system that offers the basic morphological tools and a flexible, visual programming language. These techniques are implemented in a highly user oriented image processing environment that allows the user to adapt each step of the processing to his special requirements.To illustrate the implementation and performance of this technique, images of two different materials are processed for microstructure characterization. The result is presented through the determination of volume fraction of the different phases or precipitates.

Geração automática de hardware a partir de especificações formais: estendendo uma abordagem de tradução

Removing inconsistencies in a project is a less expensive activity when done in the early steps of design. The use of formal methods improves the understanding of systems. They have various techniques such as formal specification and verification to identify these problems in the initial stages of a project. However, the transformation from a formal specification into a programming language is a non-trivial task and error prone, specially when done manually. The aid of tools at this stage can bring great benefits to the final product to be developed. This paper proposes the extension of a tool whose focus is the automatic translation of specifications written in CSPM into Handel-C. CSP is a formal description language suitable for concurrent systems, and CSPM is the notation used in tools support. Handel-C is a programming language whose result can be compiled directly into FPGA s. Our extension increases the number of CSPM operators accepted by the tool, allowing the user to define local processes, to rename channels in a process and to use Boolean guards on external choices. In addition, we also propose the implementation of a communication protocol that eliminates some restrictions on parallel composition of processes in the translation into Handel-C, allowing communication in a same channel between multiple processes to be mapped in a consistent manner and that improper communication in a channel does not ocurr in the generated code, ie, communications that are not allowed in the system specification

EUPAT for WoW: Uma ferramenta de assistência à programação por usuário final

Neste trabalho, apresentamos uma ferramenta cujo intuito é auxiliar não-programadores, jogadores de videogame, na criação de extensões na forma de Add-ons para World of Warcraft, o jogo online. Nele, o usuário pode criar extensões customizando completamente sua interface, de forma a reinventar a sua experiência de jogo e melhorar sua jogabilidade. A criação de extensões para aplicativos e jogos surgiu da crescente necessidade de fornecer aos usuários mecanismos eficientes de Programação por Usuário Final, permitindo que os mesmos preenchessem suas necessidades singulares através da criação, customização e especificação de extensões em software. Em World of Warcraft mais especificamente, os Add-ons exploram um tipo de extensão na qual os jogadores passam a programar sua própria interface de usuário ou a fazer uso de interfaces criadas por outros usuários. No entanto, realizar a programação dessas extensões - os Add-ons - não é uma tarefa fácil. Dentro deste contexto, desenvolvemos a ferramenta EUPAT for WoW (do inglês, End-User Programming Assistance Tool for World of Warcraft) que oferece assistência à criação de Add-ons. Além disso, investigamos como usuários jogadores com e sem conhecimento de programação são beneficiados. Os resultados desta pesquisa permitiram refletir sobre as estratégias de assistência de programação por usuário final no contexto de jogos

Contribuições para verificação automática de applets javacard

The widespread growth in the use of smart cards (by banks, transport services, and cell phones, etc) has brought an important fact that must be addressed: the need of tools that can be used to verify such cards, so to guarantee the correctness of their software. As the vast majority of cards that are being developed nowadays use the JavaCard technology as they software layer, the use of the Java Modeling Language (JML) to specify their programs appear as a natural solution. JML is a formal language tailored to Java. It has been inspired by methodologies from Larch and Eiffel, and has been widely adopted as the de facto language when dealing with specification of any Java related program. Various tools that make use of JML have already been developed, covering a wide range of functionalities, such as run time and static checking. But the tools existent so far for static checking are not fully automated, and, those that are, do not offer an adequate level of soundness and completeness. Our objective is to contribute to a series of techniques, that can be used to accomplish a fully automated and confident verification of JavaCard applets. In this work we present the first steps to this. With the use of a software platform comprised by Krakatoa, Why and haRVey, we developed a set of techniques to reduce the size of the theory necessary to verify the specifications. Such techniques have yielded very good results, with gains of almost 100% in all tested cases, and has proved as a valuable technique to be used, not only in this, but in most real world problems related to automatic verification