Algebraic Specification Approach to Model-Checking with Constraints
| Project/Area Number |
17500028
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Research Field |
Software
|
|---|
| Research Institution | National Institute of Informatics |
|---|
Principal Investigator |
NAKAJIMA Shin National Institute of Informatics, Information Systems Architecture Science Research Division, Professor (60350211)
|
|---|
| Project Period (FY) |
2005 – 2007
|
| Project Status |
Completed (Fiscal Year 2007)
|
| Budget Amount *help |
¥3,700,000 (Direct Cost: ¥3,400,000、Indirect Cost: ¥300,000)
Fiscal Year 2007: ¥1,300,000 (Direct Cost: ¥1,000,000、Indirect Cost: ¥300,000)
Fiscal Year 2006: ¥1,400,000 (Direct Cost: ¥1,400,000)
Fiscal Year 2005: ¥1,000,000 (Direct Cost: ¥1,000,000)
|
|---|
| Keywords | Software Engineering / Software Development Methods / Modeling / Verification / Model-Checking / Algebraic Specification / Data Constraints / ソフトウェア開発効率 |
|---|
| Research Abstract |
Model-checking is a promising approach to the automatic verification of software design It searches exhaustively a finite-state space to check if a given LTL formula is satisfied. The number of states to be explored becomes large, resulting in a state-space explosion problem, when a certain data variable makes effects on the control flow. We focus on a new method for avoiding the problem by integrating the idea of data constraints with the model-checking. In the proposed method, individual data values are not expanded, but the condition on the data variable is represented symbolically as a data constraint. Since the method deals with the symbolic representation, the state-space explosion problem can be avoided. We employ the algebraic specification language Maude as the underlying infrastructure because the algebraic techniques have been known as providing systematic mechanism to define complex data in a uniform manner. Our results can be summarized as below.
1. Constraint automaton is defined as an extension of Mealy-style automaton to integrate the notion of data constraints, which is then implemented on Maude.
2. Constraint automaton can successfully represent and analyze the three example cases ; interval constraints, distributed sorting, and Hotel key problem.
3. Constraint automaton can be extended to include timing issues, by using RT-Maude as its underlying infrastructure. We have set up next research agenda to apply the constraint automaton to the analysis of behavioral aspects of Event-B descriptions.
|
Report
(4 results)
Research Products
(15 results)
