Open Access. Powered by Scholars. Published by Universities.®
Physical Sciences and Mathematics Commons™
Open Access. Powered by Scholars. Published by Universities.®
Articles 1 - 5 of 5
Full-Text Articles in Physical Sciences and Mathematics
Symbolic Model-Checking Of Stateful Timed Csp Using Bdd And Digitization, Truong Khanh Nguyen, Jun Sun, Yang Liu, Jin Song Dong
Symbolic Model-Checking Of Stateful Timed Csp Using Bdd And Digitization, Truong Khanh Nguyen, Jun Sun, Yang Liu, Jin Song Dong
Research Collection School Of Computing and Information Systems
Stateful Timed CSP has been recently proposed to model (and verify) hierarchical real-time systems. It is an expressive modeling language which combines data structure/operations, complicated control flows (modeled using compositional process operators adopted from Timed CSP), and real-time requirements like deadline and within. It has been shown that Stateful Timed CSP is equivalent to closed timed automata with silent transitions, which implies that the timing constraints of Stateful Timed CSP can be captured using explicit tick events, through digitization. In order to tackle the state space explosion problem, we develop a BDD-based symbolic model checking approach to verify Stateful Timed …
On Combining State Space Reductions With Global Fairness Assumptions, Shao Jie Zhang, Jun Sun, Jun Pang, Yang Liu, Jin Song Dong
On Combining State Space Reductions With Global Fairness Assumptions, Shao Jie Zhang, Jun Sun, Jun Pang, Yang Liu, Jin Song Dong
Research Collection School Of Computing and Information Systems
Model checking has established itself as an effective system analysis method, as it is capable of proving/dis-proving properties automatically. Its application to practical systems is however limited by state space explosion. Among effective state reduction techniques are symmetry reduction and partial order reduction. Global fairness often plays a vital role in designing self-stabilizing population protocols. It is known that combining fairness and symmetry reduction is nontrivial. In this work, we first show that global fairness, unlike weak/strong fairness, can be combined with symmetry reduction. We extend the PAT model checker with the technique and demonstrate its usability by verifying recently …
Model Checking A Model Checker: A Code Contract Combined Approach, Jun Sun, Yang Liu, Bin Cheng
Model Checking A Model Checker: A Code Contract Combined Approach, Jun Sun, Yang Liu, Bin Cheng
Research Collection School Of Computing and Information Systems
Model checkers, like any complex software, are subject to bugs. Unlike ordinary software, model checkers are often used to verify safety critical systems. Their correctness is thus vital. Verifying model checkers is extremely challenging because they are always complicated in logic and highly optimized. In this work, we propose a code contract combined approach for checking model checkers and apply it to a home-grown model checker PAT. In this approach, we firstly embed programming contracts (i.e., pre/post-conditions and invariants) into its source code, which can capture correctness of model checking algorithms, underlying data structures, consistency between different model checking parameters, …
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 …
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 …