Specification, refinement and verification of concurrent systems - An integration of Object-Z and CSP

This paper presents a method of formally specifying, refining and verifying concurrent systems which uses the object-oriented state-based specification language Object-Z together with the process algebra CSP. Object-Z provides a convenient way of modelling complex data structures needed to define the component processes of such systems, and CSP enables the concise specification of process interactions. The basis of the integration is a semantics of Object-Z classes identical to that of CSP processes. This allows classes specified in Object-Z to he used directly within the CSP part of the specification. In addition to specification, we also discuss refinement and verification in this model. The common semantic basis enables a unified method of refinement to be used, based upon CSP refinement. To enable state-based techniques to be used fur the Object-Z components of a specification we develop state-based refinement relations which are sound and complete with respect to CSP refinement. In addition, a verification method for static and dynamic properties is presented. The method allows us to verify properties of the CSP system specification in terms of its component Object-Z classes by using the laws of the the CSP operators together with the logic for Object-Z.

Model specification tests in nonparametric stochastic regression models

In this paper, we consider testing for additivity in a class of nonparametric stochastic regression models. Two test statistics are constructed and their asymptotic distributions are established. We also conduct a small sample study for one of the test statistics through a simulated example. (C) 2002 Elsevier Science (USA).

LEARNING ENVIRONMENTS IN THE CONTEXT OF A MASTER DEGREE IN ANIMATION AND ILLUSTRATION

This paper aims to describe the processes of teaching illustration and animation, together, in the context of a masters degree program. In Portugal, until very recently, illustration and animation higher education courses, were very scarce and only provided by a few private universities, which offered separated programs - either illustration or animation. The MA in Illustration and Animation (MIA) based in the Instituto Politécnico do Cávado e Ave in Portugal, dared to join these two creative areas in a common learning model and is already starting it’s third edition with encouraging results and will be supported by the first international conference on illustration and animation (CONFIA). This masters program integrates several approaches and techniques (in illustration and animation) and integrates and encourages creative writing and critique writing. This paper describes the iterative process of construction, and implementation of the program as well as the results obtained on the initial years of existence in terms of pedagogic and learning conclusions. In summary, we aim to compare pedagogic models of animation or illustration teaching in higher education opposed to a more contemporary and multidisciplinary model approach that integrates the two - on an earlier stage - and allows them to be developed separately – on the second part of the program. This is based on the differences and specificities of animation (from classic techniques to 3D) and illustration (drawing the illustration) and the intersection area of these two subjects within the program structure focused on the students learning and competencies acquired to use in professional or authorial projects.

On the specification of a component repository

The lack of a commonly accepted de nition of a software component, the proliferation of competing `standards' and component frameworks, is here to stay, raising the fundamental question in component-based development of how to cope in practice with heterogeneity. This paper reports on the design of a Component Repository aimed to give at least a partial answer to the above question. The repository was fully speci ed in Vdm and a working prototype is currently being used in an industrial environment

Real-time hand tracking for rehabilitation and character animation

Hand and finger tracking has a major importance in healthcare, for rehabilitation of hand function required due to a neurological disorder, and in virtual environment applications, like characters animation for on-line games or movies. Current solutions consist mostly of motion tracking gloves with embedded resistive bend sensors that most often suffer from signal drift, sensor saturation, sensor displacement and complex calibration procedures. More advanced solutions provide better tracking stability, but at the expense of a higher cost. The proposed solution aims to provide the required precision, stability and feasibility through the combination of eleven inertial measurements units (IMUs). Each unit captures the spatial orientation of the attached body. To fully capture the hand movement, each finger encompasses two units (at the proximal and distal phalanges), plus one unit at the back of the hand. The proposed glove was validated in two distinct steps: a) evaluation of the sensors’ accuracy and stability over time; b) evaluation of the bending trajectories during usual finger flexion tasks based on the intra-class correlation coefficient (ICC). Results revealed that the glove was sensitive mainly to magnetic field distortions and sensors tuning. The inclusion of a hard and soft iron correction algorithm and accelerometer and gyro drift and temperature compensation methods provided increased stability and precision. Finger trajectories evaluation yielded high ICC values with an overall reliability within application’s satisfying limits. The developed low cost system provides a straightforward calibration and usability, qualifying the device for hand and finger tracking in healthcare and animation industries.

Specification of software architecture reconfiguration

In the past years, Software Architecture has attracted increased attention by academia and industry as the unifying concept to structure the design of complex systems. One particular research area deals with the possibility of reconfiguring architectures to adapt the systems they describe to new requirements. Reconfiguration amounts to adding and removing components and connections, and may have to occur without stopping the execution of the system being reconfigured. This work contributes to the formal description of such a process. Taking as a premise that a single formalism hardly ever satisfies all requirements in every situation, we present three approaches, each one with its own assumptions about the systems it can be applied to and with different advantages and disadvantages. Each approach is based on work of other researchers and has the aesthetic concern of changing as little as possible the original formalism, keeping its spirit. The first approach shows how a given reconfiguration can be specified in the same manner as the system it is applied to and in a way to be efficiently executed. The second approach explores the Chemical Abstract Machine, a formalism for rewriting multisets of terms, to describe architectures, computations, and reconfigurations in a uniform way. The last approach uses a UNITY-like parallel programming design language to describe computations, represents architectures by diagrams in the sense of Category Theory, and specifies reconfigurations by graph transformation rules.

Model driven development implementation of a control systems user interfaces specification tool

Dissertação apresentada na Faculdade de Ciências e Tecnologia da Universidade Nova de Lisboa para obtenção do grau de Mestre em Engenharia Informática

A contribution to the e-framework: a specification of a programming exercise evaluation service

This work is a contribution to the e-Framework, arguably the most prominent e-learning framework today, and consists of the definition of a service for the automatic evaluation of programming exercises. This evaluation domain differs from trivial evaluations modelled by languages such as the IMS Question & Test Interoperability (QTI) specification. Complex evaluation domains justify the development of specialized evaluators that participate in several business processes. These business processes can combine other type of systems such as Programming Contest Management Systems, Learning Management Systems, Integrated Development Environments and Learning Object Repositories where programming exercises are stored as Learning Objects. This contribution describes the implementation approaches used, more precisely, behaviours & requests, use & interactions, applicable standards, interface definition and usage scenarios.

Multilingual ontology specification: a collaborative approach

19-22 June 2012 Madrid, Spain

Hox genes control the specification of global vertebral domains

Dissertação apresentada para obtenção do grau de doutor em Biologia pelo Instituto de Tecnologia Química e Biológica da Universidade Nova de Lisboa

The influence of animation on functional food intake in children

A Work Project, presented as part of the requirements for the Award of a Masters Degree in Management from the NOVA – School of Business and Economics

Specification of a partial replication protocol with TLA+

Nowadays, data available and used by companies is growing very fast creating the need to use and manage this data in the most efficient way. To this end, data is replicated overmultiple datacenters and use different replication protocols, according to their needs, like more availability or stronger consistency level. The costs associated with full data replication can be very high, and most of the times, full replication is not needed since information can be logically partitioned. Another problem, is that by using datacenters to store and process information clients become heavily dependent on them. We propose a partial replication protocol called ParTree, which replicates data to clients, and organizes clients in a hierarchy, using communication between them to propagate information. This solution addresses some of these problems, namely by supporting partial data replication and offline execution mode. Given the complexity of the protocol, the use of formal verification is crucial to ensure the protocol two correctness properties: causal consistency and preservation of data. The use of TLA+ language and tools to formally specificity and verify the proposed protocol are also described.

A domain-specific language for ETL patterns specification in Data Warehousing Systems

During the last few years many research efforts have been done to improve the design of ETL (Extract-Transform-Load) systems. ETL systems are considered very time-consuming, error-prone and complex involving several participants from different knowledge domains. ETL processes are one of the most important components of a data warehousing system that are strongly influenced by the complexity of business requirements, their changing and evolution. These aspects influence not only the structure of a data warehouse but also the structures of the data sources involved with. To minimize the negative impact of such variables, we propose the use of ETL patterns to build specific ETL packages. In this paper, we formalize this approach using BPMN (Business Process Modelling Language) for modelling more conceptual ETL workflows, mapping them to real execution primitives through the use of a domain-specific language that allows for the generation of specific instances that can be executed in an ETL commercial tool.