Bimonthly    Since 1986
ISSN 1000-9000(Print)
CN 11-2296/TP
Indexed in:
Publication Details
Edited by: Editorial Board of Journal Of Computer Science and Technology
P.O. Box 2704, Beijing 100190, P.R. China
Sponsored by: Institute of Computing Technology, CAS & China Computer Federation
Undertaken by: Institute of Computing Technology, CAS
Distributed by:
China: All Local Post Offices
Other Countries: Springer
  • Table of Content
      30 November 2021, Volume 36 Issue 6 Previous Issue   
    For Selected: View Abstracts Toggle Thumbnails
    Special Section on Software Systems 2021-Theme: Dependable Software Engineering
    Tao Xie, Shengchao Qin, Wenhui Zhang
    Journal of Computer Science and Technology, 2021, 36 (6): 1229-1230.  DOI: 10.1007/s11390-021-0008-x
    Supplementary Material | Related Articles | Metrics
    A Multi-Agent Spatial Logic for Scenario-Based Decision Modeling and Verification in Platoon Systems
    Jingwen Xu, Yanhong Huang, Jianqi Shi, Shengchao Qin
    Journal of Computer Science and Technology, 2021, 36 (6): 1231-1247.  DOI: 10.1007/s11390-021-1565-8
    To cater for the scenario of coordinated transportation of multiple trucks on the highway, a platoon system for autonomous driving has been extensively explored in the industry. Before such a platoon is deployed, it is necessary to ensure the safety of its driving behavior, whereby each vehicle’s behavior is commanded by the decision-making function whose decision is based on the observed driving scenario. However, there is currently a lack of verification methods to ensure the reliability of the scenario-based decision-making process in the platoon system. In this paper, we focus on the platoon driving scenario, whereby the platoon is composed of intelligent heavy trucks driving on cross-sea highways. We propose a formal modeling and verification approach to provide safety assurance for platoon vehicles’ cooperative driving behaviors. The existing Multi-Lane Spatial Logic (MLSL) with a dedicated abstract model can express driving scene spatial properties and prove the safety of multi-lane traffic maneuvers under the single-vehicle perspective. To cater for the platoon system’s multi-vehicle perspective, we modify the existing abstract model and propose a Multi-Agent Spatial Logic (MASL) that extends MLSL by relative orientation and multi-agent observation. We then utilize a timed automata type supporting MASL formulas to model vehicles’ decision controllers for platoon driving. Taking the behavior of a human-driven vehicle (HDV) joining the platoon as a case study, we have implemented the model and verified safety properties on the UPPAAL tool to illustrate the viability of our framework.
    References | Supplementary Material | Related Articles | Metrics
    MEBS: Uncovering Memory Life-Cycle Bugs in Operating System Kernels
    Gen Zhang, Peng-Fei Wang, Tai Yue, Xu Zhou, Kai Lu
    Journal of Computer Science and Technology, 2021, 36 (6): 1248-1268.  DOI: 10.1007/s11390-021-1593-4
    Allocation, dereferencing, and freeing of memory data in kernels are coherently linked. There widely exist real cases where the correctness of memory is compromised. This incorrectness in kernel memory brings about significant security issues, e.g., information leaking. Though memory allocation, dereferencing, and freeing are closely related, previous work failed to realize they are closely related. In this paper, we study the life-cycle of kernel memory, which consists of allocation, dereferencing, and freeing. Errors in them are called memory life-cycle (MLC) bugs. We propose an in-depth study of MLC bugs and implement a memory life-cycle bug sanitizer (MEBS) for MLC bug detection. Utilizing an interprocedural global call graph and novel identification approaches, MEBS can reveal memory allocation, dereferencing, and freeing sites in kernels. By constructing a modified define-use chain and examining the errors in the life-cycle, MLC bugs can be identified. Moreover, the experimental results on the latest kernels demonstrate that MEBS can effectively detect MLC bugs, and MEBS can be scaled to different kernels. More than 100 new bugs are exposed in Linux and FreeBSD, and 12 common vulnerabilities and exposures (CVE) are assigned.
    References | Supplementary Material | Related Articles | Metrics
    Trace Semantics and Algebraic Laws for Total Store Order Memory Model
    Li-Li Xiao, Hui-Biao Zhu, Qi-Wen Xu
    Journal of Computer Science and Technology, 2021, 36 (6): 1269-1290.  DOI: 10.1007/s11390-021-1616-1
    Modern multiprocessors deploy a variety of weak memory models (WMMs). Total Store Order (TSO) is a widely-used weak memory model in SPARC implementations and x86 architecture. It omits the store-load constraint by allowing each core to employ a write buffer. In this paper, we apply Unifying Theories of Programming (abbreviated as UTP) in investigating the trace semantics for TSO, acting in the denotational semantics style. A trace is expressed as a sequence of snapshots, which records the changes in registers, write buffers and the shared memory. All the valid execution results containing reorderings can be described after kicking out those that do not satisfy program order and modification order. This paper also presents a set of algebraic laws for TSO. We study the concept of head normal form, and every program can be expressed in the head normal form of the guarded choice which is able to model the execution of a program with reorderings. Then the linearizability of the TSO model is supported. Furthermore, we consider the linking between trace semantics and algebraic semantics. The linking is achieved through deriving trace semantics from algebraic semantics, and the derivation strategy under the TSO model is provided.
    References | Supplementary Material | Related Articles | Metrics
    Symbolic Reasoning About Quantum Circuits in Coq
    Wen-Jun Shi, Qin-Xiang Cao, Yu-Xin Deng, Han-Ru Jiang, Yuan Feng
    Journal of Computer Science and Technology, 2021, 36 (6): 1291-1306.  DOI: 10.1007/s11390-021-1637-9
    A quantum circuit is a computational unit that transforms an input quantum state to an output state. A natural way to reason about its behavior is to compute explicitly the unitary matrix implemented by it. However, when the number of qubits increases, the matrix dimension grows exponentially and the computation becomes intractable. In this paper, we propose a symbolic approach to reasoning about quantum circuits. It is based on a small set of laws involving some basic manipulations on vectors and matrices. This symbolic reasoning scales better than the explicit one and is well suited to be automated in Coq, as demonstrated with some typical examples.
    References | Supplementary Material | Related Articles | Metrics
    HRPDF: A Software-Based Heterogeneous Redundant Proactive Defense Framework for Programmable Logic Controller
    Ke Liu, Jing-Yi Wang, Qiang Wei, Zhen-Yong Zhang, Jun Sun, Rong-Kuan Ma, Rui-Long Deng
    Journal of Computer Science and Technology, 2021, 36 (6): 1307-1324.  DOI: 10.1007/s11390-021-1647-7
    Programmable logic controllers (PLCs) play a critical role in many industrial control systems, yet face increasingly serious cyber threats. In this paper, we propose a novel PLC-compatible software-based defense mechanism, called Heterogeneous Redundant Proactive Defense Framework (HRPDF). We propose a heterogeneous PLC architecture in HRPDF, including multiple heterogeneous, equivalent, and synchronous runtimes, which can thwart multiple types of attacks against PLC without the need of external devices. To ensure the availability of PLC, we also design an inter-process communication algorithm that minimizes the overhead of HRPDF. We implement a prototype system of HRPDF and test it in a real-world PLC and an OpenPLC-based device, respectively. The results show that HRPDF can defend against multiple types of attacks with 10.22% additional CPU and 5.56% additional memory overhead, and about 0.6 ms additional time overhead.
    References | Supplementary Material | Related Articles | Metrics
    AMCheX: Accurate Analysis of Missing-Check Bugs for Linux Kernel
    Ying-Jie Wang, Liang-Ze Yin, Wei Dong
    Journal of Computer Science and Technology, 2021, 36 (6): 1325-1341.  DOI: 10.1007/s11390-021-1666-4
    The Linux kernel adopts a large number of security checks to prevent security-sensitive operations from being executed under unsafe conditions. If a security-sensitive operation is unchecked, a missing-check issue arises. Missing check is a class of severe bugs in software programs especially in operating system kernels, which may cause a variety of security issues, such as out-of-bound accesses, permission bypasses, and privilege escalations. Due to the lack of security specifications, how to automatically identify security-sensitive operations and their required security checks in the Linux kernel becomes a challenge for missing-check analysis. In this paper, we present an accurate missing-check analysis method for Linux kernel, which can automatically infer possible security-sensitive operations. Particularly, we first automatically identify all possible security check functions of Linux. Then according to their callsites, a two-direction analysis method is leveraged to identify possible security-sensitive operations. A missing-check bug is reported when the security-sensitive operation is not protected by its corresponding security check. We have implemented our method as a tool, named AMCheX, on top of the LLVM (Low Level Virtual Machine) framework and evaluated it on the Linux kernel. AMCheX reported 12 new missing-check bugs which can cause security issues. Five of them have been confirmed by Linux maintainers.
    References | Supplementary Material | Related Articles | Metrics
    Verifying Contextual Refinement with Ownership Transfer
    Zhao-Hui Li, Xin-Yu Feng
    Journal of Computer Science and Technology, 2021, 36 (6): 1342-1366.  DOI: 10.1007/s11390-021-1671-7
    Contextual refinement is a compositional approach to compositional verification of concurrent objects. There has been much work designing program logics to prove the contextual refinement between the object implementation and its abstract specification. However, these program logics for contextual refinement verification cannot support objects with resource ownership transfer, which is a common pattern in many concurrent objects, such as the memory management module in OS kernels, which transfers the allocated memory block between the object and clients. In this paper, we propose a new approach to give abstract and implementation independent specifications to concurrent objects with ownership transfer. We also design a program logic to verify contextual refinement of concurrent objects w.r.t. their abstract specifications. We have successfully applied our logic to verifying an implementation of the memory management module, where the implementation is an appropriately simplified version of the original version from a real-world preemptive OS kernel.
    References | Supplementary Material | Related Articles | Metrics
    Verification of Real Time Operating System Exception Management Based on SPARCv8
    Zhi Ma, Lei Qiao, Meng-Fei Yang, Shao-Feng Li, Jin-Kun Zhang
    Journal of Computer Science and Technology, 2021, 36 (6): 1367-1387.  DOI: 10.1007/s11390-021-1644-x
    Exception management, as the lowest level function module of the operating system, is responsible for making abrupt changes in the control flow to react to exception events in the system. The correctness of the exception management is crucial to guaranteeing the safety of the whole system. However, existing formal verification projects have not fully considered the issues of exceptions at the assembly level. Especially for real-time operating systems, in addition to basic exception handling, there are nested exceptions and task switching by exceptions service routine. In our previous work, we used high-level abstraction to describe the basic elements of the exception management and verified correctness only at the requirement layer. Building on earlier work, this paper proposes EMS (Exception Management SPARCv8), a practical Hoare-style program framework to verify the exception management based on SPARCv8 (Scalable Processor Architecture Version 8) at the design layer. The framework describes the low-level details of the machine, such as registers and memory stack. It divides the execution logic of the exception management into six phases for comprehensive formal modeling. Taking the executing scenario of the real-time operating system SpaceOS on the Beidou-3 satellite as an example, we use the EMS framework to verify the exception management. All the formalization and proofs are implemented in the interactive theorem prover Coq.
    References | Supplementary Material | Related Articles | Metrics
    Regular Paper
    Activity Diagram Synthesis Using Labelled Graphs and the Genetic Algorithm
    Chun-Hui Wang, Zhi Jin, Wei Zhang, Didar Zowghi, Hai-Yan Zhao, Wen-Pin Jiao
    Journal of Computer Science and Technology, 2021, 36 (6): 1388-1406.  DOI: 10.1007/s11390-020-0293-9
    Many applications need to meet diverse requirements of a large-scale distributed user group. That challenges the current requirements engineering techniques. Crowd-based requirements engineering was proposed as an umbrella term for dealing with the requirements development in the context of the large-scale user group. However, there are still many issues. Among others, a key issue is how to merge these requirements to produce the synthesized requirements description when a set of requirements descriptions from different participants are received. Appropriate techniques are needed for supporting the requirements synthesis. Diagrams are widely used in industry to represent requirements. This paper chooses the activity diagrams and proposes a novel approach for the activity diagram synthesis which adopts the genetic algorithm to repeatedly modify a population of individual solutions toward an optimal solution. As a result, it can automatically generate a resulting diagram which combines the commonalities as many as possible while leveraging the variabilities of a set of input diagrams. The approach is featured by: 1) the labelled graph proposed as the representation of the candidate solutions during the iterative evolution; 2) the generalized entropy proposed and defined as the measurement of the solutions; 3) the genetic algorithm designed for sorting out the high-quality solution. Four cases of different scales are used to evaluate the effectiveness of the approach. The experimental results show that not only the approach gets high precision and recall but also the resulting diagram satisfies the properties of minimization and information preservation and can support the requirements traceability.
    References | Supplementary Material | Related Articles | Metrics
    A Unified Shared-Private Network with Denoising for Dialogue State Tracking
    Qing-Bin Liu, Shi-Zhu He, Kang Liu, Sheng-Ping Liu, Jun Zhao
    Journal of Computer Science and Technology, 2021, 36 (6): 1407-1419.  DOI: 10.1007/s11390-020-0338-0
    Dialogue state tracking (DST) leverages dialogue information to predict dialogues states which are generally represented as slot-value pairs. However, previous work usually has limitations to efficiently predict values due to the lack of a powerful strategy for generating values from both the dialogue history and the predefined values. By predicting values from the predefined value set, previous discriminative DST methods are difficult to handle unknown values. Previous generative DST methods determine values based on mentions in the dialogue history, which makes it difficult for them to handle uncovered and non-pointable mentions. Besides, existing generative DST methods usually ignore the unlabeled instances and suffer from the label noise problem, which limits the generation of mentions and eventually hurts performance. In this paper, we propose a unified shared-private network (USPN) to generate values from both the dialogue history and the predefined values through a unified strategy. Specifically, USPN uses an encoder to construct a complete generative space for each slot and to discern shared information between slots through a shared-private architecture. Then, our model predicts values from the generative space through a shared-private decoder. We further utilize reinforcement learning to alleviate the label noise problem by learning indirect supervision from semantic relations between conversational words and predefined slot-value pairs. Experimental results on three public datasets show the effectiveness of USPN by outperforming state-of-the-art baselines in both supervised and unsupervised DST tasks.
    References | Supplementary Material | Related Articles | Metrics
    Pre-Train and Learn: Preserving Global Information for Graph Neural Networks
    Dan-Hao Zhu, Xin-Yu Dai, Jia-Jun Chen
    Journal of Computer Science and Technology, 2021, 36 (6): 1420-1430.  DOI: 10.1007/s11390-020-0142-x
    Graph neural networks (GNNs) have shown great power in learning on graphs. However, it is still a challenge for GNNs to model information faraway from the source node. The ability to preserve global information can enhance graph representation and hence improve classification precision. In the paper, we propose a new learning framework named G-GNN (Global information for GNN) to address the challenge. First, the global structure and global attribute features of each node are obtained via unsupervised pre-training, and those global features preserve the global information associated with the node. Then, using the pre-trained global features and the raw attributes of the graph, a set of parallel kernel GNNs is used to learn different aspects from these heterogeneous features. Any general GNN can be used as a kernal and easily obtain the ability of preserving global information, without having to alter their own algorithms. Extensive experiments have shown that state-of-the-art models, e.g., GCN, GAT, Graphsage and APPNP, can achieve improvement with G-GNN on three standard evaluation datasets. Specially, we establish new benchmark precision records on Cora (84.31%) and Pubmed (80.95%) when learning on attributed graphs.
    References | Related Articles | Metrics
    CDM: Content Diffusion Model for Information-Centric Networks
    Bo Chen, Liang Liu, Hua-Dong Ma
    Journal of Computer Science and Technology, 2021, 36 (6): 1431-1451.  DOI: 10.1007/s11390-021-0205-7
    This paper proposes the Content Diffusion Model (CDM) for modeling the content diffusion process in information-centric networking (ICN). CDM is inspired by the epidemic model and it provides a method of theoretical quantitative analysis for the content diffusion process in ICN. Specifically, CDM introduces the key functions to formalize the key factors that influence the content diffusion process, and thus it can construct the model via a simple but efficient way. Further, we derive CDM by using different combinations of those key factors and put them into several typical ICN scenarios, to analyze the characteristics during the diffusion process such as diffusion speed, diffusion scope, average fetching hops, changing and final state, which can greatly help to analyze the network performance and application design. A series of experiments are conducted to evaluate the efficacy and accuracy of CDM. The results show that CDM can accurately illustrate and model the content diffusion process in ICN.
    References | Supplementary Material | Related Articles | Metrics
  Journal Online
Current Issue
Just Accepted
Top Cited Papers
Top 30 Most Read
Top 30 Most Download
   ScholarOne Manuscripts
   Log In

User ID:


  Forgot your password?

Enter your e-mail address to receive your account information.

ISSN 1000-9000(Print)

CN 11-2296/TP

Editorial Board
Author Guidelines
Journal of Computer Science and Technology
Institute of Computing Technology, Chinese Academy of Sciences
P.O. Box 2704, Beijing 100190 P.R. China
E-mail: jcst@ict.ac.cn
  Copyright ©2015 JCST, All Rights Reserved