This paper describes a new concept of a location-based remote control. This device analysis the user location and preferences to adapt the environment according to the customer needs. It makes the operation of the remote control easier and more pleasant.

Asynchronous data communication mechanisms (ACMs) have been extensively studied as data connectors between independently timed concurrent processes. In this work an automatic method for synthesis of re-reading ACMs is introduced. This method is is oriented to the generation of hardware artifacts. The behavior of re-reading ACMs is formally defined and the correctness properties are discussed. Then it is shown how to generate the ACMs specifications and how they can be translated into a proper hardware implementation. Verilog has been used as the target language to describe the hardware being synthesized.

Safety Instrumented Systems (SIS) are designed to prevent accidents, avoid undesirable situations and guarantee continuous operation of oil and gas production systems. An interruption in the operation can be caused by faults in sensors and/or actuators. Hence, SIS are integrated to the supervisory control system in order to use the information from sensors to prevent such undesirable situations. In this scenario, it is important to be able to validate the SIS implementation against its specification in order to increase the reliability of thesystem. In this work a technique to obtain a timed automata from Function Block Diagram (FBD) implementation of a SIS is presented and applied to a case study provided by Petrobras (Brazilian oil company). This is a step towards automatic conformance testing between specification in ISA 5.2 and the implementation in FBD for a SIS to improve its dependability.

In a nutshell, UPnP aims to enable simple and robust connectivity among consumer electronics, intelligent appliances and mobile devices from many different vendors. Nowadays, it is getting an increasing popularity due to its robust way of connecting devices and the massive number of already developed applications, complementing the useful new era of pervasive computing. Although UPnP is an easy-to-use solution for discovery, which allows controlled devices to share and access users contents, it does neither provide user authentication nor authorization mechanisms, requirements that would require user's data on personal profiles. As a consequence, we propose an extension of the UPnP protocol called UPnP-UP, which allows user authentication and authorization for UPnP devices and applications. The primary goal of our proposed extension is to modify the current UPnP specification as less as possible, maintaining backwards compatibility with previous versions of the protocol. Furthermore, we present our efforts on the development of a UPnP framework for publishing and accessing multimedia contents in order to support this extension as a case of study.

Wireless Personal Area Networks (WPANs) have been widely used due to the development of new wireless technologies, mainly Bluetooth. As user mobility is the focus of WPANs some questions arise when developing applications for it, specifically handoff management. Despite Bluetooth having been used for WPAN applications it does not have facilities for handoff management. It provides inquiry and paging operations that have priority over application data in the interface. This property has an impact for real-time applications. In this work a Bluetooth handoff management is modelled and analysed using Coloured Petri Nets. All the signalling and message exchanging are done by access points and never by the mobile devices during handoff. Moreover, the protocol uses only standard Bluetooth operations.

Safety Instrumented Systems (SIS) are designed to prevent accidents, avoid undesirable situations and guarantee the continuous operation of production systems such as oil and gas facilities. In this scenario, it is important to be able to validate the SIS implementation against its specification in order to increase the reliability of the system. In this work a technique to improve the dependability of SIS is introduced. A method to obtain a timed automata from a Function Block Diagram is presented and applied to a case study provided by Petrobras (Brazilian oil company).

A battery-aware dynamic power management technique that exploits an accurate analytical battery model in a non-stationary environment is proposed. The system is modelled by discrete-time Markov chains coupled to the battery model. Such model allows a rigorous mathematical formulation of the problem and a trade-off between performance and battery lifetime. The proposed technique has been implemented using the Texas Instruments OMAP 1611 platform running Linux. Experimental results have shown that the technique introduced here results in longer battery lifetime compared to previous techniques.

In this work, the problems and respective solutions for dealing with two of the most basic questions regarding handoff management are presented: to avoid total loss of connectivity; and to reduce overall time of the handoff procedure. The focus of this research is on handoff in WPANs for real-time applications. Therefore, Bluetooth stands out as the ideal technology for case study due to its particular alignment with the behavior and requirements of the WPAN’s network model. Bluetooth’s inquiry and paging operations may be calibrated for achieving fast discoveries and connections while scatternets may be used to avoid total loss of connectivity. However, the usage of scatternets and calibration of inquiry and paging unveil a series of challenging aspects when applied along with real-time applications. Such challenges are the priority of inquiry and paging data traffic over users’ applications and unpredictability of scatternet behavior. The key point to overwhelm these difficulties is to understand how they affect the real-time data transfers. In this article a set of discussions and experiments that demonstrate how inquiries, pagings and scatternets can aid achieving the goals of fast and uninterrupted handoffs, as well as the tenuous traps and tradeoffs behind such operations and configurations over real-time applications performance are presented.

Asynchronous data communication mechanisms (ACMs) have been extensively studied as data connectors between independently timed concurrent processes. In previous work, two automatic ACM synthesis methods have been proposed. However, problems remain unresolved with the most asynchronous type of ACMs, the overwriting and re-reading bounded buffer (OWRRBB), especially with buffer sizes greater than one. In this work, a method of systematic modeling and verification of multi-cell OWRRBBs is presented. This method supports the study of these kinds of ACMs with regard to vital data and temporal characteristics.

Safety Instrumented Systems (SIS) are usually designed to prevent accidents, avoid undesirable situations and guarantee continuous operation of oil and gas production systems. An interruption in the operation can be caused by faults in sensors and/or actuators. Hence, SIS are usually integrated to the supervisory control system in order to use the information from sensors to prevent such undesirable situations. In this scenario, it is important to be able to validate the SIS implementation against its specification in order to increase the reliability of the system. In this work a technique to improve the dependability of SIS is introduced. A method to obtain a timed automata from a ISA 5.2 specification is presented and applied to a case study provided by Petrobras (Brazilian oil company). Finally, an approach to perform automatic testing of the implementation using the generated model is discussed. The method introduced here is based on the use of the Uppaal model checker and the Uppaal-TRON testing tool.

Asynchronous data communication mechanisms (ACMs) have been extensively studied as data connectors between independently timed concurrent processes. In previous work, an automatic ACM synthesis method based on the generation of the reachabi lity graph and the theory of regions was proposed. In this paper, we propose a n ew synthesis method based on the composition of Petri net modules, avoiding the exploration of the reachability graph. The behavior of ACMs is formally defined and correctness properties are specified in CTL. Model checking is used to verif y the correctness of the Petri net models. The algorithms to generate the Petri net models are presented. Finally, a method to automatically generate C++ source code from the Petri net model is described.

Asynchronous data communication mechanisms (ACMs) have been extensively studied as data connectors between independently timed processes in digital systems. In previous work, systematic ACM synthesis methods have been proposed. In this paper, we advance this work by developing algorithms and software tools which automate the major part of the ACM synthesis process. Firstly, an interleaving specification is constructed in the form of a state graph, and secondly, a Petri net model of an “ACM-type” is derived using the notion of an ACM-region. The method is applied to a number of “standard” writing and reading policies of ACMs with shared memory and unidirectional control variables.

In this work we introduce an automatic adaptation approach for Coloured Petri Nets models. For this approach we define a procedure for the synthesis of a new model based on a given model and a set of behavior restrictions. This procedure was defined based on the concepts and techniques of the supervisory control theory and model checking. Moreover, we tackle the adaptation problem in the context of models reuse.

Neste trabalho apresenta-se uma metodologia para realizar a síntese automática de especificacões em redes de Petri que satisfacam a um conjunto de restricões de comportamento. Esta metodologia baseia-se dos conceitos da teoria do controle supervisório e da verificacão automática de modelos para sintetizar um controlador que satisfaca às restricões de comportamento.

This paper addresses the design and visualization of animated models for coordinated and decentralized discrete event control systems, e.g. manufacturing systems and traffic control systems. We introduce an approach to the design and animation of such controllers based on Coloured Petri nets models and the Design/CPN tool. The approach is illustrated by a simple traffic control network modeling.