2010 Fiscal Year Self-evaluation Report
Modeling and verification of web software based on theories of symbolic computation
| Project/Area Number |
20300001
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (B)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Research Field |
Fundamental theory of informatics
|
|---|
| Research Institution | University of Tsukuba |
|---|
Principal Investigator |
IDA Tetsuo University of Tsukuba, 大学院・システム情報工学研究科, 教授 (70100047)
|
|---|
| Project Period (FY) |
2008 – 2011
|
| Keywords | ソフトウェア検証 / 記号計算 / ウェブ |
|---|
| Research Abstract |
ウェブソフトウェアには従来にない高い信頼性が要求される.単に誤りなく動作するだけでなく,頑健である,悪用・誤用されないといった性質がウェブソフトウェアに求められる.このような「健全性」を保証するには従来の開発手法やデバッグ手法だけでは不十分であり,産業界や学術研究機関で新たな方法論の構築や方法論を支援する言語やツールの開発が進められている
本研究では,記号計算の理論,形式言語・オートマトン理論をはじめとする,コンピュテーションやソフトウェアを形式化する様々な理論を駆使して,上記問題の解決に取り組んでいる.具体的には,定理証明支援系やモデル検査系を用いた方法論の高度化と広範な展開が重要課題であると考え,これまで定理証明支援系を用いたソフトウェアや幾何オブジェクト設計の正当性証明の研究を推進してきた.それと同時に,記号計算を支援するウェブサービスのシステムやサーバーサイドの記号計算アルゴリズムをクライアント(ブラウザー)から対話的にアクセスするウェブソフトウェアを構築してきた
これらの先行するあるいは同時に進展させている研究で私達が得てきた知見や経験及び記号計算の研究コミュニティーが蓄積してきた多くの知見をウェブソフトウェアの「健全性」の検証に活用して,新たな計算理論,方法論,および方法論を支援するツール群を構築している
|
Research Products
(9 results)
-
-
-
[Journal Article]2010
Author(s)
松本宗太郎, 南出靖彦
-
Journal Title
Rubyプログラムの制御フロー解析とその健全性の証明 3巻
Pages: 9-25
Peer Reviewed
-
-
-
-
-
-
