Synchronization Verification in System-Level Design with ILP Solvers
Summary :
Concurrency is one of the most important issues in system-level design. Interleaving among parallel processes can cause an extremely large number of different behaviors, making design and verification difficult tasks. In this work, we propose a synchronization verification method for system-level designs described in the SpecC language. Instead of modeling the design with timed FSMs and using a model checker for timed automata (such as UPPAAL or KRONOS), we formulate the timing constraints with equalities/inequalities that can be solved by integer linear programming (ILP) tools. Verification is conducted in two steps. First, similar to other software model checkers, we compute the reachability of an error state in the absence of timing constraints. Then, if a path to an error state exists, its feasibility is checked by using the ILP solver to evaluate the timing constraints along the path. This approach can drastically increase the sizes of the designs that can be verified. Abstraction and abstraction refinement techniques based on the Counterexample-Guided Abstraction Refinement (CEGAR) paradigm are applied.
- Publication
- IEICE TRANSACTIONS on Fundamentals Vol.E89-A No.12 pp.3387-3396
- Publication Date
- 2006/12/01
- Publicized
- Online ISSN
- 1745-1337
- DOI
- 10.1093/ietfec/e89-a.12.3387
- Type of Manuscript
- Special Section PAPER (Special Section on VLSI Design and CAD Algorithms)
- Category
- System Level Design
Authors
Keyword
Latest Issue
Copyrights notice of machine-translated contents
The copyright of the original papers published on this site belongs to IEICE. Unauthorized use of the original or translated papers is prohibited. See IEICE Provisions on Copyright for details.
Cite this
Copy
Thanyapat SAKUNKONCHAK, Satoshi KOMATSU, Masahiro FUJITA, "Synchronization Verification in System-Level Design with ILP Solvers" in IEICE TRANSACTIONS on Fundamentals,
vol. E89-A, no. 12, pp. 3387-3396, December 2006, doi: 10.1093/ietfec/e89-a.12.3387.
Abstract: Concurrency is one of the most important issues in system-level design. Interleaving among parallel processes can cause an extremely large number of different behaviors, making design and verification difficult tasks. In this work, we propose a synchronization verification method for system-level designs described in the SpecC language. Instead of modeling the design with timed FSMs and using a model checker for timed automata (such as UPPAAL or KRONOS), we formulate the timing constraints with equalities/inequalities that can be solved by integer linear programming (ILP) tools. Verification is conducted in two steps. First, similar to other software model checkers, we compute the reachability of an error state in the absence of timing constraints. Then, if a path to an error state exists, its feasibility is checked by using the ILP solver to evaluate the timing constraints along the path. This approach can drastically increase the sizes of the designs that can be verified. Abstraction and abstraction refinement techniques based on the Counterexample-Guided Abstraction Refinement (CEGAR) paradigm are applied.
URL: https://global.ieice.org/en_transactions/fundamentals/10.1093/ietfec/e89-a.12.3387/_p
Copy
@ARTICLE{e89-a_12_3387,
author={Thanyapat SAKUNKONCHAK, Satoshi KOMATSU, Masahiro FUJITA, },
journal={IEICE TRANSACTIONS on Fundamentals},
title={Synchronization Verification in System-Level Design with ILP Solvers},
year={2006},
volume={E89-A},
number={12},
pages={3387-3396},
abstract={Concurrency is one of the most important issues in system-level design. Interleaving among parallel processes can cause an extremely large number of different behaviors, making design and verification difficult tasks. In this work, we propose a synchronization verification method for system-level designs described in the SpecC language. Instead of modeling the design with timed FSMs and using a model checker for timed automata (such as UPPAAL or KRONOS), we formulate the timing constraints with equalities/inequalities that can be solved by integer linear programming (ILP) tools. Verification is conducted in two steps. First, similar to other software model checkers, we compute the reachability of an error state in the absence of timing constraints. Then, if a path to an error state exists, its feasibility is checked by using the ILP solver to evaluate the timing constraints along the path. This approach can drastically increase the sizes of the designs that can be verified. Abstraction and abstraction refinement techniques based on the Counterexample-Guided Abstraction Refinement (CEGAR) paradigm are applied.},
keywords={},
doi={10.1093/ietfec/e89-a.12.3387},
ISSN={1745-1337},
month={December},}
Copy
TY - JOUR
TI - Synchronization Verification in System-Level Design with ILP Solvers
T2 - IEICE TRANSACTIONS on Fundamentals
SP - 3387
EP - 3396
AU - Thanyapat SAKUNKONCHAK
AU - Satoshi KOMATSU
AU - Masahiro FUJITA
PY - 2006
DO - 10.1093/ietfec/e89-a.12.3387
JO - IEICE TRANSACTIONS on Fundamentals
SN - 1745-1337
VL - E89-A
IS - 12
JA - IEICE TRANSACTIONS on Fundamentals
Y1 - December 2006
AB - Concurrency is one of the most important issues in system-level design. Interleaving among parallel processes can cause an extremely large number of different behaviors, making design and verification difficult tasks. In this work, we propose a synchronization verification method for system-level designs described in the SpecC language. Instead of modeling the design with timed FSMs and using a model checker for timed automata (such as UPPAAL or KRONOS), we formulate the timing constraints with equalities/inequalities that can be solved by integer linear programming (ILP) tools. Verification is conducted in two steps. First, similar to other software model checkers, we compute the reachability of an error state in the absence of timing constraints. Then, if a path to an error state exists, its feasibility is checked by using the ILP solver to evaluate the timing constraints along the path. This approach can drastically increase the sizes of the designs that can be verified. Abstraction and abstraction refinement techniques based on the Counterexample-Guided Abstraction Refinement (CEGAR) paradigm are applied.
ER -
English
