Abstract:This paper proposes a strategy driven approach to modeling and analyzing reliable embedded systems according to their characteristics. Petri nets are used as the formal description language for embedded systems, which formally specify embedded system’s elements such as equipment, computing, physical interaction, components, and communication processes. This research studies reliability assurance strategies for embedded systems by analyzing various fault types and their characteristics. An aspect-oriented method is used to extract reliability related concerns. A complete embedded system model is obtained by constructing reliability aspect models and then applying the weaving mechanism to dynamically combining components and aspects. The effectiveness of reliability assurance strategies is analyzed based on the theories of Petri nets. A case study demonstrates that the approach can simplify design and modeling processes of embedded systems and contribute to improving its quality.

Abstract:Points-to analysis mainly aims to attain the runtime points-to sets of program variables. This paper describes the design and implementation of an efficient Andersen-style, context-sensitive points-to analysis for Java code. The implementation supports language features such as inheritance, polymorphism, and field objects. The study tracks the fields of individual objects separately and makes the algorithm in field-sensitive style for aggregate objects. To improve the efficiency and scalability of the algorithm, this study employs two kinds of optimizations, nodes topology construction with concomitance on-line cycle detection and cycle elimination. Experiment results show that this algorithm can be used to compute precise points-to sets for large-scale Java programs.

Abstract:Most research on test case generation from Object-Z specification focuses on theory. There is almost no tool to support generating test cases automatically. The Object-Z is a mathematics and logic based formal specification language. It uses schema composition and abbreviation format, which brings difficulty for extracting semantics and then generating test cases from specification automatically. This paper provides a solution in extracting semantics and generating test cases from Object-Z specification by unfolding the schema definition and improving its syntax in Object-Z. The process has three steps including parsing Object-Z language, extracting semantics, and generating test cases automatically.

Abstract:This paper defines the notion of cycle symmetry, which extends the traditional automorphism-based symmetry and enables application of symmetry reduction to a broader class of asymmetric systems. The study also shows that both cycle symmetry group and cycle symmetry generated group can be used to produce a quotient structure that is bisimilar to the original model. Furthermore, the extension of symmetry reduction over three-valued models is investigated. The quotient structure of a three-valued model is defined and induced by a permutation group and extends to both automorphism-based symmetry reduction and cycle symmetry reduction to three-valued models. Finally, the study analyzes the relationship between symmetry reduction of a three-valued model and classical models induced by it. Both approaches can lead to the same reduced quotient structure of the original model.

Abstract:This paper proposes an approach for scenario-driven Web services behavior manipulation. First, the study uses UML sequence diagrams as the scenario-based specification to describe user’s requirement on the behavior of the service and construct BPEL-Petri nets model (BPN model for short) to represent the service behavior based on its BPEL specification. Second, the service behavior is analyzed based on paths of the BPN model by utilizing the notion of concurrent transitions. The set of behavior with occurrence of the scenario depicted by the UML Sequence Diagram is obtained by traversing the BPN model. Finally, by using the result of behavior analysis, the study constructs the manipulator services to extract or filter out the behavior at run-time by listening to, checking, and filtering the messages exchanged between the user and the target service. In addition, the study has developed a prototype tool called BASIS to facilitate the behavior manipulation and conduct a case study to illustrate the feasibility of this approach.

Abstract:This paper presents a time Petri net (TPN) model with mixed semantics that efficiently addresses the schedulability analysis problem of the existing semantics models. The proposed model associates each firable transition with a mandatory firing point that is set to the least upper bound of the transition and its non-conflicting transitions. This treatment not only eliminates the effect of conflicting transitions on the transition friability and extends the scheduling scope of the TPN model, but also ensures the time limit of the task scheduling. To determine the expressiveness of the mixed model, the study proves that the mixed semantics model has the power of Turing machines and its marking reachability problem is undecidable. The timed expressiveness of three semantics models with respect to timed language acceptance is also compared. A state class approach is then proposed for the scheduling analysis of the mixed model. Finally, a flexible manufacturing system is used as an example to compare the scheduling ability of three semantics models.

Abstract:This paper proposes to represent software architectures with constraint hypergraphs, depict pre-and post-assertions of dynamic evolution of software architectures with left and right application conditions, and model the dynamic evolution process of software architectures with conditional hypergraph grammars. Firstly, how to construct conditional hypergraph grammars and how to apply to dynamic evolution of software architectures through a case study are discussed. Secondly, the consistency condition definition and the corresponding consistency decision method of dynamic evolution of software architectures are given out on this basis. Finally, an experiment is desisgned over analysis for dynamic evolution of software architectures to show the effectiveness of the proposed method.

Abstract:Nowadays, instead of only verifying systems at the model level, current state-of-the-art verification techniques tend to focus on real code and real system’s execution. Runtime verification checks the system’s execution and tries to bridge the gap between formal verification techniques and real systems. However, this brings about some problems which usually do not appear in model-level verification. This paper analyses the problem in runtime verification. It defines two kinds of conflicts and lists their corresponding detection algorithms. These algorithms are implemented based on an open source runtime verification tool and some real cases are examined. The results demonstrate the effectiveness of the proposed method.

Abstract:Distributed systems are complicated real-time systems, which have been used in many safety-critical domains. In order to ensure the real-time constraints over the tasks running on these systems, the traditional schedulability analysis techniques, based on worst-case response time analysis, usually consider the worst case which could never occur in real world applications, and therefore the obtained results are pessimistic. The model checking technique based on automata theory could exhaustively search the whole system state space and return precise results. By using formal methods to analyze the schedulability of tasks on distributed systems, this paper presents the formal task model on distributed systems. It uses action automata and environment automata to model the task execution semantics and the external event arrival patterns respectively. It also translates the schedulability analysis to the reachability analysis of the locations in automata network, and proves the decidability of schedulability under certain scheduling policies with attached conditions and scope. Based on these conclusions, the formal check model implements a schedulability check tool, SCT (schedulability checking tool), and compares it with other techniques and tools on accurateness and performance. The comparisons show that SCT always provides the most accurate results but with the longest execution time.

Abstract:This paper focuses on a reliability model of embedded system architecture using AADL (architecture analysis and design language). It performs transformation from AADL reliability model to GSPN (general stochastic Petri net) model and assesses AADL architecture reliability computation model by the means of GSPN theory. To support the reliability analysis and assessment automatically, this paper designs and implements an AADL reliability assessment model tool, ARAM (AADL reliability assessment model tool), with formal methods. It is integrated into OSATE (the open source AADL tool environment) and uses PIPE2 (platform independent Petri net editor 2) to carry out the reliability assessment of GSPN model. Meanwhile, this paper also presents a case study on the reliability analysis and assessment of avionics flight control system to demonstrate the performance of ARAM.

Abstract:This work presents timed automata as a natural tool for solving Chinese postman problems on time varying network. This study shows that the optimal Chinese tour can be equivalently casted as the shortest run in this automaton system, which can be obtained efficiently by solving a series of decision problems for reachability. A composition strategy is then proposed to adapt to the current model, such that the number of timed automaton is reduced from O(|A|+|A_R|+1) to O(1). Computational results show that the improved model can solve small-sized instances optimally, and that it can obtain a better gap between the lower bound and upper bound than the ones obtained by the cutting plane and column generation algorithms.

Abstract:The rapid increase of P2P traffic worsens the congestion of network while P2P traffic identification becomes the basic technical support for network management. The types of P2P traffic and main challenges of traffic identification are introduced first. Next, the main techniques and research progresses of P2P traffic identification are summarized. Finally, the future trend is put forward.

Abstract:Attribute-Based encryption (ABE) scheme takes attributes as the public key and associates the ciphertext and user’s secret key with attributes, so that it can support expressive access control policies. This dramatically reduces the cost of network bandwidth and sending node’s operation in fine-grained access control of data sharing. Therefore, ABE has a broad prospect of application in the area of fine-grained access control. After analyzing the basic ABE system and its two variants, Key-Policy ABE (KP-ABE) and Ciphertext-Policy ABE (CP-ABE), this study elaborates the research problems relating to ABE systems, including access structure design for CP-ABE, attribute key revocation, key abuse and multi-authorities ABE with an extensive comparison of their functionality and performance. Finally, this study discusses the need-to-be solved problems and main research directions in ABE.

Abstract:Certificateless public key cryptography (CL-PKC for short) is a new type of public key cryptography, which is developed on the foundation of identity based cryptography (ID-PKC for short). CL-PKC elimilates the key escrow problem and the need for public key certificate. These two advantages are what makes it attractive to the research community and industrial world form the beginning of its birth. It has been a very active research hot topic in the field of cryptology and information security. In about seven years, the study of CL-PKC has advanced step by step, making its theories and techniques more and more enriching. This paper revisits, analyzes, compares, and briefly reviews some of the main results. Furthermore, this study discusses some existing problems in this research field that deserve further investigation.

Abstract:Mobility model is a crucial feature to differentiate ad hoc networks from other networks. The evaluation of dynamic network properties caused by mobility model is the basic problem for research on protocol simulation and related technologies, such as topology control and network performance measurement, in ad hoc networks. In this paper, a model-based description of ad hoc networks is improved to avoid the drawbacks in describing the corresponding space-time dynamic properties. Then a universal evaluation method with measureable space-time dynamic properties is presented. The dynamic properties of several mobility models are studied by constructing the space distribution of the nodes and designing the models for analyzing the topological space-time dynamic properties. Furthermore, a novel mobility model based on circular curve movement is proposed to improve the flexibility and the capability to describe realistic scenarios with curve movement. Simulation with NS2 shows the presented method can effectively evaluate the characteristics of the existing mobility models. The numerical results also show that the proposed mobility model has good dynamic properties in comparison with the existing mobility models.

Abstract:Paterson, et al. have studied identity-based signature scheme based on Waters’ signature scheme in a standard model, which has proved to have a security reduction to CDHP assumption, but has low computational efficiency. Although Li-Jiang, et al. improves Paterson’s scheme, Li-Jiang’s scheme has low online computational efficiency. This paper shows a more efficient identity-based signature scheme based on Paterson’s scheme in standard model. The new scheme improves computational efficiency by changing multiplicative operation to addition operation and pre-computing bilinear pairing operation. The scheme comparing with Paterson’s scheme decreases the number of multiplicative operation and the number of bilinear pairing operation of verifier. The scheme comparing with Li-Jiang’s scheme decreases the on-line computation of signer and verifier and the output parameters of system. Also, the scheme has proved to have a security reduction to CDHP assumption and the existential unforgeability under an adaptive chosen message attack. Comparing with other identity-based signature schemes in standard model, the new scheme is more efficient.

Abstract:This paper aims at finding an efficient actor nodes deployment strategy under a real-time constraint. Because of the random distribution of WASNs, WSANs’ real-time coverage problem is actually NP-hard. There are no effective distributed algorithms in previous research that can solve the problem. Thus, the Voronoi-Based Maximize Real-Time deployment strategy is proposed to solve this problem, based on Voronoi diagram, Through simulated experiments, the results show that the distributed protocol is more effective than present deployment protocols in terms of real-time performance, convergence time, and energy consumption.

Abstract:In order to gain insight on the topology characteristics of P2P IPTV systems and their online user behavior characteristics, This paper develop and deploys a multiprotocol P2P IPTV network crawler, called TVCrawler, which enables users to launch an in-depth measurement and comparative research for several well-known P2P IPTV systems, including PPLive, PPStream, and UUSee. This paper presents results from experiments and research efforts on these large-scale P2P IPTV overlay graphs. Major findings include 1) more than 50% of online users are unreachable because they lie behind NAT or firewall; 2) fluctuation range of churn increases with the increase of the population of channel, and there exists a power-law upper bound for fluctuation range of churn; 3) session length of peer follows a stretched exponential distribution; 4) while the in-degree of PPLive follows the power-law distribution with exponential cutoffs, the in-degree of PPStream appears to have multiple separate power-law regimes with different exponents, and the in-degree of UUSee approaches Weibull distribution. 5) All of measured P2P IPTV overlay graphs appear as a disassortative mixing; 6) small-world networks are ubiquitous in measured P2P IPTV systems. 7) the PPLive overlay graph is clustering, but the others are not; 8) all of measured P2P IPTV overlay graphs have robustness similar to that of a power-law graph, but PPLive is more vulnerable to malicious attacks and more robust to random failures than the other. These research and findings Will be good for designing and optimizing of P2P IPTV protocols, but also for monitoring, directing, and dominating the P2P IPTV system.

Abstract:After researching the anti-monitoring problem on mobile objects in the heterogeneous sensory field, a new Exposure model is proposed, which can be used to estimate the approximate risk of a mobile object moving along a path to traverse the sensory field deployed with anisotropic sensor nodes. Based on the newly proposed Exposure model, a novel decision algorithm for path selection is designed by combing the Anisotropic Voronoi Tessellation schemes, which guarantee that the mobile object can select a suitable path with a minimal approximately risk of traveling across the anisotropic sensory field. Theoretical analyses and simulation results show that the new algorithm has a good anti-monitoring performance and requires only that the mobile object should know the local information in its detection radius, so it is distributed and practical.

Abstract:Network vulnerability analysis is one of the irreplaceable foundations of network security. Host- centric methods of vulnerability analysis can generate an attack graph in polynomial time, whereas the inherent link uncertainty has not been of a concern. An uncertain-graph based method for network vulnerability analysis is proposed in this paper, which uses link uncertainties to describe link states accurately. In this way, finding an optimal exploit chain becomes feasible. An algorithm for generating an uncertain attack graph (UAG) is proposed, whose running time is O(n⁴). Next, a heuristic algorithm to that can generate the optimal exploit chain, on the basis of UAG, is proposed, which runs in O(n³) time. Experimental results show that this method can generate UAG in an acceptable amount time and find a vulnerability exploit chain with a maximum attack benefit.