Publication Type

Conference Proceeding Article

Version

publishedVersion

Publication Date

11-2012

Abstract

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 probabilistic refinement checking is more complicated, we manage to show improvements in some cases. We have integrated these techniques into the PAT model checking framework. Experiments are conducted to demonstrate the efficiency of our approach.

Keywords

Model Check, Label Transition System, Check Algorithm Tree Automaton, Synchronous Product

Discipline

Programming Languages and Compilers | Software Engineering

Research Areas

Software and Cyber-Physical Systems

Publication

Proceedings of the 14th International Conference on Formal Engineering Methods, , ICFEM 2012, Kyoto, Japan, November 12-16

First Page

364

Last Page

380

ISBN

9783642342806

Identifier

10.1007/978-3-642-34281-3_26

Publisher

Springer Link

City or Country

Japan

Additional URL

https://doi.org/10.1007/978-3-642-34281-3_26

Download

Share

COinS