Name
Abstract | ||
|---|---|---|
Verifying realizability in the specification phase is expected to reduce the development costs of safety-critical reactive systems. If a specification is not realizable, we must correct the specification. However, it is not always obvious what part of a specification should be modified. In this paper, we propose a method for obtaining the location of flaws. Rather than realizability, we use strong satisfiability, due to the fact that many practical unrealizable specifications are also strongly unsatisfiable. Using strong satisfiability, the process of analyzing realizability becomes less complex. We define minimal strongly unsatisfiable subsets (MSUSs) to locate flaws, and construct a procedure to compute them. We also show correctness properties of our method, and clarify the time complexity of our method. Furthermore, we implement the procedure, and confirm that MSUSs are computable for specifications of reactive systems at non-trivial scales. |
Year | DOI | Venue |
|---|---|---|
2014 | 10.1145/2642937.2642968 | ASE |
Keywords | Field | DocType |
specifications,strong satisfiability,reactive systems,specification techniques,ltl,flaw-location analysis,minimal unsatisfiable subsets,formal methods,realizability,büchi automata,buchi automata | Computer science,Correctness,Satisfiability,Algorithm,Theoretical computer science,Time complexity,Reactive system,Realizability,Büchi automaton | Conference |
Citations | PageRank | References |
4 | 0.42 | 10 |
Authors | ||
4 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Shigeki Hagihara | 1 | 78 | 12.33 |
| Naoki Egawa | 2 | 4 | 0.42 |
| Masaya Shimakawa | 3 | 41 | 7.54 |
| Naoki Yonezaki | 4 | 107 | 20.02 |