Abstract:As a lightweight and highly reliable embedded database, SQLite3 has been widely used in many security-critical areas such as aerospace and operating systems. It provides rich and flexible API functions to support users to quickly construct projects. However, an incorrect API function call sequence can cause serious consequences, including runtime errors, memory leaks, orprogram crashes. In order to efficiently and accurately monitor the correct call of SQLite3 database API functions, this paper presents a parallel runtime verification approachfor multi-core machines. This approach first analyzes API function documents, automatically mines API call specification descriptions, and assists humans to formalize them as propositional projection temporal logic formulaswith the full regular expressiveness. Then, while the program is running, the multi-task scheduling strategy is employed to divide the generatedstate sequence into several segments and achieve the parallel verification for different segments. Experimental results show that the proposed approachis able to find that among the 30 programs invoking SQLite3 database API functions, there are 16 violations of the API call sequence specifications, with a violation rate of 53%. In addition, with comparative experiments of traditional sequential runtime verification approaches,it is shown that the proposed parallel runtime verification in this study can effectively improve the verification efficiency in a multi-core system.

Abstract:LTL synthesis is an important sub-class of program synthesis. The process of LTL synthesis is to automatically build a controller which interacts with the environment, where the objective is to make the interactive behaviors satisfy a given LTL formula. Generally speaking, LTL synthesis problem is often defined as a two-player game, one player is environment, and the other is controller. The solution of the problem is called synthesis policy. Recently, researchers have investigated that there exists close correspondence between LTL synthesis and non-deterministic planning from a theoretical point of view. This paper presents a novel LTL synthesis approach exploiting non-deterministic planning techniques. Moreover, the correctness and the completeness of the approach is proved formally. Concretely, at first LTL formulas are converted into Büchi automata, then the automata with the two-player game definition of LTL synthesis are translated into full-observable non-deterministic planning models which can be directly fed to existing effective planners. The experimental results show that planning based LTL synthesis has significant advantage over other approaches in improving the quality of solutions, i.e., the size of the obtained policies is much smaller.

Abstract:Asynchronously communicating program is the program that processes achieve non-blocking concurrency through asynchronous message passing. At present, the verification problem of asynchronously communicating program is usually reduced to vector addition system and its extension model, so it has high complexity and lack of efficient tools. Basic Parallel Processes, as a subclass of vector addition system, whose verification of complexity reachability is NP-complete, can also be used as an important model for verifying concurrent programs. Firstly, improve the Actor communicating system proposed by Osualdo, et al., by reducing it to Basic Parallel Processes. Then, realizing an automatic model checker for basic parallel processes named RABLE. The experimental results show that the verification method is more efficient than the existing tools for a series of program verification problems of asynchronously communicating programs.

Abstract:Model learning of timed automata (TA) aims to build a formal model of software and hardware systems by external inputs and outputs. Learning of deterministic one-clock TA is one of the important research directions, but current algorithm has some limitations and is difficult to be applied to complex systems. Therefore, an improved learning algorithm is proposed, which uses logical-time classification tree instead of logical-time observation table as the internal data structure of the learning algorithm, effectively reducing the number of membership queries and the space complexity of the algorithm. In addition, it can efficiently construct hypothetical automata. Finally, relevant experiments have been carried out, and the experimental results show that the improved algorithm proposed in this study reduces the number of member queries by 60% and the number of equivalent queries by 5%. At the same time, in this experiment, the learning speed of the improved algorithm can be increased by more than 50 times at most.

Abstract:CPS (cyber physical system) combines physics and computation on the basis of environment perception and can realize intelligent interaction with the environment. However, the constant change of cyber physical space poses some challenges to the safety of CPS resources. Therefore, how to study this kind of CPS resource safety problems caused by topology and time changes becomes the key. This study proposes a CPS-oriented resource modeling and safety verification method to solve this problem. Firstly, on the basis of TCSP (timed communicating sequential process), resource vector is extended and DSR-TCSP (duration-space resource TCSP) is proposed, enable it to describe resources in the CPS topology. Secondly, the time safety requirements are obtained from the resource safety requirements of space and time constraints, and verified by the time verification algorithm of DSR-TCSP. Thirdly, the model meeting the time safety requirements is converted to the reaction of bigraphs and bigraphs reactive system, and the model is input into the bigraphs testing tool BigMC to verify its physical topology safety requirements. For the counter examples that do not pass the verification, the DSR-TCSP model is modified until the proposed safety requirements are met. Finally, a driving scenario is given to verify the effectiveness of the proposed method.

Abstract:The scale of problems that can be verified by Boolean satisfiability (SAT) solving is usually limited. Therefore, how to predict the satisfiability of SAT problems with high accuracy is an important research problem and also a challenging task. Previous works used graphs consisting of literal nodes and clause nodes to represent the structure of SAT problems. The important relation information between variables and clauses is missing. Raw SAT instances are encoded to multi-relational heterogeneous graphs and a message passing relation (MPR) network model is used to capture more structure features of an SAT instance. It is showed that the MPR network model could outperform previous work in terms of prediction accuracy, generalization ability, and resource requirement. An average prediction accuracy of 81% is achieved on all datasets. The model trained on small-scale problems (the number of variables is 100) achieves an average prediction accuracy of 80.8% on larger-scale datasets. Prominently, this model gets 99% prediction accuracy on the randomly generated non-uniform random SAT problems, which means it has learned important features to predict satisfiability. Moreover, the running time for prediction increases linearly with the size of the problem. In conclusion, the proposed method is of higher prediction accuracy and better generalization ability based on a relational messaging network to predict propositional satisfiability.

Abstract:Airborne software is widely used in aerospace, which dramatically improves the performance of airborne equipment. Nevertheless, with airborne software's increasing scale and function, it is challenging to develop airborne software. How to ensure the correctness and safety of airborne software has become a difficult problem to be solved. Model-based development can effectively improve development efficiency, and formal methods can effectively guarantee the correctness of software. To reduce the difficulty of development and ensure airborne software's correctness and safety, this study proposes a hierarchical refinement modeling and verification method of airborne software using the SysML state machine diagram subset. Firstly, the SysML state machine diagram is used to model the dynamic behavior of airborne software. According to the proposed refinement rules, the initial model is refined to obtain the refined design model step by step manually. Then, according to the dynamic characteristics of the software model, the SysML state machine model is automatically converted to a network of timed automata, and the formal TCTL properties are manually extracted from the software requirements for model checking. Secondly, to realize coding automation, the SysML model is automatically converted to Simulink, and Simulink Coder generates the source code. Finally, an automatic flight control software is developed and verified based on the proposed method, and the experimental results show the effectiveness of the method.

Abstract:Smart contract consists of a set of commitments defined in digital form. Smart contracts can greatly reduce the intermediate links in agreement formulation and improve the efficiency of agreement formulation. Blockchain technology provides a trusted platform for the execution of smart contracts. As the application of blockchain technology expands and deepens, the role of smart contracts will become more and more important, and the potential reliability problems, however, may cause huge lose to participants. The reliability of smart contracts has received more and more attention, but there is no systematic research on problems caused by the time properties of smart contracts. This study analyzes typical smart contracts, sorts out the different manifestations of time constraints, summarizes several time constraint patterns of smart contracts and formalizes them; defines transform rules from Solidity smart contracts to the timed automata. The translation from smart contracts to the model of model checker UPPAAL is then implemented and UPPAAL is used to verify the time properties of smart contracts. Case study is carried out on two practical smart contracts. The results show that the patterns extracted are general and the formal verification solution proposed is feasible and efficient.

Abstract:TSO-to-TSO linearizability, TSO-to-SC linearizability, and TSO linearizability are three typical variants of linearizability on the total store order (TSO) memory model. This study proposes k-bounded TSO-to-TSO linearizability and k-bounded TSO linearizability, and investigates the verification problems of k-bounded TSO-to-TSO linearizability, k-bounded TSO-to-SC linearizability, and k-bounded TSO linearizability that are bounded versions of the above variants of linearizability, defined on k-extended histories. Although the corresponding executions of k-extended histories contain a bounded number (less or equal than k) of call, return, flushCall and flushReturn actions, the verification problems of these three bounded versions of linearizability are non-trivial since the corresponding executions of k-extended histories may still contain an unbounded number of write actions and use store buffers with an unbounded capacity, which makes their operational semantics built upon infinite state transition systems. The k-bounded TSO-to-TSO linearizability problem, k-bounded TSO-to-SC linearizability problem, and k-bounded TSO linearizability problem between concurrent data structures and their sequential specifications are reduced into TSO-to-TSO linearizability problem between sets of k-extended histories, which provides a uniform framework for verifying the three bounded versions of linearizability on the TSO memory model. The key point of the proposed approach is to check if a concurrent data structure contains a specific k-extended history. It is proved that this problem is decidable by reducing it into the control state reachability problem of lossy channel machines, which is known decidable. This reduction essentially requires call and return actions to be transformed into write, flush or cas (compare-and-swap) actions. In the definition of TSO-to-TSO linearizability, a call or return action taken by a process changes the store buffer and the control state of the process at the same time. A specific write action is added immediately after each call or return action; thus, the influence on store buffers is mimicked by these specific write actions and their corresponding flush actions. To mimic the influence on control states, an observer process and bind specific cas actions of the observer process are introduced to each call or return actions. In this way, three bounded versions of linearizability are decidable on the TSO memory model are proved. Three bounded versions of linearizability on the TSO memory model are at level F_ω^ω are further proved in the fast-growing hierarchy of recursive functions. This is proved by stating that the reachability problem of single-channel basic lossy channel machines, which is known in such complexity class, can be reduced into the three bounded versions of linearizability problems on the TSO memory model, while the latter problem can also be reduced into the former problem.

Abstract:This study proposes a novel approach for synthesizing ranking functions that are expressed as feed-forward neural networks. The approach employs a counter example-guided synthesis procedure, where a learner and a verifier interact to synthesize ranking function. The learner trains a candidate ranking function that satisfies the ranking function conditions over a set of sampled data, and the verifier either ensures the validity of the candidate ranking function or yields counterexamples, which are passed back to further guide the learner. The procedure leverages efficient supervised learning algorithm, while guaranteeing formal soundness via SMT solver. The tool SyntheRF is implemented, then, its scalability and effectiveness are evaluated over a set of benchmark examples.

Abstract:Model checking techniques based on automata theory play a central role in formal verification. Nevertheless, classical automata are not composable for temporal operators, such that the model checking algorithms for various temporal logics cannot be organically integrated. To realize efficient model checking for real-time branching-time temporal logic RTCTL^* integrating bounded temporal operators, a construction method is proposed for RTCTL^* positive temporal testers, and the RTCTL^* symbolic model checking algorithm is further proposed based on positive temporal testers. It is proved that the proposed construction method for RTCTL^* positive temporal testers is complete. It is also proved that the time complexity of the proposed algorithm is linear in the size of the verified system and exponential in the length of the given formula. Based on the JavaBDD software package, the model checking tool MCTK 2.0.0 is successfully developed for the proposed algorithm. The experimental data and the analysis results show that although MCTK consumes more memory than the famous symbolic model checker nuXmv, the time complexity of MCTK is doubly-exponentially less than nuXmv, which makes it possible to verify real-time temporal properties of large-scale systems by MCTK.

Abstract:Time Petri nets is a formal method for modelling real-time systems, and timed computation tree logic (TCTL) is a logical expression for specifying time-related design requirements of real-time systems, so time Petri net based TCTL model checking has been widely used to verify the correction of real-time systems. For those real-time systems with priority such as multi-core multi-task real-time systems, it not only needs to consider time constraints among tasks but also needs to consider priority of task execution and the preemptive scheduling problem caused by priority, which results that modelling and analysis of these systems become more difficult. Therefore, this study proposes time-point-interval prioritized time Petri nets. By defining priority of transition firing and suspendable transitions in time Petri nets, time-point-interval prioritized time Petri nets can model preemptive scheduling of real-time systems, i.e., first of all, a high-priority task preempts the resource of a low-priority task, which results in the interruption of the latter, then the former is completed and releases the resource, and finally the latter gets the resource again and resumes from the interruption. This study uses time-point-interval prioritized time Petri nets to model multi-core multi-task real-time systems, uses TCTL to describe their design requirements, designs the corresponding model checking algorithms, and develops the corresponding model checker to verify their correctness. An example is used to show the effectiveness of the proposed model and method.

Abstract:When analyzing real-world programs, it is often necessary to analyze the function calls in the program, and interprocedural analysis is generally used to achieve full program analysis. Function inlining is one of the most accurate and easily achievable methods for interprocedural analysis. Function inlining allows existing intraprocedural analysis methods and tools to support the analysis of programs that contain function calls. However, the size of the code increases dramatically after function inlining, and a large number of intermediate variables will be generated, which increases the variable dimension of program analysis and causes the process of program analysis to consume a lot of memory and time. This study considers some shortcomings of interprocedural analysis of function inlining based on the abstract interpretation framework and proposes a corresponding optimization method. Program analysis based on abstract interpretation is concerned with automatically deriving invariant constraint relations among program variables, so the size of the program environment constituted by program variables (i.e., the set of relevant variables to be considered at each program point) has an important impact on the time and space overhead of the analysis. In order to reduce the overhead of program analysis after function inlining, this study proposes a program environment reduction optimization method for inline function blocks. The method analyzes the program code after inlining functions to determine the program environment (i.e., set of related variables) to be maintained at different program points, instead of sharing the same global program environment at all program points, so as to realize the dimensionality reduction of the program state. The architecture, modules, and algorithm details of the tool DRIP (dimension reduction for analyzing function inlined program) implemented based on this method are described in detail. The results show that DRIP achieves sound results in variable elimination, even reducing more than half of the variables in some test suites, and the time and space spent is also reduced to a certain extent.

Abstract:Termination bugs such as deadlocks and infinite loops are common in concurrent file systems due to complex implementations. Existing efforts on file system verification have ignored the termination property. Based on a verified concurrent file system, AtomFS, this paper presents the verification of its termination property, which ensures that every method call will always return under fair scheduling. Proving a method's termination requires to show that when the method is blocked, the source thread of the obstruction will make progress. The core lies in showing the termination of the lock coupling traversal. However, two major challenges applying the idea are as following. (1) The file system is in the shape of a tree and allows threads that block others to diverge on its traversal. As a result, multiple sources of obstruction globally might be found, which leads to the loss of locality in proof, (2) The rename operation needs to traverse on two paths and could bring obstruction across the path. It not only leads to more difficulty in source location, but also could cause the failure in finding the source of obstruction when two renames block each other. This study handles these challenges through two key techniques:(1) Only recognizing each local blocking chain for source location; (2) Determining partial orders of obstruction among threads. A framework called CRL-T have been successfully built for termination verification and apply it to verify the termination of AtomFS. All the proofs are mechanized in Coq.

Abstract:The embedded system has been wildly applied in safety-critical system, such as aviation system, automobile systems, and telemedicine. However, reliability is not a property of these embedded systems that can be easily assured, for that the complexity of system architecture also increased rapidly. Thus, the reliability analysis and verification should be conducted in early design stages, so that to provide highly reliable and qualified systems while avoid economy and efficiency lose. In an embedded system, the system reliability is affected by both hardware errors, software defects, and hardware-software interactive failures. Although many achievements have been accomplished in the field of hardware-software integrated reliability analysis, they are not suitable to be applied in the early stages of system design and implementation. The SAE architecture analysis and design language (AADL) has provided an effective means of system architecture design and non-functional property verification, but it is not capable of hardware-software integrated reliability analysis for that its error model annex concentrates on software component error behavior modeling, and it cannot effectively describe the hardware error impact and propagation mechanism. An architecture level hardware-software integrated reliability modeling and analysis method, which considers the impact of both hardware, software and hardware-software interactive errors simultaneously, is proposed in this study. Combined with the transaction level modeling method in electronic circuit design, the proposed method extends the syntax and semantics of AADL in transaction level error behavior modeling to support the fine description of hardware component error and error propagation. Mapping rules from the enhanced AADL reliability model to generalized stochastic Petri net model are also proposed, so that the reliability model can be converted into calculation model to complete the hardware-software integrated reliability analysis and assessment of embedded system. A prototype IDE toolkit which implements the proposed method is developed to do testing and evaluation. It is used to do reliability modeling and analysis of avionic system, which is the control system of an air boost control system belongs to a certain type airplane. The result shows that, the proposed methods is capable of hardware-software integrated reliability modeling and analysis of complicated embedded system, and will provide refined analysis result compared with traditional AADL based methods.

Abstract:The study of code naturalness is one of the common research hotspots in the field of natural language processing and software engineering, aiming to solve various software engineering tasks by building a code naturalness model based on natural language processing techniques. In recent years, as the size of source code and data in the open source software community continues to grow, more and more researchers are focusing on the information contained in the source code, and a series of research results have been achieved. While at the same time, code naturalness research faces many challenges in code corpus construction, model building, and task application. In view of this, this paper reviews and summarizes the progress of code naturalness research and application in recent years in terms of code corpus construction, model construction, and task application. The main contents include:(1) Introducing the basic concept of code naturalness and its research overview; (2) The current corpus of code naturalness research is summarized, and the modeling methods for code naturalness are classified and summarized; (3) Summarizing the experimental validation methods and model evaluation metrics of code naturalness models; (4) Summarizing and categorizing the current application status of code naturalness; (5) Summarizing the key issues of code naturalness techniques; (6) Prospecting the future development of code naturalness techniques.

Abstract:With the progresses of open source concept, open source software has become the trend of software development, and the use of open source software is subject to various open source licenses. How open source participants can correctly choose open source software licenses in their development to ensure the efficient and reasonable use of the collaborative results of community groups is still an urgent issue to be solved. To this end, commonly used open source licenses are firstly analyzed and interpreted for OSI certification in the paper. Furthermore, with the studies of the license terms and structure, the open source license framework, and compatibility derivation models are deduced. The model is applied to the analysis and interpretation of Mulan permissive software license independently developed in China. Finally, based on the above work, a license choosing tool for open source license is developed, which provides references and decision support for open source developers to understand and use licenses.

Abstract:Smart contract, one of the most successful applications of blockchain, provides the foundation for realizing various real-world applications of blockchain, playing an essential role in the blockchain ecosystem. However, frequent smart contract security events not only caused huge economic losses but also destroyed the blockchain-based credit system. The security and reliability of smart contract thus gain wide attention from researchers worldwide. This study first introduces the common types and typical cases of smart contract vulnerabilities from three levels, i.e., Solidity code layer, EVM execution layer, and blockchain system layer. Then, the research progress of smart contract vulnerability detection is reviewed and existing efforts are classified into five categories, namely formal verification, symbolic execution, fuzzing testing, intermediate representation, and deep learning. The detectable vulnerability types, accuracy, and time consumption of existing vulnerability detection methods are compared in detail as well as their limitations and improvements. Finally, based on the summary of existing researches, the challenges in the field of smart contract vulnerability detection are discussed and combined with the deep learning technology to look forward to future research directions.

Abstract:Many reinforcement learning methods do not take into consideration the safety of decisions made by agents. In fact, regardless of many successful applications in research and industrial area, it is still necessary to make sure that agent decisions are safe. The traditional approaches to address the safety problems mainly include changing the objective function, changing the exploration process of agents and so on, which, however, neglect the possible grave consequences caused by unsafety decisions and, as a result, cannot effectively solve the problem. To address the issue, a safe Sarsa(λ) and a safe Sarsa method, based on the constrained Markov decision processes, are proposed by imposing safety constraints to the action space. During the solution process, the agent should not only seek to get the maximum state-action value, but also satisfy the safety constraints, so as to obtain an optimal safety strategy. Since the standard reinforcement learning methods are no longer suitable for solving the safe Sarsa(λ) and safe Sarsa model, in order to obtain the global optimal state-action value function under the constrained conditions, a solution model of safe reinforcement learning is also introduced. Such model is based on linearized multidimensional constraints and adopts the Lagrange multiplier method to transform safe reinforcement learning model into a convex model provided that the objective and constraint functions are differentiable. The proposed solution algorithm guides the agent away from a local optimal and improves the solution efficiency and precision. The feasibility of the algorithm is proved. Finally, the effectiveness of the algorithm is verified by experiments.

Abstract:To reveal parent-child influence relationships between nodes in a diffusion network, most prior work requires knowledge of node infection time, which is possible only by carefully monitoring the diffusion process. This work investigates how to solve this problem by learning from diffusion results, which contain only the final infection statuses of nodes in each diffusion process and are often more easily accessible in practice. A conditional entropy-based method is presented to infer potential candidate parent nodes for each node in the network. Furthermore, the inference results are able to be refined by identifying and pruning the inferred influence relations that are unlikely to exist in reality. Experimental results on both synthetic and real-world networks verify the effectiveness and efficiency of our approach.

Abstract:The optimal sequenced path query is a hot topic in the intelligent transportation. In practical applications, the existing approaches cannot effectively solve these constrained path query problems in the time-dependent network because of the constraints of the optimal sequenced path query. This study employs the rules to stand for the constraints. In order to solve the shortest travel time problem of the constrained path in the time-dependent network, a new query form of the optimal sequenced path, namely the multi-rule based shortest path query, is studied. This study provides a unified framework, which includes the path set query and the shortest path query. In order to efficiently retrieve the path set satisfying multiple rules, a new tree traversal method, inheritance and traversal of trees, is proposed on the basis of generalized rule tree. Based on the idea of tree inheritance and traversal, a pruning method is proposed to prune the path set, and finally, the candidate path set is obtained. In the shortest path query part, a dynamic threshold method is proposed. Extensive experiments with two real data offer evidence that the proposed solutions can solve the problem of multi-rule based shortest path query.