Modeling and verification of web software based on theories symbolic computation

基于符号计算理论的Web软件建模与验证

• 批准号: 20300001
• 负责人: IDA Tetsuo
• 金额: $ 12.23万
• 依托单位: University of Tsukuba
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research (B)
• 财政年份: 2008
• 资助国家: 日本
• 起止时间: 2008 至 2011
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-20300001/
• 关键词: ソフトウェア検証; 記号計算; ウェブ; 情報基礎; ソフトウェア; 検証; ソフトウェア学

As a case study of Web software verification, we have verified the core of WebEos. The effective verification was conducted by utilizing some results of the computation conducted on Mathematica. With respect to the verification based on string analysis, we developed the method to precisely analyze regular expression matching. By introducing the analysis of communication to database, we enabled the detection of stored XSS. We designed and implemented an algorithm of greedy regular expression matching based on position automata.

作为Web软件验证的案例研究，我们已经验证了Webeos的核心。通过利用对Mathematica进行的计算结果进行有效验证。关于基于字符串分析的验证，我们开发了精确分析正则表达匹配的方法。通过将通信分析引入数据库，我们启用了存储的XSS的检测。我们根据位置自动机设计并实施了一种贪婪的正则表达式匹配算法。

项目成果

Linear Systems for Regular Hedge Languages

常规对冲语言的线性系统

• 发表时间: 2010
• 期刊: Advances in Databases and Information Systems. Associated Workshops and Doctoral Consortium of ADBIS 2009. Proceedings. LNCS 5968
• 作者: Mircea Marin;Temur Kutsia
• 通讯作者: Temur Kutsia

Origami Fold as Algebraic Graph Rewriting.

折纸折叠作为代数图重写。

• 发表时间: 2010
• 期刊: Journal of Symboli Computation 45(4)
• 作者: Tetsuo Ida;Hidekazu Takahashi
• 通讯作者: Hidekazu Takahashi

A Translation from the HTML DTD into a Regular Hedge Grammar

从 HTML DTD 到常规模糊限制语法的翻译

• 发表时间: 2008
• 期刊: Proc. of the 13th International Conference on-Implementation and Application of Automata LNCS 5184
• 作者: T. Nishiyama;Y. Minamide
• 通讯作者: Y. Minamide

Copy-on-Write in the PHP Langauge

PHP 语言中的写时复制

• 发表时间: 2009
• 期刊: Proc. of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
• 作者: Tozawa;M. Tatsubori;T. Onodera;Y. Minamide
• 通讯作者: Y. Minamide

動的に生成されるHTML文書の妥当性検査

验证动态生成的 HTML 文档

• 发表时间: 2008
• 作者: 上原伸介;小林隆志;大須賀俊憲;山本晋一郎;阿草清滋;西山拓哉,南出靖彦
• 通讯作者: 西山拓哉,南出靖彦