Bounded Strong Satisfiability Checking of Reactive System Specifications
Summary :
Many fatal accidents involving safety-critical reactive systems have occurred in unexpected situations that were not considered during the design and test phases of development. To prevent such accidents, reactive systems should be designed to respond appropriately to any request from an environment at any time. Verifying this property during the specification phase reduces development reworking. This property of a specification is commonly known as realizability. Realizability checking for reactive system specifications involves complex and intricate analysis. The complexity of realizability problems is 2EXPTIME-complete. To detect typical simple deficiencies in specifications efficiently, we introduce the notion of bounded strong satisfiability (a necessary condition for realizability), and present a method for checking this property. Bounded strong satisfiability is the property that, for all input patterns represented by loop structures of a given size k, there is a response that satisfies a given specification. We report a checking method based on a satisfiability solver, and show that the complexity of the bounded strong satisfiability problem is co-NEXPTIME-complete. Moreover, we report experimental results showing that our method is more efficient than existing approaches.
- Publication
- IEICE TRANSACTIONS on Information Vol.E97-D No.7 pp.1746-1755
- Publication Date
- 2014/07/01
- Publicized
- Online ISSN
- 1745-1361
- DOI
- 10.1587/transinf.E97.D.1746
- Type of Manuscript
- PAPER
- Category
- Software System
Authors
Masaya SHIMAKAWA
Tokyo Institute of Technology
Shigeki HAGIHARA
Tokyo Institute of Technology
Naoki YONEZAKI
Tokyo Institute of Technology
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
Masaya SHIMAKAWA, Shigeki HAGIHARA, Naoki YONEZAKI, "Bounded Strong Satisfiability Checking of Reactive System Specifications" in IEICE TRANSACTIONS on Information,
vol. E97-D, no. 7, pp. 1746-1755, July 2014, doi: 10.1587/transinf.E97.D.1746.
Abstract: Many fatal accidents involving safety-critical reactive systems have occurred in unexpected situations that were not considered during the design and test phases of development. To prevent such accidents, reactive systems should be designed to respond appropriately to any request from an environment at any time. Verifying this property during the specification phase reduces development reworking. This property of a specification is commonly known as realizability. Realizability checking for reactive system specifications involves complex and intricate analysis. The complexity of realizability problems is 2EXPTIME-complete. To detect typical simple deficiencies in specifications efficiently, we introduce the notion of bounded strong satisfiability (a necessary condition for realizability), and present a method for checking this property. Bounded strong satisfiability is the property that, for all input patterns represented by loop structures of a given size k, there is a response that satisfies a given specification. We report a checking method based on a satisfiability solver, and show that the complexity of the bounded strong satisfiability problem is co-NEXPTIME-complete. Moreover, we report experimental results showing that our method is more efficient than existing approaches.
URL: https://global.ieice.org/en_transactions/information/10.1587/transinf.E97.D.1746/_p
Copy
@ARTICLE{e97-d_7_1746,
author={Masaya SHIMAKAWA, Shigeki HAGIHARA, Naoki YONEZAKI, },
journal={IEICE TRANSACTIONS on Information},
title={Bounded Strong Satisfiability Checking of Reactive System Specifications},
year={2014},
volume={E97-D},
number={7},
pages={1746-1755},
abstract={Many fatal accidents involving safety-critical reactive systems have occurred in unexpected situations that were not considered during the design and test phases of development. To prevent such accidents, reactive systems should be designed to respond appropriately to any request from an environment at any time. Verifying this property during the specification phase reduces development reworking. This property of a specification is commonly known as realizability. Realizability checking for reactive system specifications involves complex and intricate analysis. The complexity of realizability problems is 2EXPTIME-complete. To detect typical simple deficiencies in specifications efficiently, we introduce the notion of bounded strong satisfiability (a necessary condition for realizability), and present a method for checking this property. Bounded strong satisfiability is the property that, for all input patterns represented by loop structures of a given size k, there is a response that satisfies a given specification. We report a checking method based on a satisfiability solver, and show that the complexity of the bounded strong satisfiability problem is co-NEXPTIME-complete. Moreover, we report experimental results showing that our method is more efficient than existing approaches.},
keywords={},
doi={10.1587/transinf.E97.D.1746},
ISSN={1745-1361},
month={July},}
Copy
TY - JOUR
TI - Bounded Strong Satisfiability Checking of Reactive System Specifications
T2 - IEICE TRANSACTIONS on Information
SP - 1746
EP - 1755
AU - Masaya SHIMAKAWA
AU - Shigeki HAGIHARA
AU - Naoki YONEZAKI
PY - 2014
DO - 10.1587/transinf.E97.D.1746
JO - IEICE TRANSACTIONS on Information
SN - 1745-1361
VL - E97-D
IS - 7
JA - IEICE TRANSACTIONS on Information
Y1 - July 2014
AB - Many fatal accidents involving safety-critical reactive systems have occurred in unexpected situations that were not considered during the design and test phases of development. To prevent such accidents, reactive systems should be designed to respond appropriately to any request from an environment at any time. Verifying this property during the specification phase reduces development reworking. This property of a specification is commonly known as realizability. Realizability checking for reactive system specifications involves complex and intricate analysis. The complexity of realizability problems is 2EXPTIME-complete. To detect typical simple deficiencies in specifications efficiently, we introduce the notion of bounded strong satisfiability (a necessary condition for realizability), and present a method for checking this property. Bounded strong satisfiability is the property that, for all input patterns represented by loop structures of a given size k, there is a response that satisfies a given specification. We report a checking method based on a satisfiability solver, and show that the complexity of the bounded strong satisfiability problem is co-NEXPTIME-complete. Moreover, we report experimental results showing that our method is more efficient than existing approaches.
ER -
English
