Bounded verification of Ruby on Rails data models
Bounded verification of Ruby on Rails data models
复制标题
Ruby on Rails 数据模型的有限验证
DOI：
10.1145/2001420.2001429
复制
发表时间：
2011
期刊：
影响因子：
--
通讯作者：
T. Bultan
中科院分区：
文献类型：
--
作者：
J. Nijjar;T. Bultan
使用脚本语言构建Web应用程序提高了程序员的生产力，但代价是降低了可靠性。在本文中，我们专注于一类出现在Web应用程序中的错误，这些应用程序是基于模型-视图-控制器架构构建的。我们的目标是自动发现Ruby on Rails应用程序中的数据模型错误。为此，我们创建了一个自动翻译器，可以将Ruby on Rails应用程序中的数据模型表达式转换为正式规范。特别是，我们的翻译器将Active Records规范（用于在Ruby on Rails应用程序中指定数据模型）作为输入，并生成Alloy语言的数据模型作为输出。然后，我们使用有界验证技术实现的合金分析仪，寻找这些正式的数据模型规范中的错误。我们将我们的方法应用于两个开源Web应用程序，以证明其可行性。
The use of scripting languages to build web applications has increased programmer productivity, but at the cost of degrading dependability. In this paper we focus on a class of bugs that appear in web applications that are built based on the Model-View-Controller architecture. Our goal is to automatically discover data model errors in Ruby on Rails applications. To this end, we created an automatic translator that converts data model expressions in Ruby on Rails applications to formal specifications. In particular, our translator takes Active Records specifications (which are used to specify data models in Ruby on Rails applications) as input and generates a data model in Alloy language as output. We then use bounded verification techniques implemented in the Alloy Analyzer to look for errors in these formal data model specifications. We applied our approach to two open source web applications to demonstrate its feasibility.