Open Access. Powered by Scholars. Published by Universities.®
Physical Sciences and Mathematics Commons™
Open Access. Powered by Scholars. Published by Universities.®
Articles 1 - 8 of 8
Full-Text Articles in Physical Sciences and Mathematics
Automatic Generation Of Provably Correct Embedded Systems, Shang-Wei Lin, Yang Liu, Pao-Ann Hsiung, Jun Sun, Jin Song Dong
Automatic Generation Of Provably Correct Embedded Systems, Shang-Wei Lin, Yang Liu, Pao-Ann Hsiung, Jun Sun, Jin Song Dong
Research Collection School Of Computing and Information Systems
With the demand for new and complicated features, embedded systems are becoming more and more difficult to design and verify. Even if the design of a system is verified, how to guarantee the consistency between the design and its implementation remains a big issue. As a solution, we propose a framework that can help a system designer to model his or her embedded system using a high-level modeling language, verify the design of the system, and automatically generate executable software codes whose behavior semantics are consistent with that of the high-level model. We use two case studies to demonstrate the …
More Anti-Chain Based Refinement Checking, Ting Wang, Songzheng Song, Jun Sun, Yang Liu, Jin Song Dong, Xinyu Wang, Shanping Li
More Anti-Chain Based Refinement Checking, Ting Wang, Songzheng Song, Jun Sun, Yang Liu, Jin Song Dong, Xinyu Wang, Shanping Li
Research Collection School Of Computing and Information Systems
Refinement checking plays an important role in system verification. It establishes properties of an implementation by showing a refinement relationship between the implementation and a specification. Recently, it has been shown that anti-chain based approaches increase the efficiency of trace refinement checking significantly. In this work, we study the problem of adopting anti-chain for stable failures refinement checking, failures-divergence refinement checking and probabilistic refine checking (i.e., a probabilistic implementation against a non-probabilistic specification). We show that the first two problems can be significantly improved, because the state space of the product model may be reduced dramatically. Though applying anti-chain for …
An Analytical And Experimental Comparison Of Csp Extensions And Tools, Ling Shi, Yang Liu, Jun Sun, Jin Song Dong, Gustavo Carvalho
An Analytical And Experimental Comparison Of Csp Extensions And Tools, Ling Shi, Yang Liu, Jun Sun, Jin Song Dong, Gustavo Carvalho
Research Collection School Of Computing and Information Systems
Communicating Sequential Processes (CSP) has been widely applied to modeling and analyzing concurrent systems. There have been considerable efforts on enhancing CSP by taking data and other system aspects into account. For instance, CSP M combines CSP with a functional programming language whereas CSP# integrates high-level CSP-like process operators with low-level procedure code. Little work has been done to systematically compare these CSP extensions, which may have subtle and substantial differences. In this paper, we compare CSP M and CSP# not only on their syntax, but also operational semantics as well as their supporting tools such as FDR, ProB, and …
Verification Of Orchestration Systems Using Compositional Partial Order Reduction, Tian Huat Tan, Yang Liu, Jun Sun, Jin Song Dong
Verification Of Orchestration Systems Using Compositional Partial Order Reduction, Tian Huat Tan, Yang Liu, Jun Sun, Jin Song Dong
Research Collection School Of Computing and Information Systems
Orc is a computation orchestration language which is designed to specify computational services, such as distributed communication and data manipulation, in a concise and elegant way. Four concurrency primitives allow programmers to orchestrate site calls to achieve a goal, while managing timeouts, priorities, and failures. To guarantee the correctness of Orc model, effective verification support is desirable. Orc has a highly concurrent semantics which introduces the problem of state-explosion to search-based verification methods like model checking. In this paper, we present a new method, called Compositional Partial Order Reduction (CPOR), which aims to provide greater state-space reduction than classic partial …
Scalable Multi-Core Model Checking Fairness Enhanced Systems, Yang Liu, Jun Sun, Jin Song Dong
Scalable Multi-Core Model Checking Fairness Enhanced Systems, Yang Liu, Jun Sun, Jin Song Dong
Research Collection School Of Computing and Information Systems
Rapid development in hardware industry has brought the prevalence of multi-core systems with shared-memory, which enabled the speedup of various tasks by using parallel algorithms. The Linear Temporal Logic (LTL) model checking problem is one of the difficult problems to be parallelized or scaled up to multi-core. In this work, we propose an on-the-fly parallel model checking algorithm based on the Tarjan’s strongly connected components (SCC) detection algorithm. The approach can be applied to general LTL model checking or with different fairness assumptions. Further, it is orthogonal to state space reduction techniques like partial order reduction. We enhance our PAT …
Verifying Stateful Timed Csp Using Implicit Clocks And Zone Abstraction, Jun Sun, Yang Liu, Jin Song Dong, Xian Zhang
Verifying Stateful Timed Csp Using Implicit Clocks And Zone Abstraction, Jun Sun, Yang Liu, Jin Song Dong, Xian Zhang
Research Collection School Of Computing and Information Systems
In this work, we study model checking of compositional real-time systems. A system is modeled using mutable data variables as well as a compositional timed process. Instead of explicitly manipulating clock variables, a number of compositional timed behavioral patterns are used to capture quantitative timing requirements, e.g. delay, timeout, deadline, timed interrupt, etc. A fully automated abstraction technique is developed to build an abstract finite state machine from the model. The idea is to dynamically create/delete clocks, and maintain/solve a constraint on the clocks. The abstract machine weakly bi-simulates the model and, therefore, LTL model checking or trace-refinement checking are …
Model Checking Linearizability Via Refinement, Yang Liu, Wei Chen, Yanhong A. Liu, Jun Sun
Model Checking Linearizability Via Refinement, Yang Liu, Wei Chen, Yanhong A. Liu, Jun Sun
Research Collection School Of Computing and Information Systems
Linearizability is an important correctness criterion for implementations of concurrent objects. Automatic checking of linearizability is challenging because it requires checking that 1) all executions of concurrent operations be serializable, and 2) the serialized executions be correct with respect to the sequential semantics. This paper describes a new method to automatically check linearizability based on refinement relations from abstract specifications to concrete implementations. Our method avoids the often difficult task of determining linearization points in implementations, but can also take advantage of linearization points if they are given. The method exploits model checking of finite state systems specified as concurrent …
Pat: Towards Flexible Verification Under Fairness, Jun Sun, Yang Liu, Jin Song Dong, Jun Pang
Pat: Towards Flexible Verification Under Fairness, Jun Sun, Yang Liu, Jin Song Dong, Jun Pang
Research Collection School Of Computing and Information Systems
Recent development on distributed systems has shown that a variety of fairness constraints (some of which are only recently defined) play vital roles in designing self-stabilizing population protocols. Current practice of system analysis is, however, deficient under fairness. In this work, we present PAT, a toolkit for flexible and efficient system analysis under fairness. A unified algorithm is proposed to model check systems with a variety of fairness effectively in two different settings. Empirical evaluation shows that PAT complements existing model checkers in terms of fairness. We report that previously unknown bugs have been revealed using PAT against systems functioning …