Streaming applications usually run on heterogeneous multiprocessor platforms and are required to have a high throughput, which in turn may increase the energy consumption. A trade-off between these two criteria is important for a system. Synchronous data flow graphs (SDFGs) are widely used to model streaming applications. In this paper, we propose a paralleled Pareto optimal scheduling method (PPOS) for SDFGs on heterogeneous multiprocessors. It deals with both time arrangement and processor allocation of computations. PPOS is an exact method to chart the Pareto space of energy consumption and throughput, and to find all Pareto optimal schedules of a system model. An approximation technique is presented to further increase the scalability of our methods. Our experiments are carried out on a practical multimedia application with different configurations and hundreds of synthesis graphs. The results show that the proposed methods are capable of dealing with large-scale models.

With the process of non-functional properties research on real-time systems, multi-resource estimation and analysis of real-time systems become a hotspot. Process algebra is a formal method that is fit for analyzing the functional properties of real-time systems, but it cannot analyze the multi-resource properties. Resource timed process algebra (RTPA) proposed in this paper can handle it efficiently by extending multi-resource semantics on timed communicating sequential process (TCSP). The multi-resource consumption of real-time instruction is mapped into the resource vector of RTPA, and then the multi-resource consumption of real-time systems can be modeled and optimized by using RTPA; the resource optimal checking algorithms are proposed to check the multi-resource satisfiability of instructions and calculate the minimum resource and accumulated resource of real-time systems. This formal method improves the accuracy and efficiency of multi-resource calculation, and the calculation results can be further used to quantitatively analyze and optimize the multi-resource consumption of real-time systems.

The behaviour mismatch analysis is absolutely necessary for guaranteeing the correct composition of web services. In order to improve the reliability of the Web service composition, we present a mismatch detection method which can capture incompatible behavior and timed conflict among multiple asynchronous services. In this paper, we use software architecture description language XYZ/ADL based on temporal logic to describe Web service composition and use XYZ/RE to express the relative timed constraints. Additionally, we also set up a timed asynchronous service model TASM which can depict asynchronous interacting behavior and timed properties. In particular, the model satisfies the specification of model check UPPAAL. We convert XYZ/ADL description to TASM, and give the definition of compatibility. Then we use UPPAAL to realize mismatch detection of asynchronous Web services. Finally an example is demonstrated to illustrate how the approach we proposed works.

Service composition is becoming a central aspect in the new paradigm SaaS. In practice, most web services can not be integrated directly into applications because there are some mismatches in their interfaces. These mismatches may arise at different interoperability levels: technical, signature, behavioral, quality of service and semantic. In this paper, we present a model-based framework for generating adaptor protocol for a set of participating behavioral mismatching web services, which also have the ability to deal with time-related issues in QoS level. In order to detect interaction mismatches of time-aware web services, we introduce a formalism, called timed service protocol, to capture timed behavior of time-aware web services and implement automatic mismatch detection via model checker UPPAAL. Building upon this formalization, we present a mechanism to automatically generate adaptor protocol if interaction protocols of the participating time-aware web services are partial compatible. Meanwhile, we illustrate our framework with the help of order management system case study.

In wireless ad hoc networks, the constructed topology is preferred to be planar since a planar topology enables guaranteed delivery of packets without a routing table. Previous planar structures are statically constructed for the whole network. However, environmental or network dynamics such as channel status, interference, or residual energy will prevent such structures from providing the best service to the network. In this paper, we present a t-adjustable planar structure (TAP) which enables each node to adjust the topology independently via a parameter t and allows nodes to have different path loss exponent. TAP is based on three well-known planar structures: Gabriel Graph, Relative Neighborhood Graph, and Local Minimum Spanning Tree. We show properties of TAP by proof or simulation: (1) It preserves connectivity; (2) it is planar, sparse, and symmetric; (3) it preserves all minimum energy path when t = 1 for all nodes; and (4) the average transmission power, interference, and node degree decrease as t increases and the maximum node degree is bounded by 6 when t = 3 for all nodes.

In wireless ad hoc networks, a planar topology enables nodes to deliver packets without a routing table. Pervious planar structures are fixed for the whole network. However, environmental or network dynamics such as channel status, interference or energy will prevent such structures from providing the best service to the network. In this paper, we present a t-adjustable planar structure (TAP) which enables nodes to adjust the topology independently and allows nodes to have different path loss exponent. We show by proof or simulation properties of TAP: (1) It preserves connectivity; (2) It is planar, sparse and symmetric; (3) It preserves all minimum energy path when t=1 for all nodes; (4) The average transmission power, interference and node degree decrease as t increases and the maximum node degree is bounded by 6 when t=3 for all nodes.

The dimensions of twisted cubes in the original definition of twisted cubes are only limited to odd integers. In this paper, we first extend the dimensions of twisted cubes to all the positive integers. Then, we introduce the concept of the set of restricted faulty nodes into twisted cubes. We further prove that under the condition that each node of the n-dimensional twisted cube TQnhas at least one fault-free neighbor its restricted connectivity is 2n - 2, which is almost as twice as that of TQnunder the condition of arbitrary faulty nodes, the same as that of the n-dimensional hypercube. Moreover, we give an O(N log N) fault-free unicast algorithm, where N denotes the node number of TQn-1. Finally, we give the simulation result of the expected length of the fault-free path gotten by our algorithm.

It has been widely recognized that inconsistencies of- ten appear and are inevitable when specifying large and complex concurrent systems. In this paper, a non-classical temporal logic QCTL (quasi-classical temporal logic) is introduced, which subsumes both QCL and CTL. It is para- consistent, i.e., it can be used to reason non-trivially about system specifications containing inconsistent information. A semantics for QCTL is proposed in terms of paraKripke structures (the extended Kripke strucutres). Furthermore, a sound and complete proof system for QCTL is presented. Although the models and proof theory of QCTL are different comparing with classical logics like CTL, most natural and intuitive properties are preserved. This work bridges the gap between the specification and verification of temporal aspects and non-trivial reasoning under inconsistency.