Abstract In many verification tasks, system models do not correspond to the focused and idealized models that appear in research literature. In practice, models usually contain components and execution paths that are irrelevant to the property being verified or have only a limited effect on it. Compositional verification presents a practical method for coping with the larger and less targeted models found in such settings. In this paper, we present an automated compositional framework for verifying timed safety properties in networks of timed automata. We show as a main result that the weakest environment assumption, commonly used in compositional reasoning, may in general fail to be recognizable within the timed automata formalism. This negative result motivates shifting the focus to the complement language of violation-inducing timed words, for which we establish recognizability using timed automata with silent transitions. We provide an algorithm for its construction and reduce its size by retaining only the parts directly relevant to the property. The synthesized assumption is later applied to verify the original system. This provides a sound and complete basis for compositional verification of timed automata, including the novel ability to handle automata with multiple clocks and non-deterministic behavior. Our results broaden the applicability of assume–guarantee verification techniques in timed automata and show substantial reductions in the size of the state-space, outperforming monolithic methods on a range of case studies.

This paper centers around a multiple-input-multiple-output (MIMO) visible light communication (VLC) system, where an unmanned aerial vehicle (UAV) benefits from a light emitting diode (LED) array to serve photo-diode (PD)equipped users for illumination and communication simultaneously. Concerning the battery limitation of the UAV and considerable energy consumption of the LED array, a hybrid dimming control scheme is devised at the UAV that effectively controls the number of glared LEDs and thereby mitigates the overall energy consumption. To assess the performance of this system, a radio resource allocation problem is accordingly formulated for jointly optimizing the motion trajectory, transmit beamforming and LED selection at the UAV, assuming that channel state information (CSI) is partially available. By reformulating the optimization problem in Markov decision process (MDP) form, we propose a soft actor-critic (SAC) mechanism that captures the dynamics of the problem and optimizes its parameters. Additionally, regarding the high mobility of the UAV and thus remarkable rearrangement of the system, we enhance the trained SAC model by integrating a meta-learning strategy that enables more adaptation to system variations. By defining energy efficiency as a trade-off between the data rate and power consumption, simulations verify that upgrading a single-LED UAV by an array of 10 LEDs, exhibits 47 % and 34 % improvements in data rate and energy efficiency, albeit at the expense of 8 % more power consumption.

This endeavor centers around downlink transmission of a base station (BS), outfitted with a stacked intelligent metasurface (SIM) that realizes an energy-efficient wave-domain multi-user beamforming. The underlying network includes mobile devices with multimedia service requirements, including web surfing, HTTP live video streaming and voice-over-LTE (VoLTE). Rather than conventional quality-of-service (QoS) metrics, we assess the satisfaction level of users relying on quality-of-experience (QoE) criteria. Invoking mean opinion score (MOS) as the subjective measurement of QoE, we also evaluate the overall efficacy of this system by posing a resource allocation optimization problem aimed at maximizing the achievable MOS of all users, while adhering to their minimum MOS requirements and the maximum transmit power budget of the BS. Due to the interdependency of optimization variables and non-convex nature of the problem, we first reformulate it in Markov decision process, which captures its dynamic traits. Relying on the MDP model, a conservative Q-learning (CQL) agent is trained for jointly designing the optimization variables, including the BS downlink transmit power, as well as the electromagnetic response of the SIM. In light of real-time mobility of users and the resulting non-trivial network dynamism, we further utilize meta-learning technique to enhance the adaptability and generalization of the CQL agent. Numerically, it is demonstrated that, respectively, 31%, 44% and 26% superior average MOS is achieved, for web, video and audio services, compared to traditional QoS-driven resource allocation.

This research investigates a wireless system in which a base station (BS), outfitted with a stacked intelligent meta-surface (SIM), performs wave-domain multi-user beamforming in downlink transmission. The communication benefits from the assistance of an active reconfigurable intelligent surface (RIS) that amplifies incoming signal strength to extend the network coverage. System performance is evaluated through the formulation of a resource allocation optimization problem aimed at maximizing the number of served users while adhering to their quality-of-service demands and the maximum transmit power budget of the BS. Due to the complex interdependencies among optimization variables and the non-convex nature of the problem, we first reformulate it in Markov decision process, which captures its dynamic traits. Subsequently, a maximum a posteriori policy optimization (MPO) agent is trained for jointly designing the optimization variables, including the BS transmit power, the electromagnetic response of the SIM, as well as the amplitude/phase of the active RIS. In light of real-time mobility of users and non-trivial network dynamism, we invoke the integration of meta-learning technique to enhance the adaptability and generalization of the MPO model. Numerically, it is demonstrated that incorporating an active RIS upscales the number of served users by 57% and 113%, on average, in comparison with existing passive RIS-assisted and conventional SIM-enabled systems, respectively.

Downlink transmission of a nonorthogonal visible light communication (VLC) system, empowered by autonomous aerial vehicles (AAVs), is studied for coexisting enhanced mobile broadband (eMBB), ultrareliable low-latency communication (URLLC), and massive machine-type communication (mMTC) services. A joint resource allocation problem involving user association, transmit power, and flight trajectory of AAVs is formulated, with the goal of characterizing a multiobjective tradeoff as a weighted sum of the power consumption of each AAV and the perceived Quality of Experience (QoE) of its associated eMBB users, while ensuring the service-specific requirements for eMBB, mMTC, and URLLC are met. Assuming the imperfection of channel state information (CSI), we invoke a generalized Benders decomposition (GBD) methodology, leveraging tools from convex optimization and multiagent deep reinforcement learning to address this problem. We further analytically derive the upper and lower bounds on the reward function for each AAV as a learning agent. Extensive simulations confirm that our proposed method outperforms the single-agent counterpart in the literature, with up to a 22% reduction in power consumption and a 13% gain in perceived QoE. Additionally, compared to the globally optimal brute-force method for AAV-user association, our proposed method experiences only a trivial performance loss in a small-scale scenario.

Software-defined networks (SDNs) provide customizable traffic control by storing numerous rules in on-chip memories with minimal access latency. However, the current on-chip memory capacity falls short of meeting the growing demands of SDN control applications. While rule eviction and aggregation strategies address this challenge at the switch level, programmable data planes enable a more flexible approach through cooperative rule caching. However, current solutions rely on computationally intensive off-the-shelf solvers to perform rule placement across the network. In this paper, we present an efficient solution for the cooperative rule caching problem. We first present the design of a resource-efficient switch capable of caching rules for its neighbors alongside a lightweight protocol for retrieving cached rules. Then, we introduce RaSe, an approximation algorithm for minimizing rule lookup latency across the network through optimized cooperation-aware rule placement. We conduct a theoretical analysis of RaSe, followed by a P4-based proof-of-concept assessment in Mininet and a large-scale numerical evaluation using real-world network topology. In comparison with existing solver-based solutions, the proposed method obtains the solution 160 times faster and improves the average rule lookup latency by about 21% compared to several algorithmic baselines.

Large-scale services are deployed in data centers using clusters of servers, and load balancers (LB) are responsible for distributing requests for a service among its servers. Layer-4 (L4) LBs process requests faster than Layer-7 (L7) ones, but they cannot provide session-persistent load balancing, and therefore, they direct connections of an application-level session to different servers. On the other side, L7 LBs can direct all requests of an application-level session to the same server, but they have a very limited capacity because they act as a reverse-proxy and process requests at the application layer. We present “Yuz”, a stateless session-persistent load balancer that does not act as a reverse-proxy. Yuz works near layer 4, and it makes use of TLS session data instead of processing incoming requests at the application level. Our evaluations show that the request rate that can be handled by cluster-based services equipped with Yuz is twice as high as when the clusters use the best existing load balancers. Yuz also significantly reduces the average and tail of the clusters’ response time. Moreover, while each of the existing session-persistent LBs works only for a specific application, Yuz provides an application-independent session-persistent load balancing.

Downlink transmission of non-orthogonal multiple access visible light communication systems empowered by an unmanned aerial vehicle (UAV) is considered for multiplexing enhanced mobile broadband (eMBB) and massive machine type communication (mMTC) services. Accordingly, a resource allocation problem of joint transmit power control and motion trajectory design of the DAVs is formulated, whose goal is to characterize a multi-objective trade-off as a weighted sum of the UAVs' power consumption and the perceived quality-of-experience (QoE) of eMBB users, while ensuring the eMBB and mMTC service-specific requirements. We leverage an alternative decomposition and tools from convex optimization and actorcritic multi-agent deep reinforcement learning to address this problem in an iterative fashion. We analytically derive the upper-and lower-bounds on the reward of the DAVs as the learning agents and demonstrate that the proposed resource allocation method outperforms the similar scheme in literature, by up to 17% average reduced power consumption, as well as 12% average perceived QoE gain.

Companies depend on mining data to grow their business more than ever. To achieve optimal performance of Big Data analytics workloads, a careful configuration of the cluster and the employed software framework is required. The lack of flexible and accurate performance models, however, render this a challenging task. This article fills this gap by presenting accurate performance prediction models based on Stochastic Activity Networks (SANs). In contrast to existing work, the presented models consider multiple work queues, a critical feature to achieve high accuracy in realistic usage scenarios. We first introduce a monolithic analytical model for a multi-queue YARN cluster running DAG-based Big Data applications that models each queue individually. To overcome the limited scalability of the monolithic model, we then present a fixed-point model that iteratively computes the throughput of a single queue with respect to the rest of the system until a fixed-point is reached. The models are evaluated on a real-world cluster running the widely-used Apache Spark framework and the YARN scheduler. Experiments with the common transaction-based TPC-DS benchmark show that the proposed models achieve an average error of only$5.6\%$in predicting the execution time of the Spark jobs. The presented models enable businesses to optimize their cluster configuration for a given workload and thus to reduce their expenses and minimize service level agreement (SLA) violations. Makespan minimization and per-stage analysis are examined as representative efforts to further assess the applicability of our proposition.

We study the behavior of epidemic routing in a delay tolerant network as a function of node density. Focusing on the probability of successful delivery to a destination within a deadline (PS), we show that PS experiences a phase transition as node density increases. Specifically, we prove that PS exhibits a phase transition when nodes are placed according to a Poisson process and allowed to move according to independent and identical processes with limited speed. We then propose four fluid approximations to evaluate the performance of epidemic routing in non-sparse networks. An ordinary differential equation (ODE) is proposed for supercritical networks based on approximation of the infection rate as a function of time. Other ODEs are based on the approximation of thepairwise infection rate. Two of them, one for subcritical networks and another for supercritical networks, use the pairwise infection rate as a function of the number of infected nodes. The other ODE uses pairwise infection rate as a function of time, and can be applied for both subcritical and supercritical networks achieving good accuracy. The ODE for subcritical networks is accurate when density is not close to the percolation critical density. Moreover, the ODEs that target only supercritical regime are accurate.

The era of personal resources being sufficient for enterprise big data computations has passed. As computations are executed in the cloud, small policy changes of cloud operators may cause considerable changes in operational costs. Carefully choosing the amount of resources for a given application is thus of great importance. This, however, requires a priori knowledge of the application's performance under different configurations. Creating a performance prediction model needs to account for the heterogeneity of resources and the diversity in application workflows. Previous approaches for heterogeneous environments consider a black-box representation of the application which results in single-purpose models. This paper addresses the problem with two gray-box prediction models using linear programming (LP) and mixed-integer linear programming (MILP). Given a set of available resources, the models consider Apache Spark applications and their Directed Acyclic Graph (DAG) of workflow running on top of a Hadoop-YARN cluster. We then propose a configuration recommendation algorithm to optimize the cost-performance trade-offs when renting machine instances. The accuracy of the proposed models is evaluated with real-world executions of several representative applications on the Wikipedia dataset and the TPC-DS benchmark. The average error of only 3.28% for the proposed prediction models demonstrates the practicality of the proposed approach in handling cost-performance trade-offs.

The Social Internet of Things (SIoT), integration of the Internet of Things, and Social Networks paradigms, has been introduced to build a network of smart nodes that are capable of establishing social links. In order to deal with misbehaving service provider nodes, service requestor nodes must evaluate their trustworthiness levels. In this article, we propose a novel trust management mechanism in the SIoT to predict the most reliable service providers for each service requestor, which leads to reduce the risk of being exposed to malicious nodes. We model the SIoT with a flexible bipartite graph (containing two sets of nodes: service providers and service requestors), then build a social network among the service requestor nodes, using the Hellinger distance. Afterward, we develop a social trust model using nodes’ centrality and similarity measures to extract trust behaviors among the social network nodes. Finally, a matrix factorization technique is designed to extract latent features of SIoT nodes, find trustworthy nodes, and mitigate the data sparsity and cold start problems. We analyze the effect of parameters in the proposed trust prediction mechanism on prediction accuracy. The results indicate that feedbacks from the neighboring nodes of a specific service requestor with high Hellinger similarity in our mechanism outperforms the best existing methods. We also show that utilizing the social trust model, which only considers a similarity measure, significantly improves the accuracy of the prediction mechanism. Furthermore, we evaluate the effectiveness of the proposed trust management system through a real-world SIoT use case. Our results demonstrate that the proposed mechanism is resilient to different types of network attacks, and it can accurately find the most proper and trustworthy service provider.

Abstract Quality of Service (QoS) of Web services plays an essential role in selecting Web services by consumers. The dynamic QoS attributes of Web services have different values for different users. Therefore, the value of many Web services' QoS features for many users are undetermined, and these values should be predicted. The collaborative filtering (CF) method is one of the most successful approaches to predict these values. CF‐based methods use the QoS values contributed by the other users for prediction and, consequently, the values contributed by unreliable users can decrease the accuracy of prediction. To utilize the reputation of users can be regarded as one of the conventional approaches to overcome this problem. In this paper, we have defined a concept called regional reputation that represents the reputation of a user for users in each geographical region. Regional reputation has been achieved with the combination of the location information of the users and their reputation. Subsequently, by combining this concept with the matrix factorization, we have proposed a prediction method called regional reputation‐based matrix factorization. This approach has been able to improve the accuracy of prediction and be more persistent to the data contributed by unreliable users.

Abstract The majority of studies in the field of developing identification and authentication protocols for Internet of Things (IoT) used cryptographic algorithms. Using brain signals is also a relatively new approach in this field. EEG signal‐based authentication algorithms typically use feature extraction algorithms that require high processing time. On the other hand, the dynamic nature of the EEG signal makes its use for identification/authentication difficult without relying on feature extraction. This paper presents an EEG‐and fingerprint‐based two‐stage identification‐authentication protocol for remote healthcare, which is fast, robust, and multilayer‐based. A modified Euclidean distance pattern matching method is proposed to match the EEG signal in the identification stage due to its dynamic nature. The authentication stage is also an optimized method with the Genetic Algorithm (GA), which utilizes a modified Diffie–Hellman algorithm. Due to the vulnerability of the Diffie–Hellman algorithm to different types of attacks, the parameters used for this algorithm are extracted from the fingerprint and the EEG signal of the patient to provide a fast and robust authentication method. The proposed method is evaluated using data from patients with spinal cord injuries. Simulating results demonstrated high identification and authentication accuracy of the proposed method. Furthermore, it is extremely fast and efficient.

Abstract In cloud computing services, high availability is one of the quality of service requirements which is necessary to maintain customer confidence. High availability systems can be built by applying redundant nodes and multiple clusters in order to cope with software and hardware failures. Due to cloud computing complexity, dependability analysis of the cloud may require combining state‐based and nonstate‐based modeling techniques. This article proposes a hierarchical model combining reliability block diagrams and continuous time Markov chains to evaluate the availability of OpenStack private clouds, by considering different scenarios. The steady‐state availability, downtime, and cost are used as measures to compare different scenarios studied in the article. The heterogeneous workloads are considered in the proposed models by varying the number of CPUs requested by each customer. Both hardware and software failure rates of OpenStack components used in the model are collected via setting up a real OpenStack environment applying redundancy techniques. Results obtained from the proposed models emphasize the positive impact of redundancy on availability and downtime. Considering the tradeoff between availability and cost, system providers can choose an appropriate scenario for a specific purpose.

There are a vast number of cloud service providers, which offer virtual machines (VMs) with different configurations. From the companies perspective, an appropriate selection of VMs is an important issue, as the proper service selection leads to improved productivity, higher efficiency, and lower cost. An effective service selection cannot be done without a systematic approach due to the modularity of requests, the conflicts between requirements, and the impact of network parameters. In this paper, we introduce an innovative framework, called PCA, to solve service selection problem in the hybrid environment of peer-assisted, public, and private clouds. PCA detects the conflicts between the requests and enterprises policies, finds proper services based on the requirements, and reduces VMs rent and end-to-end network costs. PCA selects the services from multiple clouds to utilize resources and reduce the total cost. Our proposed framework utilizes set theory, B+ tree, and greedy algorithms to meet its goals. The simulation results show that PCA can reduce up to 30 percent of cloud-related costs and can achieve answers at least seven times faster in comparison to recent studies.

We study queues with impatient customers and Processor Sharing (PS) discipline as well as other variants of PS discipline, namely, Discriminatory Processor Sharing (DPS) and Generalized Processor Sharing (GPS) disciplines, where customers have deadlines until the end of service (DES). Customers arrive according to a state-dependent Poisson process and have general impatience. Customers have exponential service times with state-dependent service rates. Analytical methods based on simple Markov chains are given for the performance analysis of such queues. The principal measures of performance are the steady-state probability of missing deadline and the steady-state probability of blocking. Similar results are obtained for related queues with Random Order Service (ROS) discipline where customers have deadlines until the beginning of service (DBS). In view of a lack of exact analytical results for First Come First Served (FCFS) queues with state-dependent rates, a highly accurate approximation method is also given for these latter queues. The efficacy and accuracy of the approach are illustrated by some numerical examples and simulation experiments.

In this paper, we propose a robust solution for the path planning and scheduling of the moving objects in a Track-based Traffic Control System (TTCS). The moving objects in a TTCS pass over pre-specified sub-tracks. Each sub-track accommodates at most one moving object in-transit. Due to the uncertainties in the context of a TTCS, we assign an arrival time window to each moving object for each sub-track in its route, instead of an exact value. The moving object can safely enter into the sub-track in the mentioned time window. To develop a safe plan, we adapt the tagged-signal model and provide a rigorous mathematical formalism for the actor model of a TTCS. To illustrate the applicability of the provided semantics, we provide a formal model of TTCSs in the Alloy language and use its analyzer to verify the developed model against system safety properties.

While the cost of the access network could be considerably reduced by the use of caching, this is not currently happening because content providers (CPs), who alone have the detailed demand data required for optimal content placement, have no natural incentive to use them to minimize access network operator (ANO) expenditure. We argue that ANOs should therefore provide such an incentive in the form of direct subsidies paid to the CPs in proportion to the realized savings. We apply coalition game theory to design the required subsidy framework and propose a distributed algorithm, based on Lagrangian decomposition, allowing ANOs and CPs to collectively realize the optimal memory for bandwidth tradeoff. The considered access network is a cache hierarchy with per-CP central office caches, accessed by all ANOs, at the apex, and per-ANO dedicated bandwidth and storage resources at the lower levels, including wireless base stations, that must be shared by multiple CPs.

Cloud systems empower the big data management by providing virtual machines (VMs) to process data nodes (DNs) in a faster, cheaper and more effective way. The efficiency of a VM allocation is an important concern that is influenced by the communication latencies. In the literature, it has been proved that the VM assignment minimizing communication latency in the presence of the triangle inequality is 2-approximation. However, a 2-approximation solution is not efficient enough as data center networks are not limited to the triangle inequality. In this paper, we define the quadrilateral inequality property for latencies such that the time complexity of the VM assignment problem minimizing communication latency in the presence of the quadrilateral inequality is in P (polynomial) class. Indeed, we propose an algorithm for the problem of assigning VMs to DNs to minimize the maximum latency among allocated VMs in addition to DNs with their assigned VMs. This algorithm is latency optimal and 2-approximation for networks with the quadrilateral inequality and the triangle inequality, respectively. Besides, the extension of the proposed method can be applied to the cloud elasticity. The simulation results illustrate the good performance and scalability of our method in various known data center networks.

The increasing demand for Web services encourages commercial cloud service providers to publish their own services with various functional and nonfunctional capabilities in different cloud platforms. The aggregation of atomic services from multiple service repositories is the main idea of the service composition concept in multiclouds. The cloud Web service composition is a suitable way for satisfying users' complex requests by integrating services from different clouds in order to create a new value-added composite service. The time required to serve a composite service by a multicloud environment is an important parameter, which depends on different factors, ranging from the service composition and selection algorithm to the number of atomic services published in the clouds. In this paper, a model based on timed colored Petri nets (TCPNs) is proposed to evaluate the service composition in multicloud environments while minimizing the number of clouds involved in serving a composite service request. The proposed TCPN graphically models the process of request submission, composite service analysis, service selection, and service provisioning in a multicloud environment. It also assesses both mean response time of the environment and probability of dropping composite requests. The verification of the accuracy of the proposed model is done by comparing the results obtained from the TCPN model, in two different scenarios, with the results from the CloudSim framework. These results confirm that our proposed TCPN model can appropriately model the system and evaluate its performance more efficiently than the CloudSim.

This paper investigates the performance of epidemic routing, in mobile social networks (MSNs), which makes use of the store-carry-forward paradigm for communication. Real-life mobility traces show that people have skewed location visiting preferences, with some places visited frequently and some others infrequently. In order to model epidemic routing in MSNs, we first analyze the time taken for a node to meet the first node belonging to a set of nodes restricted to move in a specific subarea. Afterwards, a monolithic stochastic reward net (SRN) is proposed to evaluate the delivery delay and the average number of transmissions under epidemic routing by considering skewed location visiting preferences. This monolithic model is not scalable enough, in terms of the number of nodes and frequently visited locations. In order to achieve higher scalability, the folding technique is applied to the monolithic SRN and an approximate folded SRN is proposed to evaluate the performance of epidemic routing. Discrete-event simulation is applied to cross-validate the proposed models. Results indicate that the monolithic model has higher accuracy in predicting the performance of epidemic routing. The approximate folded model also achieves a good accuracy and can be solved for a network with a large number of nodes/frequently visited locations. This model is more accurate than the ordinary differential equation approach.

The paper revisits the performance evaluation of caching in a Named Data Networking (NDN) router where the content store (CS) is supplemented by a pending interest table (PIT) which aggregates requests for a given content that arrive within the download delay. We extend prior work on caching with non-zero download delay by proposing a novel mathematical framework that is applicable to general traffic models and alternative cache insertion policies. Specifically we consider the impact of time locality in demand due to finite content lifetimes and we evaluate the use of an LRU filter to improve CS hit rate performance. The analysis is used to demonstrate that the impact of the PIT on upstream bandwidth reduction is significant only for relatively small content catalogues or high average request rate per content. We also show that the filter can be counterproductive when contents have finite lifetimes and traffic intensity is low.

Few fuzzy temporal logics and modeling formalisms are developed such that their model checking is both effective and efficient. State-space explosion makes model checking of fuzzy temporal logics inefficient. That is because either the modeling formalism itself is not compact, or the verification approach requires an exponentially larger yet intermediate representation of the modeling formalism. To exemplify, Fuzzy Program Graph (FzPG) is a very compact, and powerful formalism to model fuzzy systems; yet, it is required to be translated into an equal Fuzzy Kripke model with an exponential blow-up should it be formally verified. In this paper, we introduce Fuzzy Computation Tree Logic (FzCTL) and its direct symbolic model checking over FzPG that avoids the aforementioned state-space explosion. Considering compactness and readability of FzPG along with expressiveness of FzCTL, we believe the proposed method is applicable in real-world scenarios. Finally, we study formal verification of fuzzy flip-flops to demonstrate capabilities of the proposed method.

Infrastructure as a Service (IaaS) is one of the most significant and fastest growing fields in cloud computing. To efficiently use the resources of an IaaS cloud, several important factors such as performance, availability, and power consumption need to be considered and evaluated carefully. Evaluation of these metrics is essential for cost-benefit prediction and quantification of different strategies which can be applied to cloud management. In this paper, analytical models based on Stochastic Reward Nets (SRNs) are proposed to model and evaluate an IaaS cloud system at different levels. To achieve this, an SRN is initially presented to model a group of physical machines which are controlled by a management layer. Afterwards, the SRN models presented for the groups of physical machines in the first stage are combined to capture a monolithic model representing an entire IaaS cloud. Since the monolithic model does not scale well for large cloud systems, two approximate SRN models using folding and fixed-point iteration techniques are proposed to evaluate the performance, availability, and power consumption of the IaaS cloud. The existence of a solution for the fixed-point approximate model is proved using Brouwer's fixed-point theorem. A validation of the proposed monolithic and approximate models against both an ad-hoc discrete-event simulator developed in Java and the CloudSim framework is presented. The analytic-numeric results obtained from applying the proposed models to sample cloud systems show that the errors introduced by approximate models are insignificant while an improvement of several orders of magnitude in the state space reduction of the monolithic model is obtained.

Execution speed seriously bothers application developers and users for wearable devices such as Google Glass. Intensive applications like 3D games suffer from significant delays when CPU is busy. Energy is another concern when the devices are in low battery level, but users need them for urgency use. To ease such pains, one approach is to expand the computational power by cloud offloading. This paradigm works well when the available Internet access has enough bandwidth. Another way is to leverage nearby devices for computation-offloading, which is known as device-to-device (D2D) offloading. In this paper, we present Dandelion, a unified code offloading system for wearable computing. Such applications can leverage both the nearby devices and cloud for performance acceleration and energy efficiency. Dandelion is a novel generic code offloading system for wearable computing with a reference implementation on Google Glass. Dandelion includes a programmer-friendly framework based on Java annotation, a lightweight offloading service, and a runtime task scheduler to make offloading decisions. We design some wearable applications and several parallel execution benchmark methods for Dandelion performance evaluation. Extensive experiments on a testbed of Google Glass and Android phones demonstrate that Dandelion generally achieves over 5X execution speedup for local execution and can quickly recover from errors caused by network disruption.

In some applicable scenarios, such as community patrolling, mobile nodes are restricted to move only in their own communities. Exploiting the meetings of the nodes within the same community and the nodes within the neighboring communities, a delay tolerant network (DTN) can provide communication between any two nodes. In this paper, two analytical models based on stochastic reward nets (SRNs) are proposed to evaluate the performance of the epidemic content retrieval in such multi-community DTNs. Performance measures computed by the proposed models are the average retrieval delay and the average number of transmissions. The monolithic SRN model proposed in the first step is not scalable, in terms of the number of communities and nodes, due to the state space explosion in the underlying Markov chain. In order to solve the scalability problem of the monolithic model, an approximate model based on the folding technique is presented which allows us to evaluate the performance of large-scale DTNs. In order to cross-validate the results obtained from the proposed models, we extend the ONE simulator to support our network model. The analytic-numeric results indicate that both models have good accuracy, and the folded model reduces the state space highly, achieving good scalability without any significant loss of accuracy.

In this paper, the performance of a grid resource is modeled and evaluated using stochastic reward nets (SRNs), wherein the failure–repair behavior of its processors is taken into account. The proposed SRN is used to compute the blocking probability and service time of a resource for two different types of tasks: grid and local tasks. After modeling a grid resource and evaluating the performability measures, an algorithm is presented to find the probability mass function (pmf) of the service time of the grid resource for a program which is composed of grid tasks. The proposed algorithm exploits the universal generating function to find the pmf of service time of a single grid resource for a given program. Therefore, it can be used to compute the pmf of the service time of entire grid environment for a workflow with several dependent programs. Each possible scheduling of programs on grid resources may result in different service times and successful execution probabilities. Due to this fact, a genetic-based scheduling algorithm is proposed to appropriately dispatch programs of a workflow application to the resources distributed within a grid computing environment. Numerical results obtained by applying the proposed SRN model, the algorithm to find the pmf of grid service time, and the genetic-based scheduling algorithm to a comprehensive case study demonstrate the applicability of the proposed approach to real systems.

The end-to-end throughput of multi-hop communication in wireless ad hoc networks is affected by the conflict between forwarding nodes. It has been shown that sending more packets than maximum achievable end-to-end throughput not only fails to increase throughput but also decreases throughput owing to high contention and collision. Accordingly, it is of crucial importance for a source node to know the maximum end-to-end throughput. The end-to-end throughput depends on multiple factors, such as physical layer limitations, medium access control (MAC) protocol properties, routing policy, and nodes' distribution. There have been many studies on analytical modeling of end-to-end throughput but none of them has taken routing policy and nodes' distribution as well as MAC layer altogether into account. In this paper, the end-to-end throughput with perfect MAC layer is obtained based on routing policy and nodes' distribution in 1-D and 2-D networks. Then, imperfections of IEEE 802.11 protocol are added to the model to obtain precise value. An exhaustive simulation is also made to validate the proposed models using ns-2 simulator. Results show that if the distribution to the next hop for a particular routing policy is known, our methodology can obtain the maximum end-to-end throughput precisely.

Key pre-distribution algorithms have recently emerged as efficient alternatives of key management in today’s secure communications landscape. Secure routing techniques using key pre-distribution algorithms require special algorithms capable of finding optimal secure overlay paths. To the best of our knowledge, the literature of key pre-distribution systems is still facing a major void in proposing optimal overlay routing algorithms. In the literature work, traditional routing algorithms are typically used twice to find a NETWORK layer path from the source node to the destination and then to find required cryptographic paths. In this paper, we model the problem of secure routing using weighted directed graphs and propose a Boolean linear programming (LP) problem to find the optimal path. Albeit the fact that the solutions to Boolean LP problems are of much higher complexities, we propose a method for solving our problem in polynomial time. In order to evaluate its performance and security measures,we apply our proposed algorithm to a number of recently proposed symmetric and asymmetric key pre-distribution methods. The results show that our proposed algorithm offers great network performance improvements as well as security enhancements when augmenting baseline techniques.

Public key management scheme in mobile ad hoc networks (MANETs) is an inevitable solution to achieve different security services such as integrity, confidentiality, authentication and non reputation. Probabilistic asymmetric key pre-distribution (PAKP) is a self-organized and fully distributed approach. It resolves most of MANET's challenging concerns such as storage constraint, limited physical security and dynamic topology. In such a model, secure path between two nodes is composed of one or more random successive direct secure links where intermediate nodes can read, drop or modify packets. This way, intelligent selection of intermediate nodes on a secure path is vital to ensure security and lower traffic volume. In this paper, subjective logic is used to improve PAKP method with the aim to select the most trusted and robust path. Consequently, our approach results in a better data traffic and also improve the security. Proposed algorithm chooses the least number of nodes among the most trustworthy nodes which are able to act as intermediate stations. We exploit two subjective logic based models: one exploits the subjective nature of trust between nodes and the other considers path conditions. We then evaluate our approach using network simulator ns-3. Simulation results confirm the effectiveness and superiority of the proposed protocol compared to the basic PAKP scheme.

One of the most relevant characteristics of social networks is community structure, in which network nodes are joined together in densely connected groups between which there are only sparser links. Uncovering these sparse links (i.e. intercommunity links) has a significant role in community detection problem which has been of great importance in sociology, biology, and computer science. In this paper, we propose a novel approach, called CS-ComDet, to efficiently detect the inter-community links based on a newly emerged paradigm in sparse signal recovery, called compressive sensing. We test our method on real-world networks of various kinds whose community structures are already known, and illustrate that the proposed method detects the inter-community links accurately even with low number of measurements (i.e. when the number of measurements is less than half of the number of existing links in the network).

The degree distribution is an important characteristic of complex networks. In many data analysis applications, the networks should be represented as fixed-length feature vectors and therefore the feature extraction from the degree distribution is a necessary step. Moreover, many applications need a similarity function for comparison of complex networks based on their degree distributions. Such a similarity measure has many applications, including classification and clustering of network instances, evaluation of network sampling methods, anomaly detection and study of epidemic dynamics. The existing methods are unable to effectively capture the similarity of degree distributions, particularly when the corresponding networks have different sizes. In this paper, we propose a feature extraction method and a similarity function for the degree distributions in complex networks. We propose to calculate the feature values based on the mean and standard deviation of the node degrees in order to decrease the effect of the network size on the extracted features. Experiments on a wide range of real and artificial networks confirms the accuracy, stability and effectiveness of the proposed method.

Abstract Recently, by defining suitable fuzzy temporal logics, temporal properties of dynamic systems are specified during model checking process, yet a few numbers of fuzzy temporal logics along with capable corresponding models are developed and used in system design phase, moreover in case of having a suitable model, it suffers from the lack of a capable model checking approach. Having to deal with uncertainty in model checking paradigm, this paper introduces a fuzzy Kripke model (FzKripke) and then provides a verification approach using a novel logic called Fuzzy Computation Tree Logic* (FzCTL*). Not only state space explosion is handled using well-known concepts like abstraction and bisimulation, but an approximation method is also devised as a novel technique to deal with this problem. Fuzzy program graph, a generalization of program graph and FzKripke, is also introduced in this paper in consideration of higher level abstraction in model construction. Eventually modeling, and verification of a multi-valued flip-flop is studied in order to demonstrate capabilities of the proposed models.

In this paper, performance of grid computing environment is studied in the presence of failure-repair of the resources. To achieve this, in the first step, each of the grid resource is individually modeled using Stochastic Reward Nets (SRNs), and mean response time of the resource for grid tasks is computed as a performance measure. In individual models, three different scheduling schemes called random selection, non-preemptive priority, and preemptive priority are considered to simultaneously schedule local and grid tasks to the processors of a single resource. In the next step, single resource models are combined to shape an entire grid environment. Since the number of the resources in a large-scale grid environment is more than can be handled using such a monolithic SRN, two approximate SRN models using folding and fixed-point techniques are proposed to evaluate the performance of the whole grid environment. Brouwer's fixed-point theorem is used to theoretically prove the existence of a solution to the fixed-point approximate model. Numerical results indicate an improvement of several orders of magnitude in the model state space reduction without a significant loss of accuracy.

Data aggregation is a key, yet time-consuming functionality introduced to conserve energy in wireless sensor networks (WSNs). In this paper, to minimize time latency, we focus on aggregation scheduling problem and propose an efficient distributed algorithm that generates a collision-free schedule with the least number of time slots. In contrast to others, our approach named FAST mainly contributes to both tree construction, where the former studies employ Connected 2-hop Dominating Sets, and aggregation scheduling that was previously addressed through the Competitor Sets computation. We prove that the latency of FAST under the protocol interference model is upper-bounded by 12R + Δ - 2, where R is the network radius and Δ is the maximum node degree in the communication graph of the original network. Both the theoretical analysis and simulation results show that FAST outperforms the state-of-the-art aggregation scheduling algorithms.

Performance evaluation of mobile networks needs accurate simulation set up including realistic characteristics. The most important issue in mobile networks' simulation is the mobility of the nodes. Since mobile nodes usually are carried by humans, thus, nodes mobility should be modelized as human movement. To the best of our knowledge, none of the existing mobility models have the ability to modelize all the human movement characteristics. In this paper, a new mobility model has been proposed based on the human mobility data collected for more than 6000 hours. The new model captures human mobility properties by introducing hotspot zones, using a graph of hotspot zones as the input area map, dividing day time to some periods and modeling various speeds in different times and spaces. Moreover, it models some other important human mobility features that had been modeled in previous works. To evaluate the performance of the proposed model, it is compared with real collected data.

We consider a firm real-time system with a single processor working in two power modes depending on whether it is idle or executing a job. The system is equipped with dynamic thermal management through a cooling subsystem which can switch between two cooling modes. Real-time jobs which arrive to the system have stochastic properties and are prone to soft errors. A successful job is one that enters the system and completes its execution with no timing or soft error. Appropriateness of the system is evaluated based on its performance, temperature behavior, reliability, and energy consumption. It is noteworthy that these criteria have mutual interactions to each other: the stochastic nature of the system affects the success ratio of jobs beside the system dynamic power, the leakage as well as dynamic power impacts the processor temperature, this temperature affects the leakage power, the cooling subsystem power, and the soft error rate, which the latter in turn impacts the system reliability and the success ratio of jobs. This paper proposes an analytical evaluation method with a Markovian view to the system which considers these reciprocal effects. A number of simulation experiments are carried out to validate the accuracy of the proposed method.

Availability of the service delivered by cloud providers is one of the most important QoS factors of the service level agreements between providers and customers. Since current Infrastructure-as-a-Service providers use virtualization technology to manage data centers, virtual data centers (VDCs) have become a popular infrastructure for cloud computing. In order to study the service availability, a stochastic activity network (SAN) model is presented in this paper. The proposed SAN model can be appropriately used to investigate the impact of different characteristics and policies on service availability of VDCs.

Mobile ad hoc networks (MANETs) have been turned into very attractive area of research in the duration of recent years, whereas security is the most challenging point that they undergo. Cryptography is an essential solution for providing security within MANETs. However, storing all keys in every node, if practically possible, is inefficient in large scale MANETs due to some limitations such as memory or process capability. This paper extends our previous idea which was a novel probabilistic key management algorithm that stores only a few randomly chosen keys instead of all ones. In this paper, several different scenarios are proposed for key selection in which they are more practical, and then, the impact of each scenario on the performance and security metrics is analyzed. Results show that the proposed scenarios can reduce the path length in addition to keeping the network highly connected.

Data aggregation is an effective technique which is introduced to conserve energy by reducing packet transmissions in wireless sensor networks (WSNs). In addition, it is possible to consume less energy by using the spatial correlation and redundancy of data in dense networks to form clusters of nodes sensing similar values and, in turn, transmit one data packet per cluster. In this paper, we propose a Data-Aware Clustering and Aggregation scheme (DACA) to manage the energy constraint in a query-driven WSN. The DACA selects cluster head nodes by forming a new factor as a function of three parameters including the residual energy, the data value, and the number of neighbors at each node. Moreover, it exploits a cluster merging method to overcome the problem of the previous studies in which all sensor nodes become cluster heads over time, so it prolongs the network lifetime. Extensive simulations in NS-2 verify the superiority of our approach.

Data aggregation is an efficient method to conserve energy by reducing packet transmissions in WSNs. However, providing end-to-end data reliability is a major challenge when the network uses data aggregation. In this case, a packet loss can miss a complete subtree of values, thus greatly affecting the final results. Data transmission in multiple paths can tolerate this problem, but it may incur some computation errors for duplicate-sensitive aggregates. In this paper, we propose a Flexible Overlay Multi-path data Aggregation protocol (FOMA) which uses the available path redundancy to deliver a correct aggregate result to the sink with high reliability in an energy-efficient manner. It aggregates data in two layers, routing layer and data aggregation layer, while eliminating the computation errors by using a signature-based method. We implement FOMA in TinyOs 2.x and test it by the TOSSIM simulator. The results reveal that the proposed algorithm outperforms other existing ones in terms of energy consumption and data accuracy.

Network Coding (NC) is an emerging technique that helps wireless networks to have higher throughput and better energy efficiency. In this paper, a novel network coding-aware routing (S-NC) which uses NC to improve reliability and robustness in unreliable WSNs is proposed. It is based on a structure-free routing algorithm as the underlying routing engine which employs neighbor queue length to increase coding opportunity; while exploiting a spatial coding method to control the amount of redundancy. To the best of our knowledge, this is the first study on the topic of network coding-aware routing in WSNs. Simulation results in TOSSIM demonstrate that S-NC significantly improves the performance in terms of reliability, end-to-end delay, and energy consumption in the network.

The main source of energy consumption in the current MAC protocols for wireless sensor networks is idle listening. To mitigate this problem, duty cycling is used. However, it increases data delivery latency. In this paper, we propose an Interference-aware duty-cycle MAC (IMAC) protocol for wireless sensor networks that uses cross-layer information to reserve multiple paths for each source and send data packets along them efficiently. IMAC also handles the existing interference between these paths such that data packets can be delivered in the minimum required number of cycles. Simulation results in ns-2 show that the proposed algorithm has an average reduction of 49% in data delivery latency compared to a current solution called RMAC.

Data aggregation is an effective technique which is introduced to save energy by reducing packet transmissions in WSNs. However, it extends the delay at the intermediate nodes, so it can complicate the handling of delay-constrained data in event-critical applications. Besides, the structure-based aggregation as the dominant data gathering approach in WSNs suffers from high maintenance overhead in dynamic scenarios for event-based applications. In this paper, to make aggregation more efficient, we design a novel structure-free Real-time Data Aggregation protocol, RDAG, using a Real-time Data-aware Routing policy and a Judiciously Waiting policy for spatial and temporal convergence of packets. Extensive simulations in NS-2 verify the superiority of RDAG in WSNs.

We consider a single-processor firm real-time (FRT) system with exponential interarrival and execution times for jobs with relative deadlines following a general distribution. The scheduling policy of the system is first-come first-served (FCFS) and the capacity of the system is arbitrary. This system is subject to an arbitrary-shaped time/utility function (TUF), which determines the accrued utility of each job according to its completion time. It is considered that the system power consumption at different working states is predetermined for each processor speed. We have proposed an exact analytical method for the calculation of specific performance and power-related measures of the system. The resulting analytical formulations for the performance measures are functions of the processor speed and system capacity. These measures are optimized through appropriate selections of the speed using derivatives and the capacity employing numerical search methods. Some experimental results are presented for different unimodal TUFs in systems with deterministic and exponential relative deadlines. For the latter distribution, the results are compared against similar results obtained through simulation for the nonpreemptive earliest-deadline-first (NP-EDF) scheduling policy. The comparisons show that FCFS is superior to NP-EDF for some measures and TUFs.

Security in mobile ad hoc networks (MANETs) is an active research topic. Bulks of prior work focused on key management and secure routing without addressing an important pre-requisite: network access control, the problem of how securely extend the network. In this paper, we present INAC, an identity-based network access control scheme for MANETs. In INAC, each node in the network must have an identity-based membership token in order to take part in network activities. Membership tokens have special formats, which not only guarantee security of non-compromised nodes, but also enable that nodes obtain identity-based membership tokens based on their trustworthiness. Through simulations we verify the feasibility of our design in the single authority MANETs.

We provide an equational theory for Restricted Broadcast Process Theory to reason about ad hoc networks. We exploit an extended algebra called Computed Network Theory to axiomatize restricted broadcast. It allows one to define the behavior of an ad hoc network with respect to the underlying topologies. We give a sound and ground-complete axiomatization for CNT terms with finite-state behavior, modulo what we call rooted branching computed network bisimilarity.

One of the main properties of today's distributed and parallel systems, such as mobile ad-hoc networks and grids, is their heterogeneity in the available resources. Further, many applications of such systems are subject to Time/Utility Function (TUF) time constraints for jobs, unavoidable variability in job characteristics and arrivals, and statistical assurance requirements on timeliness behaviors. In this paper, we propose an exact analytical solution for performance evaluation of dynamic policies used for routing of TUF-constrained Firm Real-Time (FRT) jobs among parallel single-processor queues with arbitrary processing rates and capacities. The analytical method can be used for the evaluation of the compliance of some important statistical assurance requirements. Furthermore, we present a utility-aware dynamic routing policy to improve the expected accrued utility of the parallel system. The policy called Maximum Expected Utility (MEU) behaves based on the information gathered from the analytical solution. MEU is compared with some well-known Dynamic Routing (DR) policies for different TUF shapes and both cases of homogeneous and heterogeneous processors of a two-queue system. The comparisons show the efficiency of MEU for the former case and its good behavior in most situations for the latter case.

The manner of organizing the sensors in the wireless sensor network for increasing the capability and optimized using of the sensors is of great importance. Hence considering coverage parameter in every Wireless Sensor Network (WSN) is extremely essential and critical. The matter of overlapping covered area by sensors in 2D space had been considered until now. This paper is suggested a pattern in which no more are the sensors located at the same surface, but using the 3D geometrical figures like cube, pyramid and etc, in which the sensors were spreading about the different surfaces. Locating the sensors on the different surfaces can be useful under conditions where the space is not in same surface. The surface coverage parameter does not count using the 3D geometrical figures rather than covered volume. This paper is considered this parameter and the method of obtaining it.

Few works has been focused on the problem of joint distributed data compression and network coding. In this paper we give some examples showing the advantage of broadcast nature of wireless environment as a basis for joint codes design. Also we show that joint coding is possible in the case of multiple unicasts. The idea of this paper can be exploited in an opportunistic manner. Actually, the foundation of our idea is nothing but combining opportunistic network coding (COPE) and distributed source coding using syndromes (DISCUS) for wireless applications.

Topology control algorithms in mobile ad-hoc networks aim to reduce the power consumption while keeping the topology connected. These algorithms can preserve network resources and increase network capacity. However, few efforts have focused on the issue of topology control in presence of node mobility. One of the notable mobility aware topology control protocols is the ldquomobility aware distributed topology control protocolrdquo. The main drawback of this protocol is on its mobility prediction method. This prediction method assumes linear movements and is unable to cope with sudden changes in the mobile node movements. In this paper, we propose a pattern matching based mobility prediction method in which every mobile node predicts its future location through finding similar patterns in its history of movements. Simulation results show significant improvements in terms of prediction accuracy and power consumption compared to the other known algorithms.

In new applications of mobile ad hoc networks (MANETs), nodes may decide not to cooperate in routing protocols in order to save their limited resources while still using the network to relay their own traffic. Exhibiting such a selfish behavior by even a few nodes may degrade network performance and other cooperating nodes may find themselves unfairly loaded. To cope with such a situation, we propose a stable path, low overhead, truthful, and cost efficient (SLTC) routing protocol which stimulates nodes to cooperate and act truthfully by utilizing the game theoretic notion of mechanism design. To the best of our knowledge, SLTC is the first protocol attaining the message complexity of O(nd), where n is the number of nodes, and d is the network diameter. In addition, SLTC considers stability of the paths in order to deal with the mobility of the nodes in a better way. We evaluated SLTC through simulation in terms of packet delivery ratio, end-to-end delay, traffic overhead and energy consumption. SLTC can achieve more than 80% packet delivery ratio. Compared to ad hoc-VCG which is one of the best known methods in this area, the packet delivery ratio is increased by a factor of 9 along with a reduction in the end-to-end delay, the traffic overhead, and the energy consumption respectively by a factor of 22, 7, and 3.

Constraint automata as acceptors of timed data streams are the semantic models of component connectors specified in the language of Reo. In this paper, we investigate the augmentation of the theory of constraint automata by live- ness and fairness requirements. We define the notion of liveness for constraint automata as a set of infinite runs and show that our definitions of weak and strong fairness requirements, as we expect, satisfy the liveness requirements. It is shown that live or fair constraint automata can be composed using extended versions of the join operator for ordinary constraint automata such that, the resulted automaton itself be live or fair, respectively. Also, we present a linear temporal logic interpreted over infinite strings of transitions of constraint automata as a specification language for their properties. This temporal logic can be used as the specification language in the field of model checking. We show that our defined fairness conditions can be expressed not only by sets of computations but also by temporal formulas in the proposed linear temporal logic of steps.

We present a process algebra for modeling and reasoning about Mobile Ad hoc Networks (MANETs) and their protocols. In our algebra we model the essential modeling concepts of ad hoc networks, i.e. local broadcast, connectivity of nodes and connectivity changes. Connectivity and connectivity changes are modeled implicitly in the semantics, which results in a more compact state space. Our connectivity model supports unidirectional links. A key feature of our algebra is eliminating connectivity information from the specification of a network, and transferring its complexity to the semantics. We give a formal operational semantics for our process algebra, and define equivalence relations on protocols and networks. We show how our algebra can be applied to prove correctness of an adhoc routing protocol.

A component-based computing system consists of two main parts: a set of components and a coordination subsystem. Reo is an exogenous coordination language for compositional construction of the coordination subsystem. Constraint automaton has been defined as the operational semantics of Reo. The main goal of this paper is to prepare a model checking method for verifying linear time temporal properties of component-based systems whose coordinating subsystems are modeled by Reo and components are modeled by labeled transition systems. For this purpose, we introduce modified definitions of constraint automata and their composition operators by which, every constraint automaton can be considered as a labeled transition system and each labeled transition system can be translated into a constraint automaton. We show that failure-based equivalences CFFD and NDFD are congruences with respect to the composition operators of constraint automata. Also we present a method for compositional model checking of component-based systems using these equivalences for reducing the sizes of constraint automata models.

Reo is an exogenous coordination language for compositional construction of the coordinating subsystems of component-based softwares. Constraint automaton has been proposed as the operational semantics of Reo networks. The main goal of this work is to prepare a model checking based verification environment for component-based systems, whose component connectors are modeled by Reo networks and constraint automata. We use the methods of compositional reduction and abstraction in model checking of component-based systems and their component connectors modeled by Reo.

Cooperation of nodes for routing and packet forwarding is inevitable in a mobile ad hoc network. Selfishness in such networks is a significant challenge and can cause network performance to noticeably degrade. In this paper, we propose some new selfishness models elicited from psychological behavior of human beings. We also evaluate performance of MANET in the presence of different percentages of selfish nodes that act based on our selfishness models. Results show that energy-based selfishness is a serious problem that could affect performance depends on mobility of nodes, density of network, and time of simulation. This kind of selfishness needs a comprehensive mechanism to cope with and we have planned to publish such mechanism in early future.

We have recently introduced a high-level extension for stochastic activity networks (SANs) called coloured stochastic activity networks (CSANs). CSANs have several distinguishing properties, which make them quite appropriate for modeling and evaluation of software performance and dependability. CSANs have introduced a construct called coloured place for data manipulation. A coloured place holds a list of tokens of a userdefined token type. CSAN models can be evaluated by state space analysis techniques or discrete-event simulation. However, their state spaces will become very large, even for a small CSAN model. For efficient evaluation of these models by state space analysis methods, we will introduce measure-adaptive state space analysis process in this paper. Based on this method, it is possible to construct high-level CSAN models. However, for efficient evaluation, it is possible to generate and analyze a reduced state space based on user-specified performance or dependability measures.

Stochastic activity networks (SANs) are a stochastic generalization of Petri nets. SAN models have been used to evaluate a wide range of systems and are supported by several modeling tools. We have introduced object stochastic activity networks (OSANs) to overcome some restrictions of these models. OSANs integrate the concepts of object-orientation into SAN models. Elements of OSANs and their submodels are defined as classes. OSANs are more appropriate that most other objectoriented or high-level extensions of Petri nets for application on software systems. In this paper, we will present the definitions, behavior and an example of OSAN models. The objectorientation of OSANs and the flexibility of having functions for activities, make these models more appropriate than other extensions of Petri nets for modeling and evaluation of software systems.

This paper introduces an analytical method for approximating the performance of a soft real-time system modeled by a single-server queue. The service discipline in the queue is earliest-deadline-first (EDF), which is an optimal scheduling policy. Real-time jobs with exponentially distributed deadlines arrive according to a Poisson process. All jobs have deadlines until the end of service and are served non-preemptively. Occurrences of transient faults in the server are also taken into account. The important performance measure to calculate is the loss probability due to deadline misses and/or transient faults. The system is approximated by a Markovian model in the long run. A key parameter, namely, the loss rate when there are n jobs in the system is used in the model, which is estimated by partitioning the system into two virtual subsystems. The resulting model can then be solved analytically using standard Markovian solution techniques. Comparing numerical and simulation results, we find that the existing errors are relatively small.

This paper introduces an analytical method for approximating the fraction of jobs that miss their deadlines in a real-time system when earliest-deadline-first scheduling policy (EDF) is used. In the system, jobs either all have deadlines until the beginning of service or deadlines until the end of service. In the former case, EDF is known to be optimal and, in the latter case, it is optimal if preemption is allowed. In both cases, the system is modeled by an M/M/1/EDF+M queue, i.e., a single server queue with Poisson arrival, and service times and customer impatience, which are exponentially distributed. The optimality property of EDF is used for the estimation of a key parameter, /spl gamma//sub n/, which is the loss rate when there are n customers in the system. The estimation is possible by finding an upper bound and a lower bound for /spl gamma//sub n/ and linearly combining these two bounds. The resulting Markov chains are then easy to solve numerically. Comparing numerical and simulation results, we find that the existing errors are relatively small.