Nothing Special   »   [go: up one dir, main page]

IEICE Transactions on Information and Systems
Online ISSN : 1745-1361
Print ISSN : 0916-8532
Regular Section
Bounded Strong Satisfiability Checking of Reactive System Specifications
Masaya SHIMAKAWAShigeki HAGIHARANaoki YONEZAKI
Author information
JOURNAL FREE ACCESS

2014 Volume E97.D Issue 7 Pages 1746-1755

Details
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.

Content from these authors
© 2014 The Institute of Electronics, Information and Communication Engineers
Previous article Next article
feedback
Top