Open Access. Powered by Scholars. Published by Universities.®
Physical Sciences and Mathematics Commons™
Open Access. Powered by Scholars. Published by Universities.®
Articles 1 - 9 of 9
Full-Text Articles in Physical Sciences and Mathematics
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 …
Towards Expressive Specification And Efficient Model Checking, Jin Song Dong, Jun Sun
Towards Expressive Specification And Efficient Model Checking, Jin Song Dong, Jun Sun
Research Collection School Of Computing and Information Systems
System modeling is important and highly non-trivial. The choice of specification language is an important factor in the success of the entire development. The language should cover several facets of the requirements and the model should precisely capture (up to abstraction of irrelevant details) an existing system or a system to be built. The language should have a semantic model suitable to study the behaviors of the system and to establish the validity of desired properties. A formal model can be the basis for a variety of system development activities, e.g., system simulation, visualization, verification or prototype synthesis.
Verification Of Population Ring Protocols In Pat, Yang Liu, Jun Pang, Jun Sun, Jianhua Zhao
Verification Of Population Ring Protocols In Pat, Yang Liu, Jun Pang, Jun Sun, Jianhua Zhao
Research Collection School Of Computing and Information Systems
The population protocol model has emerged as an elegant paradigm for describing mobile ad hoc networks, consisting of a number of nodes that interact with each other to carry out a computation. One essential property of self-stabilizing population protocols is that all nodes must eventually converge to the correct output value, with respect to all possible initial configurations. It has been shown that fairness constraints play a crucial role in designing population protocols. The Process Analysis Toolkit (PAT) has been developed to perform verifications under different fairness constraints efficiently. In particular, it can handle global fairness, which is required for …
Integrating Specification And Programs For System Modeling And Verification, Jun Sun, Yang Liu, Jin Song Dong, Chunqing Chen
Integrating Specification And Programs For System Modeling And Verification, Jun Sun, Yang Liu, Jin Song Dong, Chunqing Chen
Research Collection School Of Computing and Information Systems
High level specification languages like CSP use mathematical objects as abstractions to represent systems and processes. System behaviors are described as process expressions combined with compositional operators, which are associated with elegant algebraic laws for system analysis. Nonetheless, modeling systems with non-trivial data and functional aspects using CSP remains difficult. In this work, we propose a modeling language named CSP# (short for communicating sequential programs) which integrates high-level modeling operators with low-level procedural codes, for the purpose of efficient mechanical system verification. We demonstrate that data operations can be modeled as terminating sequential programs, which can be composed using high-level …
Fair Model Checking With Process Counter Abstraction, Jun Sun, Yang Liu, Abhik Roychoudhury, Shanshan Liu, Jin Song Dong
Fair Model Checking With Process Counter Abstraction, Jun Sun, Yang Liu, Abhik Roychoudhury, Shanshan Liu, Jin Song Dong
Research Collection School Of Computing and Information Systems
Parameterized systems are characterized by the presence of a large (or even unbounded) number of behaviorally similar processes, and they often appear in distributed/concurrent systems. A common state space abstraction for checking parameterized systems involves not keeping track of process identifiers by grouping behaviorally similar processes. Such an abstraction, while useful, conflicts with the notion of fairness. Because process identifiers are lost in the abstraction, it is difficult to ensure fairness (in terms of progress in executions) among the processes. In this work, we study the problem of fair model checking with process counter abstraction. Even without maintaining the process …
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 …
A Formal Framework For Modeling And Validating Simulink Diagrams, Chunqing Chen, Jin Song Dong, Jun Sun
A Formal Framework For Modeling And Validating Simulink Diagrams, Chunqing Chen, Jin Song Dong, Jun Sun
Research Collection School Of Computing and Information Systems
Simulink has been widely used in industry to model and simulate embedded systems. With the increasing usage of embedded systems in real-time safety-critical situations, Simulink becomes deficient to analyze (timing) requirements with high-level assurance. In this article, we apply Timed Interval Calculus (TIC), a realtime specification language, to complement Simulink with TIC formal verification capability. We elaborately construct TIC library functions to model Simulink library blocks which are used to compose Simulink diagrams. Next, Simulink diagrams are automatically transformed into TIC models which preserve functional and timing aspects. Important requirements such as timing bounded liveness can be precisely specified in …
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 …