Open Access. Powered by Scholars. Published by Universities.®
Physical Sciences and Mathematics Commons™
Open Access. Powered by Scholars. Published by Universities.®
Articles 1 - 3 of 3
Full-Text Articles in Physical Sciences and Mathematics
Model Checking Hierarchical Probabilistic Systems, Jun Sun, Songzheng Song, Yang Liu
Model Checking Hierarchical Probabilistic Systems, Jun Sun, Songzheng Song, Yang Liu
Research Collection School Of Computing and Information Systems
Probabilistic modeling is important for random distributed algorithms, bio-systems or decision processes. Probabilistic model checking is a systematic way of analyzing finite-state probabilistic models. Existing probabilistic model checkers have been designed for simple systems without hierarchy. In this paper, we extend the PAT toolkit to support probabilistic model checking of hierarchical complex systems. We propose to use PCSP#, a combination of Hoare’s CSP with data and probability, to model such systems. In addition to temporal logic, we allow complex safety properties to be specified by non-probabilistic PCSP# model. Validity of the properties (with probability) is established by refinement checking. Furthermore, …
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, …
Developing Model Checkers Using Pat, Yang Liu, Jun Sun, Jin Song Dong
Developing Model Checkers Using Pat, Yang Liu, Jun Sun, Jin Song Dong
Research Collection School Of Computing and Information Systems
During the last two decades, model checking has emerged as an effective system analysis technique complementary to simulation and testing. Many model checking algorithms and state space reduction techniques have been proposed. Although it is desirable to have dedicated model checkers for every language (or application domain), implementing one with effective reduction techniques is rather challenging. In this work, we present a generic and extensible framework PAT, which facilitates users to build customized model checkers. PAT provides a library of state-of-art model checking algorithms as well as support for customizing language syntax, semantics, state space reduction techniques, graphic user interfaces, …