Open Access. Powered by Scholars. Published by Universities.®
Physical Sciences and Mathematics Commons™
Open Access. Powered by Scholars. Published by Universities.®
Articles 1 - 7 of 7
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 …
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 …
Automatic Compositional Verification Of Timed Systems, Shang-Wei Lin, Yang Liu, Jun Sun, Jin Song Dong, Étienne André
Automatic Compositional Verification Of Timed Systems, Shang-Wei Lin, Yang Liu, Jun Sun, Jin Song Dong, Étienne André
Research Collection School Of Computing and Information Systems
Specification and verification of real-time systems are important research topics with crucial applications; however, the so-called state space explosion problem often prevents model checking to be used in practice for large systems. In this work, we present a self-contained toolkit to analyze real-time systems specified using event-recording automata (ERAs), which supports system modeling, animated simulation, and fully automatic compositional verification based on learning techniques. Experimental results show that our tool outperforms the state-of-the-art timed model checker.
Improved Bdd-Based Discrete Analysis Of Timed Systems, Truong Khanh Nguyen, Jun Sun, Yang Liu, Jin Song Dong, Yan Liu
Improved Bdd-Based Discrete Analysis Of Timed Systems, Truong Khanh Nguyen, Jun Sun, Yang Liu, Jin Song Dong, Yan Liu
Research Collection School Of Computing and Information Systems
Model checking timed systems through digitization is relatively easy, compared to zone-based approaches. The applicability of digitization, however, is limited mainly for two reasons, i.e., it is only sound for closed timed systems; and clock ticks cause state space explosion. The former is mild as many practical systems are subject to digitization. It has been shown that BDD-based techniques can be used to tackle the latter to some extent. In this work, we significantly improve the existing approaches by keeping the ticks simple in the BDD encoding. Taking advantage of the ‘simple’ nature of clock ticks, we fine-tune the encoding …
Probabilistic Model Checking Multi-Agent Behaviors In Dispersion Games Using Counter Abstraction, Jianye Hao, Songzheng Song, Yang Liu, Jun Sun, Lin Gui, Jin Song Dong, Ho-Fung Leung
Probabilistic Model Checking Multi-Agent Behaviors In Dispersion Games Using Counter Abstraction, Jianye Hao, Songzheng Song, Yang Liu, Jun Sun, Lin Gui, Jin Song Dong, Ho-Fung Leung
Research Collection School Of Computing and Information Systems
Accurate analysis of the stochastic dynamics of multi-agent system is important but challenging. Probabilistic model checking, a formal technique for analysing a system which exhibits stochastic behaviors, can be a natural solution to analyse multi-agent systems. In this paper, we investigate this problem in the context of dispersion games focusing on two strategies: basic simple strategy (BSS) and extended simple strategies (ESS). We model the system using discrete-time Markov chain (DTMC) and reduce the state space of the models by applying counter abstraction technique. Two important properties of the system are considered: convergence and convergence rate. We show that these …