Ghosh, Priyankar ; Ramesh, B ; Banerjee, Ansuman ; Dasgupta, Pallab (2009) Abstraction refinement for state space partitioning based on auxiliary state machines In: TENCON 2009 - 2009 IEEE Region 10 Conference, 23-26 January 2009, Singapore.
Full text not available from this repository.
Official URL: http://ieeexplore.ieee.org/document/5395794/
Related URL: http://dx.doi.org/10.1109/TENCON.2009.5395794
Abstract
Counter-example guided abstraction refinement (CEGAR) techniques have been primarily used to scale the capacity of formal property verification. This paper explores the utility of CEGAR for verifying an emerging style of formal specifications, called AuxSM+properties, which consists of auxiliary state machines (AuxSMs) and formal properties based on the AuxSMs. A core challenge in formally verifying these specifications is in partitioning the states of the design-under-test (DUT) into sets which map into the different states of the AuxSM. In this paper we present a CEGAR approach for solving this problem without explicitly traversing the entire state space of the DUT.
| Item Type: | Conference or Workshop Item (Paper) |
|---|---|
| Source: | Copyright of this article belongs to Institute of Electrical and Electronics Engineers. |
| Keywords: | State-Space Methods; Protocols; Labeling; Computer Science; Design Engineering; Space Technology; Design Automation; Refining; Partitioning Algorithms; Formal Specifications |
| ID Code: | 101669 |
| Deposited On: | 12 Dec 2016 09:58 |
| Last Modified: | 12 Dec 2016 09:58 |
Repository Staff Only: item control page
