Analyzing partially-implemented real-time systems

Most analysis methods for real-time systems assume that all the components of the system are at roughly the same stage of development and can be expressed in a single notation, such as a specification or programming language. There are, however, many situations in which developers would benefit from tools that could analyze partially-implemented systems: those for which some components are given only as high-level specifications while others are fully implemented in a programming language. In this paper, we propose a method for analyzing such partially-implemented real-time systems. We consider real-time concurrent systems for which some components are implemented in Ada and some are partially specified using regular expressions and graphical interval logic (GIL), a real-time temporal logic. We show how to construct models of the partially-implemented systems that account for such properties as run-time overhead and scheduling of processes, yet support tractable analysis of nontrivial programs. The approach can be fully automated, and we illustrate it by analyzing a small example     

On spiking neural P systems

This work deals with several aspects concerning the formal verification of SN P systems and the computing power of some variants. A methodology based on the information given by the transition diagram associated with an SN P system is presented. The analysis of the diagram cycles codifies invariants formulae which enable us to establish the soundness and completeness of the system with respect to the problem it tries to resolve. We also study the universality of asynchronous and sequential SN P systems and the capability these models have to generate certain classes of languages. Further, by making a slight modification to the standard SN P systems, we introduce a new variant of SN P systems with a special I/O mode, called SN P modules, and study their computing power. It is demonstrated that, as string language acceptors and transducers, SN P modules can simulate several types of computing devices such as finite automata, a-finite transducers, and systolic trellis automata.     

On the power and size of extended gemmating P systems

In [3] P systems with gemmation of mobile membranes were examined. It was shown that (extended) systems with eight membranes are as powerful as the Turing machines. Moreover, it was proved that extended gemmating P systems with only pre-dynamical rules are still computationally complete: in this case nine membranes are needed to obtain this computational power. In this paper we improve the above results concerning the size bound of extended gemmating P systems, namely we prove that these systems with at most five membranes (with meta-priority relations and without communication rules) form a class of universal computing devices, while in the case of extended systems with only pre-dynamical rules six membranes are enough to determine any recursively enumerable language.     

Notes on spiking neural P systems and finite automata

Spiking neural P systems (in short, SN P systems) are membrane computing models inspired by the pulse coding of information in biological neurons. SN P systems with standard rules have neurons that emit at most one spike (the pulse) each step, and have either an input or output neuron connected to the environment. A variant known as SN P modules generalize SN P systems by using extended rules (more than one spike can be emitted each step) and a set of input and output neurons. In this work we continue relating SN P modules and finite automata. In particular, we amend and improve previous constructions for the simulatons of deterministic finite automata and state transducers. Our improvements reduce the number of neurons from three down to one, so our results are optimal. We also simulate finite automata with output, and we use these simulations to generate automatic sequences.     

Reversible spiking neural P systems

Spiking neural (SN) P systems are a class of distributed parallel computing devices inspired by the way neurons communicate by means of spikes. In this work, we investigate reversibility in SN P systems, as well as the computing power of reversible SN P systems. Reversible SN P systems are proved to have Turing creativity, that is, they can compute any recursively enumerable set of non-negative integers by simulating universal reversible register machine.     

Using enzymatic numerical P systems for modeling mobile robot controllers

P systems (PSs) are powerful computing models based on the structure of a biological cell and on the way chemicals interact in complex biochemical reactions which take place in various compartments (or membranes) of the cell. A lot of interest has been focused on developing various forms of PSs, from cell-like to tissue-like structures. Most of the research effort has been concentrated on symbolical PSs. Numerical P systems (NPSs) have been introduced in 2006 for possible applications in economics and business processes but no other structures and applications concerning this type of PSs have been provided since then. This paper proposes a new class of NPSs, in which enzyme-like variables allow the existence of more than one production function in each membrane, while keeping the deterministic nature of the system. The way this new type of deterministic NPSs works and a possible use of it for modeling mobile robot controllers are detailed.     

Modelling computational requirements of mobile robotic systems using zones and processing windows

Mobile robotic systems must sense constraints imposed by a dynamically changing environment and predictably react to those changes in real-time. Complexity arises in mobile robotic systems because the computing platform travels through the environment with which the system is interacting. These systems have spatio-temporal requirements in the sense that correct behavior is defined in terms of both space and time. The focus of this paper is mobile robotic platforms that must sense their environment and avoid obstacles as they navigate from one point to another. We present a design and analysis methodology for these platforms that integrates spatio-temporal attributes with fixed priority real-time scheduling through the use of zone and processing window abstractions.     

Measurement study on P2P streaming systems

Originally used as the default infrastructure for efficient file sharing, peer-to-peer (P2P) architecture achieved great successes. Now, the P2P model has been adopted for many other distributed applications, such as instant message and phone services, Internet gaming, and large-scale scientific computing. In recent years, P2P streaming systems experienced tremendous growth and became one of the largest bandwidth consumers on the Internet. Compared to standard file sharing systems, the streaming services show unique characteristics with more stringent time constraints and require much higher network bandwidth. It is extremely important to evaluate and analyze existing applications, and investigate the merits and weaknesses in these systems for future development. In this paper, we conduct a comprehensive measurement study on two of the most popular P2P streaming systems, namely, PPLive and PPStream. They are very popular P2P streaming applications, and serving millions of registered users with hundreds of live TV channels and millions of other video clips. In our measurement, we deploy our collectors in China, and both live TV and video-on-demand (VoD) channels are evaluated. We record run-time network traffic on the client side, compare and analyze the characteristics of these channels based on their popularity. For both categories, we perceive that, in general, the two measured P2P streaming systems provide satisfactory experience to the audiences for all channels regardless of popularity. However, the most of data are downloaded from the dedicated servers for unpopular channels. We also observe that live TV channels show better peer coordination than VoD channels. Beside the traffic, we have also collected cache replacement information for VoD channels, and these measurement results can help us understand the caching mechanism of P2P streaming systems. With the support of the cache, VoD channels perform better than their counterparts in the live TV category in terms of data transmission, workload distribution, and signal traffic overhead. Overall, our results reveal that although P2P streaming systems can usually provide excellent viewing experience for popular channels, there are still challenges to fully support unpopular channels. New designs and algorithms are in urgent need, especially for unpopular live TV channels.     

Homogenous spiking neural P systems with anti-spikes

Spiking neural P systems with anti-spikes (ASN P systems, for short) are a class of neural-like computing models in membrane computing, which are inspired by neurons communication through both excitatory and inhibitory impulses (spikes). In this work, we consider a restricted variant of ASN P systems, called homogeneous ASN P systems, where any neuron has the same set of spiking and forgetting rules. As a result, we prove that such systems can achieve Turing completeness. Specifically, it is proved that two categories of pure form of spiking rules (for a spiking rule, if the language corresponding to the regular expression that controls its application is exactly the form of spikes consumed by the rule, then the rule is called pure) are sufficient to compute and accept the family of sets of Turing computable natural numbers.     

P systems with local graph productions

P systems (membrane systems) of various types so far mainly have been considered as computing devices working on multisets or strings. In this paper we investigate P systems with local graph productions generating weakly connected directed graphs. At least when equipped with a priority relation on the rules, such P systems can generate any recursively enumerable language of weakly connected directed graphs with only one membrane. Rudolf Freund, Ph.D.: He holds a master and doctor degree in computer science and a master degree in mathematics and physics. Since 1995 he is Associate Professor at the Vienna University of Technology in Austria. His research interests include array and graph grammars, regulated rewriting, infinite words, syntactic pattern recognition, neural networks, and especially models and systems for biological computing. In these fields, he is author or co-author of more than ninety scientific papers. Marion Oswald, Ph.D.: She received her master and doctor degree in computer science from the Vienna University of Technology, Austria, in 2001 and 2003, respectively. Her research interests include but are not limited to artificial life as well as models and systems for biological computing, in which fields she is author or co-author of more than fifteen scientific papers.     

Spiking neural P systems with neuron division and budding

Spiking neural P systems are a class of distributed and parallel computing models inspired by spiking neurons.In this work,the features of neuron division and neuron budding are introduced into the framework of spiking neural P systems,which are processes inspired by neural stem cell division. With neuron division and neuron budding,a spiking neural P system can generate exponential work space in polynomial time as the case for P systems with active membranes.In this way,spiking neural P systems can efficie...     

Using model checking to assess the dependability of agent-based systems

Model checking and the problem of analyzing the dependability of complex agent-based systems are well matched. Mathematical models of simple agents are relatively straightforward to specify. We can construct a model of the system as a whole from the models of the individual agents, and we can easily express dependability properties in the logical language used in model checking. However, there's one crucial mismatch: the state spaces of complex systems are many orders of magnitude larger than automated model-checking tools can handle. So, the mathematical models of computing systems that we use in model checking must be much simpler than the systems we are modeling. Yet, the models must contain all the detail that's essential to the dependability analysis we are performing, because omitting relevant detail can invalidate the analysis results. To make model checking of agent-based systems feasible and useful, we must answer two crucial questions. Here we describe our current best answers to these questions and how we've applied them to a real-world problem - assessing the UltraLog system.     

An Eigentrust dynamic evolutionary model in P2P file-sharing systems

Many reputation systems have been proposed to distinguish malicious peers and to ensure the quality of the service in P2P file sharing systems. Most of those reputation systems implicitly assumed that normal peers are always altruistic and provide their resources unconditionally when requested. However, as independent decision makers in real networks, peers can be completely altruistic (always cooperative, ALLC), purely selfish (always defective, ALLD), or reciprocal (R). In addition, those systems do not provide an effective method to reduce free-riders in P2P networks. To address these two problems, in this paper, we propose an EigenTrust evolutionary game model based on the renowned EigenTrust reputation model. In our model, we use evolutionary game theory to model strategic peers and their transaction behaviors, which is close to the realistic scenario. Many experiments have been designed and performed to study the evolution of strategies and the emergence of cooperation under our proposed EigenTrust evolutionary model. The simulation results showed that rational users are inclined to cooperate (enthusiastically provide resources to other peers) even under some conditions in which malicious peers try to destroy the system.     

Experimental evaluation of software development tools for safety-critical real-time systems

Since the early years of computing, programmers, systems analysts, and software engineers have sought ways to improve development process efficiency. Software development tools are programs that help developers create other programs and automate mundane operations while bringing the level of abstraction closer to the application engineer. In practice, software development tools have been in wide use among safety-critical system developers. Typical application areas include space, aviation, automotive, nuclear, railroad, medical, and military. While their use is widespread in safety-critical systems, the tools do not always assure the safe behavior of their respective products. This study examines the assumptions, practices, and criteria for assessing software development tools for building safety-critical real-time systems. Experiments were designed for an avionics testbed and conducted on six industry-strength tools to assess their functionality, usability, efficiency, and traceability. The results some light on possible improvements in the tool evaluation process that can lead to potential tool qualification for safety-critical real-time systems.     

Fighting pollution attacks in P2P streaming

In recent years, the demand for multimedia streaming over the Internet is soaring. Due to the lack of a centralized point of administration, Peer-to-Peer (P2P) streaming systems are vulnerable to pollution attacks, in which video segments might be altered by any peer before being shared. Among existing proposals, reputation-based defense mechanisms are the most effective and practical solutions. We performed a measurement study on the effectiveness of this class of solutions. We implemented a framework that allows us to simulate different variations of the reputation rating systems, from the centralized global approaches to the decentralized local approaches, under different parameter settings and pollution models. One key finding is that a centralized reputation system is only effective in static network and in defending against light pollution attacks. In general, a fully distributed reputation system is more suitable for the “real-time” P2P streaming system, since it is better in handling network dynamics and fast in detecting the polluters. Based on this key finding, we propose DRank, a fully distributed rank-based reputation system. Experimental results show that this technique is more flexible and robust in fighting pollution attacks.     

移动计算系统中的自适应位置更新策略

移动计算系统中一个很重要的问题就是管理移动客户机的实时位置.在现有商业的移动计算系统中,采用一种两层的体系结构.这种两层的结构不具有可扩展性,因而不能适应具有大量移动用户的新型移动计算应用.人们提出了一种新的层次结构的位置数据库结构,系统中的位置数据库组成一个树形结构以方便移动用户位置查找.尽管这种结构把位置更新及查询的任务在系统中的所有位置数据库中进行了分摊,它也有其自身的弱点:位置更新的代价较大及位置查询的延迟较长.研究了树形位置数据库结构中的位置更新策略,给出了一个位置变更的阈值计算方法,以使得位置管理的代价最少.     

Evaluation of P2P and cloud computing as platform for exhaustive key search on block ciphers

Over the years, parallel computing models have been proposed to solve large-scale application problems. P2P and cloud computing are well-known distributed computing models and have the advantage of running and implementing the parallel computing. Applying the advantages of both models can enhance the benefits of parallel computing. In this paper, we analyze the efficiency of key search algorithm by combining P2P and cloud computing. For our experiment, we apply the key search algorithm in the field of cryptography. The length of the key, which is stable criterion of cryptographic algorithm, is judged according to the amount of exhaustive key search. And the key space required for the whole investigation is easy to divide and is very appropriate for parallel calculation of P2P environment. In addition, cloud computing can provide the fitting environment to meet the various user requirements using virtualization technology. We conduct the following two performance experiments with P2P and cloud computing. First, we propose the method to guarantee the performance in P2P environment based on virtualization. Next, we simulate the performance of the suggested encryption method in the aforementioned system environment. Results reveal effectiveness and validity of the proposed system environment, which can also provide both scalability and flexibility.     

Experiments on the reliability of stochastic spiking neural P systems

In the area of membrane computing, time-freeness has been defined as the ability for a timed membrane system to produce always the same result, independently of the execution times associated to the rules. In this paper, we use a similar idea in the framework of spiking neural P systems, a model inspired by the structure and the functioning of neural cells. In particular, we introduce stochastic spiking neural P systems where the time of firing for an enabled spiking rule is probabilistically chosen and we investigate when, and how, these probabilities can influence the ability of the systems to simulate, in a reliable way, universal machines, such as register machines.     

UM-RTCOM: An analyzable component model for real-time distributed systems

Component-based development is a key technology in the development of software for modern real-time systems. However, standard component models and tools are not suitable for this type of system, since they do not explicitly address real time, memory or cost constraints. This paper presents a new predictable component model for real-time systems (UM-RTCOM) together with a set of tools to support it. The environment allows new components to be developed which can then be assembled to build complete applications, including hardware interaction. The model includes support for real-time analysis at the component and application level. The analysis is achieved by combining component meta-information in the form of an abstract behaviour model and a method to measure worst-case execution times in the final platform. Additionally, we propose an implementation model based on RT-CORBA where the developer uses the UM-RTCOM components and a set of tools to map these elements to elements of the desired platform. In order to apply our proposals, we have used the model and tools in real applications specifically in the context of nuclear power plant simulators.     

Concurrency control strategies for ordered data broadcast in mobile computing systems

Although data broadcast has been shown to be an efficient method for disseminating data items in mobile computing systems, the issue on how to ensure consistency and currency of data items provided to mobile transactions (MT), which are generated by mobile clients, has not been examined adequately. While data items are being broadcast, update transactions may install new values for them. If the executions of update transactions and the broadcast of data items are interleaved without any control, mobile transactions may observe inconsistent data values. The problem will be more complex if the mobile clients maintain some cached data items for their mobile transactions. In this paper, we propose a concurrency control method, called ordered update first with order (OUFO), for the mobile computing systems where a mobile transaction consists of a sequence of read operations and each MT is associated with a time constraint on its completion time. Besides ensuring data consistency and maximizing currency of data to mobile transactions, OUFO also aims at reducing data access delay of mobile transactions using client caches. A hybrid re-broadcast/invalidation report (IR) mechanism is designed in OUFO for checking the validity of cached data items so as to improve cache consistency and minimize the overhead of transaction restarts due to data conflicts. This is highly important to the performance of the mobile computing systems where the mobile transactions are associated with a deadline constraint on their completion times. Extensive simulation experiments have been performed to compare the performance of OUFO with two other efficient schemes, the multi-version broadcast method and the periodic IR method. The performance results show that OUFO offers better performance in most aspects, even when network disconnection is common.