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
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 …
Prts: An Approach For Model Checking Probabilistic Real-Time Hierarchical Systems, Jun Sun, Yang Liu, Songzheng Song, Jin Song Dong, Xiaohong Li
Prts: An Approach For Model Checking Probabilistic Real-Time Hierarchical Systems, Jun Sun, Yang Liu, Songzheng Song, Jin Song Dong, Xiaohong Li
Research Collection School Of Computing and Information Systems
Model Checking real-life systems is always difficult since such systems usually have quantitative timing factors and work in unreliable environment. The combination of real-time and probability in hierarchical systems presents a unique challenge to system modeling and analysis. In this work, we develop an automated approach for verifying probabilistic, real-time, hierarchical systems. Firstly, a modeling language called PRTS is defined, which combines data structures, real-time and probability. Next, a zone-based method is used to build a finite-state abstraction of PRTS models so that probabilistic model checking could be used to calculate the probability of a system satisfying certain property. We …
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 …