Abstract:

Abstract:Bisimilarity plays an important role in the analysis and verification of concurrent systems. In this paper, an optimization of the quasi-local algorithm of Du and Deng is proposed to make it applicable for general labeled transition systems. Both the optimized algorithm and the local algorithm of Fernandez and Mounier are implemented in Java, and experiment using the VLTS benchmark suite shows the former outperforms the latter in most cases. The algorithms are also modified to check similarity. Finally, a procedure for transforming labeled transition systems is implemented to facilitate checking weak bisimilarity.

Abstract:This paper proposes a framework facilitating the automatic analysis on inductive properties for recursive data structures. This work has three main parts. First, the analysis of heap-manipulating programs is simplified by classifying inductive properties of recursive data structures into two classifications, each of them is handled with observed patterns. Second, a slicing and splicing technique, in which data structures are first sliced into several parts and these parts are further spliced into new data structures, is proposed to track and specify how data structures are manipulated by programs. The key idea of this technique is to preserve the properties of original data structures, which can be used by further analysis. Third, a calling context sensitive interprocedural analysis is presented for computing program summaries. A case study and experimental results show that the proposed analysis framework can effectively analyze inductive properties for recursive data structures, resulting in assertions that are helpful in program verification.

Abstract:This paper proposes a method of using abstract interpretation for discovering properties about array contents in programs which manipulate one-dimensional or multi-dimensional arrays by sequential traversal. The method directly treats invariant properties (including interval universally quantified formulas and atomic formulas) set as abstract domains. It synthesizes invariants by "iterating forward" analysis. This method is sound and converges in finite time. The paper demonstrates the flexibility of the method by some examples. The method has been implemented in a prototype tool. The experiments applying the tool on a variety of array programs (including array-examples benchmark of competition on software verification) demonstrate the feasibility and effectiveness of the approach.

Abstract:Petri nets is a fundamental model in the area of formal verification. It is popular in both theoretical study and application. For the analysis of algorithmic properties of Petri nets, they are often equivalently viewed as vector addition systems. This survey gives a comprehensive review of the recent achievements in this area. First, formal definitions of the vector addition systems and their key verification problems are provided with emphasis on the discussion about reachability problem, including the latest results and the main proof techniques. Then the development on the case where the dimension is a constant number rather than a variable is summarized along with some key theorems which are fundamental to the current complexity results. Furthermore, as some important variants of vector addition systems have been proposed in recent years, a brief introduction is given to the motivation and definitions of some of the most representative ones, and the latest results on verification relating to these models. In addition, possible future work are highlighted at the end of each section.

Abstract:Model-checking, an automatic verification methodology, has been applied to verify multi-agent systems. Alternating-time temporal logic (ATL), a property specification language for multi-agent systems was also investigated. According to whether agents are able to observe the whole information of the system and whether agents are able to record the history information, agents' strategies are divided into four types. These strategy abilities are defined in semantic level of ATL, as well as other logics. However, under perfect information and perfect recall setting, all agents have the same strategy ability. Under imperfect information and/or imperfect recall setting, only agents appeared in coalition modalities <<A>>φ and [[A]]φ have imperfect information and/or imperfect recall strategies, while other agents not in A still have perfect information and perfect recall strategies. When coalition modalities are nested, same agents may have different strategy abilities to fulfill different sub formulas, which results in inconsistency. On the other hand, in practice, agents' strategy abilities are usually decided by the multi-agent systems rather than the specifications, and different agents may own different strategy abilities. This kind of multi-agent systems is called heterogeneous mutli-agent systems. To overcome these problems, this paper proposes a new formal model, called typed interpreted systems which are able to define agent's strategy abilities at syntax level. Typed interpreted systems extend interpreted systems by associating each agent with a strategy type denoting the agent's strategy ability, therefore are able to model heterogeneous mutli-agent systems. The paper investigates the semantics of ATL on this new model and proposes an EXPTIME model-checking algorithm. The model-checking algorithm is implemented in a prototype tool ShTMC.

Abstract:CCSL (abbreviated for clock constraint specification language) is a formal language for specifying the constraints on the occurrences of events in real-time and embedded systems. CCSL is a companion language of MARTE (abbreviated for modeling and analysis of real-time and embedded systems), a UML profile which provides support for specification, design, and verification/validation stages for model-driven development of real time and embedded Systems. Given a set of CCSL constraints, it is necessary to check if there exist schedules that satisfy all the constraints and if all the behaviors that conforming to the constraints will never incur deadlock of systems. Many approaches have been proposed based on state transition system, timed automata, etc. However, most of the existing approaches have some drawbacks, such as being ad hoc to specific formal analysis, and being suited to only subsets of CCSL constraints or inefficient. In this paper, a unified and efficient SMT-based approach to formal analysis of CCSL is proposed. This approach is unified in that it can be applied to various analysis such as validity proving, trace analysis, deadlock detection and LTL model checking. A prototype tool for the new approach is implemented to support the four types of formal analysis, utilizing the state-of-the-art SMT solvers such as Z3 and CVC4. With efficient SMT solvers, verification can be completed in a reasonable time, as demonstrated by the experimental results in the case studies.

Abstract:The modeling, simulation and verification language (MSVL) is a temporal logic programming language as well as an executable subset of projection temporal logic (PTL). MSVL and PTL are used for modeling and verifying properties of concurrent systems. However, MSVL lacks a mechanism of communication based on message passing which is essential for modeling and verifying concurrent distributed systems. This paper shows how to develop and implement a suitable mechanism in MSVL to model and verify concurrent distributed systems. First, channel structure is defined while communication statements and process structures are formalized. Then, the implementation mechanisms for those communication statements are presented. Finally, a modeling and verification example involving an electronic contract signing protocol is provided to illustrate how the message passing works in MSVL.

Abstract:Runtime verification is an important method for improving software reliability of pervasive computing applications. Some properties of these applications consider both temporal and spatial relationships. Such spatio-temporal properties bring some specific challenges for runtime verification. On one hand, traditional temporal logic cannot describe spatial properties. On the other hand, while ambient logic is suitable for spatial properties, it does not properly support the description of temporal properties in finite traces, especially when the truth values cannot be decided. In order to support the runtime verification of spatio-temporal properties for pervasive computing applications, this paper firstly imports 3-valued semantics and proposes AL₃ (3-valued ambient logic). On the basis of AL₃, it designs and implements an algorithm for properties checking and a runtime monitor. Moreover, the paper uses a case study and a performance measurement to clarify the usability and feasibility of the proposed approach.

Abstract:Alternating projection temporal logic (APTL) has a concise syntax with strong expressive power. It is able to express not only properties specified in classical temporal logic LTL, but also interval related sequential and periodical properties, as well as game related properties of open systems and multi-agent systems. To verify whether a system satisfies an APTL formula, the satisfiability of the APTL formula should be checked. In this paper, based on the method for checking satisfiability of an arbitrary APTL formula provided, a supporting tool APTL2BCG has been developed. The details of implementation are given as follows. Firstly, LNFG of P is constructed according to the normal form of the formula P. Then, the LNFG is transformed to a generalized alternating Büchi automaton over concurrent game structure (GBCG). Finally, the alternating Büchi automaton is developed over concurrent game structure (BCG) from the obtained GBCG, and the BCG is simplified for checking the satisfiability of the formula P.

Abstract:As the main object manipulated by a software system, data with a domain standard can contribute to the process of software design and data shareware between software systems. In this paper, focusing on domain data standardization, a domain data modelling language (DDML) and a domain data modelling method (DDMM based on the type theory are proposed. In DDML, the syntax and semantics of types and terms are defined to describe the structure of the domain data types and objects, and the typing rules are defined to process the judgement of t:T. For DDMM, the data modelling processes are presented with the data modelling of κ₁ (atomic type), κ₂ (data element), κ₃ (data element directory) and the generation of typing rules in κ₃. Furthermore, the definition of the data element directory sequences and the algorithms of checking its correctness are defined. Finally, a prototype of the domain data modelling system as a modelling tool is developed and applied to a real case of large scale by the generation of the domain data standard and its evaluation.

Abstract:The interrupt mechanism is a commonly used means to ensure real-time response to various asynchronous events in embedded systems and various real-time operating systems. Nested interrupts are likely to occur when the request of more urgent interrupt event arise while processing a less urgent one. Modeling and verifying such systems are challenging tasks. This paper proposes an approach to modeling and verifying systems with nested interrupts. First, MSVL (modeling, simulation and verification language) is extended to model such systems by defining an interrupt statement using projection temporal logic (PTL). Then, methods of modeling different nested interrupt systems using the interrupt statement are studied. Next, the MSV toolkit is extended to model, simulate, and verify MSVL programs with nested interrupts automatically. Finally, a case study is given to demonstrate how the proposed method works.

Abstract:Interrupt and context switch are basic mechanisms for multi-task scheduling in real-time and embedded systems. During schedulability analysis, the overheads of the interrupt and context switch should be considered in the calculation of tasks' worst-case response time. The current calculation methods of response time add interrupt as task with high priority, and simply add the overheads of context switch in the meantime. However, these methods neglect the details of practical systems and roughly give an inaccurate worst-case response time. In this paper, the mechanisms and time flow of interrupt and context switch are thoroughly described. In addition, their influence on tasks' critical instant is discussed. More importantly, a much more accurate calculation method for response time is presented. At last, simulations is conducted to validate the improvement in accuracy of this new method. The response time analysis accounting for scheduling overheads is extended in this paper for the resource-constrained hard real-time systems which need to accurately calculate the response time.

Abstract:Controller area network (CAN) is a high-speed serial fieldbus, widely deployed in the robot communication system. Due to the concurrency of service-oriented robot tasks and tightness requirement for real-time, it is necessary to explore how to refine the design model according to the bus protocol specifications and application system, in order to ensure the correctness and real-time requirements of the system and avoid bugs in design process. However the traditional methods are limited. This paper proposes a formal method to verify and analyze the correctness of CAN based fieldbus real-time control system. The model abstraction, formal modeling and automatic verification are presented for the system including the time automata model of master, joint controller, transceiver, arbitration and CAN bus. The formal models show that the worst arbitration delay of the low priority node increases rabidly with the increasing number of joints on the CAN bus. Furthermore, an improved dynamic priority strategy is designed and added into the formal models in order to improve the worst arbitration delay problem. The experimental results show that the deployment of the dynamic priority strategy not only reduces the arbitration delay of the low priority nodes, but also increases the capacity of nodes on CAN bus. The result provides guidance and effective reference for the system design.

Abstract:API (application programming interface) is widely used in modern software development process. Developers save a lot of time when they quickly build projects through invoking APIs. However, API is often difficult to use for many reasons, such as the presence of large number of interfaces, lack of perfect document, and no timely maintenance and updates. Further, API is often used incorrectly, resulting in bugs and sometimes significant security problems.This paper summarizes the recent domestic and overseas research results based on a thorough survey of the API related literatures. Firstly, it introduces the API concept and recognizes the three key issues that affect the API usage:poor API documentation, incomplete invocation specification and undetermined API call sequence. Next, it analyzes the latest advances from these three main aspects:API document, invocation specification and API recommendation. Finally, this paper outlines the challenges of the future research.

Abstract:Many service composition scenarios involve the sharing of user's privacy data. Due to the transparency of composition's business logic and lack of privacy protocol between user and member service, how to prevent the leakage of user privacy information has become a hot research topic in the field of service-oriented computing. A static analysis method of secure privacy information flow for service composition is proposed in this article according to the characteristics of privacy protection. Firstly, a security model is developed to formalize the security policy of privacy information flow on three aspects:service reputation, retention and purpose. Then, the composition is modeled with privacy workflow net, which gives support to the analysis of privacy information flow, and the detection of privacy information leakage is performed by analyzing execution paths of composition. Finally, a case study is included to demonstrate the effectiveness of the proposed method, and the performance experiment is also presented. Compared with the existing relevant works, the security model proposed reflects the characteristics of privacy protection, and the analysis method is able to deal with issues caused by the aggregation of privacy data items. Therefore, the application of this method can prevent the information leakage more efficiently.

Abstract:Fault localization is an essential step of software debugging, and spectrum-based fault localization (SFL) is currently amongst the most effective methods. The fundamental premise underlying SFL is that there exists a potential relationship between program spectra and the corresponding execution results. To formally describe and accurately quantify this relation, this paper introduces the conception of conditional probability to construct a P model by using the statistical analysis of experimental data. In addition, based on the presented P model, a fault localization method is proposed to effectively locate the faulty statement of the program under test. Finally, taking seven programs contained in the Siemens suite, Space program and three real-life Unix utility programs as the benchmark, a detailed experiment is conducted to evaluate the effectiveness and efficiency of the proposed method. Compared with fifteen classic fault localization methods, the experimental results show that the presented approach is more promising.

Abstract:This paper reviews two state-of-the-art algorithmic architectures, MapReduce and Spark, and compares them from their backgrounds, principles and application scenarios. The advantages and their corresponding limitations of these two algorithms are summarized. When dealing with non-iterative problems, MapReduce, by virtue of its task scheduling strategy and shuffle mechanisms, performs better than Spark in terms of intermediate data transfers and number of files. Spark can be used to deal with iterative problems and low latency issues, as it divides a computing task according to the dependencies between the data and the task. Compared with MapReduce, Spark can effectively reduce the number of intermediate data transmissions and the number of synchronizations, and improve the running efficiency of computing systems.

Abstract:Subgrpah matching is a basic operation in graph theory. This paper focuses on a variant, namely subgraph matching with inclusion degree (SMID), which retrieves subgraphs that are structurally isomorphic to the query graph while satisfying the condition that the inclusion degree between matched vertexes is greater than a given value. SMID can be applied to many applications, including paper search, crowdsourcing, and recruitment. To efficiently process SMID, this paper designs a novel signature mechanism for data graph and query graph respectively by holding the information of both vertex elements and graph structure. Based on graph signature, a dynamic signature tree (DS-Tree) is built to speed up the SMID processing. A compression method is proposed to reduce the memory usage of DS-Tree. To achieve a better performance, an efficient dominating-set-based subgraph matching algorithm is also developed. Extensive experiments on both real and synthetic datasets demonstrate that the method introduced in this paper outperforms state-of-the-art methods by an order of magnitude in terms of efficiency and scalability.

Abstract:The fifth generation mobile communication network, abbreviated 5G network or 5G, is also called the next generation of mobile communication network, which aims at constructing a networked society and realizing the goal of "everything-connecting". With 4G mobile communication network entering the commercial stage, the research on 5G has gained wider attention all over the world. The realization of the vision for 5G needs the revolution and innovation of system structure and core techniques, and until now the corresponding techniques and standards are in the primary stage. The new architectures, new business, and new technology bring new challenges to 5G security. This paper briefly summarizes performance, key technology, application scenario, and standardization progress of 5G, analyzes the security requirements and challenges of 5G, introduces 5G security framework, and investigates some key issues and the corresponding solutions based on the research efforts, white paper and related standards. Furthermore, the paper discusses the current research trends in industries and academia in the context of 5G security.