Name
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 the systems. To prevent these 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. For the purpose of detecting simple and typical defects in specifications, 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 present a checking method based on a satisfiability solver, and report experimental results. |
Year | DOI | Venue |
|---|---|---|
2013 | 10.1007/978-3-642-36818-9_7 | ICT-EurAsia |
Keywords | Field | DocType |
bounded strong satisfiability,strong satisfiability checking,specification phase,reactive system,satisfiability solver,realizability checking,development reworking,checking method,reactive system specification,safety-critical reactive system | Computer science,Satisfiability,Algorithm,Theoretical computer science,Linear temporal logic,Solver,Reactive system,Realizability,Bounded function | Conference |
Citations | PageRank | References |
2 | 0.38 | 9 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Masaya Shimakawa | 1 | 41 | 7.54 |
| Shigeki Hagihara | 2 | 78 | 12.33 |
| Naoki Yonezaki | 3 | 107 | 20.02 |