2009 Fiscal Year Final Research Report
Reuse of Abstraction in Model Checking
| Project/Area Number |
20700004
|
|---|
| Research Category |
Grant-in-Aid for Young Scientists (B)
|
| Allocation Type | Single-year Grants |
|---|
| Research Field |
Fundamental theory of informatics
|
|---|
| Research Institution | Tottori University of Environmental Studies |
|---|
Principal Investigator |
NISHIZAWA Koki Tottori University of Environmental Studies, 環境情報学部, 講師 (60455433)
|
|---|
| Project Period (FY) |
2008 – 2009
|
| Keywords | 情報基礎 / システム検証 / モデル検査 / 抽象化 / 多値論理 |
|---|
| Research Abstract |
There is no end to the number of problem posed by bugs of software and hardware. Model checking is the technique to verify such systems. We gives a theory to reuse'abstraction' that is efficiency technology in model checking. The cost of abstraction is high, because even if an abstraction is efficient to verify a property, it may be inefficient to verify other properties. If this result allows us to reuse abstractions, it reduces the cost of abstractions. We especially gives a theory to reuse abstractions between different multi-valued logics. The validity of abstractions is mathematically guaranteed by using theories about multi-valued logics and simulations.
The results are as follows. We give a general fixed point logic including four multi-valued logics (Frame, De Morgan Frame, Bilattice, Mied TS) as examples. Under the logic, we formulate abstractions by using `the pair of two adjunctions'and prove that the abstraction allows us to pull back results of verification. Moreover, we give the sufficient condition to reuse such abstractions.
As related work, we also analyze unary operators on multi-valued logics whose truth values form a powerset. We discover the correspondence between the hierarchy of Kleene algebras and the hierarchy of multirelations that is another representation of such unary operators.
|
