基于模型检查的Web应用程序设计

理论计算机科学电子笔记151（2006）19-32www.elsevier.com/locate/entcs一种基于模型检查的Web应用程序设计Francesco Maria Donini1Universit`adellaTusciaViterbo，ItalyMarina Mongiello2Dipartimento di Elettrotecnica edElettronica Politecnico di Bari，意大利米歇尔·鲁塔3Dipartimento di Elettrotecnica edElettronica Politecnico di Bari，意大利Rodolfo Totaro4Dipartimento di Elettrotecnica edElettronica Politecnico di Bari，意大利摘要Web应用程序（WA）的开发需要新的方法，技术和工具来支持工程项目在其生命周期的所有阶段。为确保WA的可靠性，在早期设计阶段对其进行验证和验证我们使用模型检查技术来执行自动验证的WA的UML设计我们提出了一个数学模型的WA分区通常Kripke结构成窗口，链接，页面和行动。然后，我们指定要检查的时态逻辑，计算树逻辑（CTL）的属性验证是根据我们的形式主义调整SMV模型检查器来执行的嵌入SMV验证器的已实现系统自动解析UML工具的XMI输出，并构建SMV模型以根据规范进行验证。验证结果证明了该方法的益处。关键词：Web应用程序，模型检查，可靠性，验证。1571-0661© 2006 Elsevier B.V. 在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.07.03420F.M. Donini等人/理论计算机科学电子笔记151（2006）191引言Web应用程序（WAs）的发展速度使得Web工程成为一项复杂的活动，其策略仍在开发中。事实上，今天许多WA都是大规模的，涉及用户和数据库之间复杂的交互：许多组织开发了高性能的网站和应用程序，并开始使用Web作为业务工具。由于Web是一个具有快速变化特征的开放系统，Web工程（WE）尚未对其主要特征进行明确定义。它必须面对新的问题和挑战，这些问题和挑战随着基于Web的系统的新方法和方向而动态变化和发展。因此，需要设计WAs的开发在Web工程主要问题的概述中，通过软件工程（SE）的经验来学习复杂软件系统的管理是很有趣的;然而，理解WE和SE之间存在的差异也很重要。首先，基于Web的系统比软件系统更以用户为中心，事实上，用户通常可以要求在开发过程中可以轻松添加到系统中的新功能和特性;因为它特别适用于业务系统。WA的发展需要的方法和形式化，解决系统的设计，和工具，可以涵盖设计过程的各个方面考虑到工作区所开展活动的相关性，必须通过确认和核查过程确保其可靠性。本文的重点是黑箱核查。特别是，我们认为设计阶段，并提出了一种方法来检查的UML设计的正确性一般来说，方法的定义需要指定一些元素：描述要分析的对象的类的模型，表示符号技术的语言，过程模型。为了我们的目的，我们选择模型检验方法[1]，这是一种对有限状态转换系统进行合理和完整推理的技术。它根据系统模型的规范对其进行自动验证。具体化以逻辑形式主义表达，通常是时间框架内的逻辑。在过去的几十年中，这项技术已成功地应用于硬件和软件验证。模型检查的主要优点是1电子邮件：donini@unitus.it2电子邮件：mongiello@poliba.it3电子邮件：m. poliba.it4电子邮件：r. poliba.itF.M. Donini等人/理论计算机科学电子笔记151（2006）1921它可以自动执行，不像测试和其他需要用户交互的正式基于不同的形式模型，已经开发了几种用于系统分析的验证工具。对于模型检查，使用较多的是符号模型验证器（SMV）[12]和SPIN[1]。首先，我们提出了一个数学模型的WA划分通常的Kripke结构成窗口，链接，页面和动作。然后我们指定要在时态逻辑中检查的属性，即计算树逻辑（CTL）。验证是根据我们的形式主义调整SMV模型检查器来执行的。一个实现的系统嵌入了一个解析器来执行UML设计工具的XMI输出的自动翻译，并自动构建SMV模型来验证规范。论文的其余部分组织如下：在第2节中，我们描述了一些相关的工作。第3节回顾了CTL的基础知识;在第4节中，我们描述了我们为Web应用程序提出的模型，并形式化了要验证的属性。第5节和第6节分别描述了实现的系统和评估环境。最后一部分是结论和未来的发展。2相关工作据我们所知，只有少数作品考虑了Web应用程序分析;无论如何，他们中的大多数都不是基于正式的方法。我们简要介绍了更相关的建议。一些方法认为Web类似于数据库，因此提出了其结构的概念模型;最近的方法侧重于Web工程的角度来看，Web应用程序。所有建模技术的完整综述见[9]。HDM [6]是超媒体应用程序的第一个模型驱动设计之一;相继的提议是RMM[20]，Strudel [11]和Araneus[14]。它们都建立在HDM模型上，并支持特定的导航结构。特别地，Araneus描述了基于实体关系模型的数据结构.在第二个角度，即考虑一个Web应用程序作为一个软件对象，几个建模技术已被采用。Conallen [2]提出了一种基于UML的方法论。该方法的主要优点是可以使用一个标准的UML符号。OOHDM [15]是一种在WA中表示设计结构的面向对象方法。该方法将Web应用程序视为对象模型上的导航视图，并为22F.M. Donini等人/理论计算机科学电子笔记151（2006）19设计导航模型。UWE [13]是一种基于UML的面向对象、迭代和增量的方法。WebML [16]引入了用于设计Web应用程序的概念的图形和XML表示总之，所有的建议都是建模技术。要对WA进行验证，必须使用验证或测试技术。[7]中提出的方法基于WAs的UML模型，并考虑了所开发的Web系统的测试和验证。在[5]中，提出了一种基于队列模型的Web应用分析。最后，在[4]中，作者验证了使用HTML语言和ASP代码构建的Web中重复页面的正确使用。同样，所提出的方法没有考虑正式的方法。另一方面，在[3]中已经使用了基于μ-演算语言的模型检查，但是该方法没有给出动态的分析。页面.无论如何，在这项工作中，作者认为网络的模型就像一个图，其中状态是页面，状态之间的转换是页面中的因此，超链接不能像我们一样被属性限定在[19]中，自动机被用来勾勒超文本中链接的框架。因此，分支时态逻辑（超文本逻辑）HTL被定义。借助于它，可以描述自动机中状态之间的转换序列。该逻辑也被用来验证时态逻辑的命题，但同样不考虑动态页面3形式主义形式验证正迅速成为一种有前途的自动化方法，以确保软件系统的准确性和正确性。基于静态分析的验证允许指定系统的正确性，并对其进行系统和详尽的分析。在本节中，我们简要回顾了CTL [1]形式语言和SMV模型检查器[12]的基础知识。公式的语法可以使用巴科斯-诺尔形式定义如下：φ：：= p |¬φ |φ ∧ ψ |φ ∨ ψ |φ → ψ |φ ↔ ψ |EFφ |EXφ|EGφ|E（φU）|AGφ|AF φ|AXφ |A（φU）其中p是命题原子，φ，是CTL公式。任何命题逻辑公式都是CTL公式。CTL公式还包含路径量化器，后跟时间运算符。 路径量化器E指定来自当前状态的某些路径，而路径量化器A指定来自当前状态的所有路径。时态运算符是X（neXt-time运算符）、U（Until运算符）、G（全局运算符）和FF.M. Donini等人/理论计算机科学电子笔记151（2006）1923未来的运营商Xφ指定φ在路径上的下一个状态下成立，φU则指定φ在路径上的每一个状态下都成立，直到φ为真。 Gφ指定φ对路径上的每个状态都成立，Fφ指定路径上至少有一个状态φ为真。符号X、U、G、F在没有量化器E和A的情况下不能出现。该语言的语义是通过Kripke结构定义的，该结构定义了用于描述时态逻辑语义的模型。Kripke模型是三元组（S，→，L），其中S是状态的集合，→是二元关系，描述了系统可以从一个状态移动到另一个状态，并且，对于每个状态s，解释函数L提供了在该特定状态下为真的原子命题集合L（s）[10]。直觉，而时间连接词的语义如下：EFφ：一条路径，使得φ在某个Future状态下成立;E（φU）：一条路径，使得φ在某个Future状态下成立;EGφ：一条路径，使得φ沿着路径全局地成立;EXφ：φ在某个neXt状态下成立;AF φ：对于所有路径，都将有某个未来状态，其中φ成立;A（φU）：所有路径都满足φ在某个neXt状态下成立;AGφ：对于所有路径，属性φ全局地成立;AXφ：φ在每个neXt状态下成立;SMV [12]是一种用于根据表示为CTL公式的规范检查有限状态系统的工具。SMV的符号模型检验方法允许以更紧凑的方式描述模型系统的转换关系，即，，将转换关系编码为由有序二元决策图表示的布尔函数。4该模型Web的超文本结构的复杂性不能使用简单的图结构来建模，其中节点表示页面，弧表示超链接。事实上，框架的广泛使用，虽然有争议，但使窗口由几个页面组成。此外，新的实现技术，如脚本，servlets，applets增加了动态属性的网页。 因此，链接可以指向一个新窗口或在内部启动一个操作动态页面。它需要一个更紧凑和强大的模型来传达链接页面的复杂性，窗口的层次结构，链接到网页的不同媒体的类型，可以执行的操作这种情况类似于概念数据建模，其中层次和网状模型被证明不足以对结构化信息进行建模。事实上，数据库现在采用关系模型而不是使用网状或层次模型来建模。也24F.M. Donini等人/理论计算机科学电子笔记151（2006）19对于超媒体文档以及因此对于web结构，需要更强大的模型。一些方法已经考虑了Web与巨大数据库的相似性，并提出了Web上数据的实体关系模型或面向对象模型[8]。我们提出了一个数学模型的WA的基础上扩展的简单图一般采用模型页面和页面之间的链接。该模型的主要优点是它也支持WA属性的形式化验证。在以前的论文[18]，[17]中，我们提出了一个自动检查Web应用程序的模型。在这里，我们扩展了模型，可以表示页面中执行的操作更具体地说，我们提出了一个扩展的Kripke结构通常用于传达CTL的语义。将该模型转化为合适的CTL模型。这里的状态是窗口、页面、链接和动作，因为模型中的状态表示观察中可见的所有内容定义4.1Web应用程序图（WAG）是一个图G=（N，C），其中节点N被划分为N=W<$P<$L<$A（Windows，Pages，Links和Actions），使得(i) W、P、L、A是成对分布的，即，，WP=，WL=WA=LP=LA=PA=，(ii) 弧仅将窗口与页面、页面与链接或动作、链接与窗口以及动作与窗口连接，即，C<$（W×P）<$（P×（L<$A））<$（（L<$A）×W）;(iii) <$w∈W< $p ∈P：（w，p） ∈C(iv) <$x ∈（L <$A）<$w ∈ W：（x，w）∈ C“ 每 个 链 接 指 向 一个 窗 口 ， 每 个 动 作 创 建 一 个 窗 口 ” 。定义4.2导航路径是一个序列w1w2.其中n= 1 privateBAX（<$private））使用这些命题，我们可以检查Web应用程序设计的一些有趣属性例如，我们可以检查访问私有26F.M. Donini等人/理论计算机科学电子笔记151（2006）19页面通过登录发生，因此它是否正确：(i) 我们必须在登录操作后找到一些私人信息：AG（登录）(ii) 在登录操作之后，我们可以在将来进行注销操作，或者应用程序必须管理登录错误，并且必须可以再次登录：AG（login）AG（wEX（（EXlogout）error）EFlogin）(iii) 在注销操作之后，我们可以在新登录之前仅加载非私有页面：AG（logout）AG（logout）(iv) 主页必须验证以下属性：A（€privateU login）Web应用程序设计的另一个属性涉及错误管理;我们可以在错误发生时检查Web应用程序的行为。例如：(i) 对于每个未注销动作，web应用程序必须最终管理错误页面：AG（一个注销错误EXEXerror））(ii) 当发生错误时，用户必须重复登录操作AG（errorA（<$privateU login））定义4.3[Web应用程序]给定WAGG建模Web应用程序，给定初始状态s和属性p，Web应用程序验证pip对G中的s成立。我们的方法的部署实现将嵌入CTL的自动验证器中;然而，为了建立一个原型来显示该方法的可行性，验证阶段也可以使用可用的工具来执行，例如SMV。在这种情况下，验证过程包括在SMV输入语言中表达Web应用程序图-也是在参数模块的帮助下-然后启动验证。F.M. Donini等人/理论计算机科学电子笔记151（2006）1927工具UMLXMI文XMI解析器SMV文NuSMVCTL规格和属性值Fig. 1.系统架构。5一个原型系统我们提出的方法是由两个步骤组成：第一个是检查的Web应用程序在设计阶段的基础上，其UML模型。在第二步中，检查将扩展到Web应用程序实现。在第一步中，我们使用根据Conallen [2]提出的方法开发的应用程序的UML设计。在UML图中，应用程序的组件用它们的属性来标记，例如。、login、logout、private、error，以便在SMV模型中执行转换。所实现的系统嵌入了SMV验证器，以根据第4节中描述的规范检查模型。图1显示了系统的架构。将SMV集成到我们的自动化测试应用程序中具有以下优点：(i) 一旦新的SMV实现可用，它们就可以顺利地替代我们应用程序中的旧实现;(ii) 当Web应用程序的新部分被形式化为转换系统时，它们的自动转换可以独立于模型检查器来实现。XMI解析器接收一个带有规格和属性的XML文件，并自动将UML设计工具的输出转换为SMV代码，该SMV代码对相应的WAG进行建模。6评价环境为了说明这种方法背后的基本原理，让我们考虑图2中的UML设计模型。图3显示了相应的WAG。每个状态都有一个属于集合的名称{HomepageW，HomepageP，Login，Logout，ErrorW，ErrorP，ErrorLink，new1，new2，page1，page2，indexLink1，indexLink2，index1}28F.M. Donini等人/理论计算机科学电子笔记151（2006）19图二.检查Web应用程序设计的UML模型。属于集合的类型：{window，page，link，action}和属于该集合的属性：{login，logout，private，error，null}初始状态设置为：（HomepageW，window，null）图中满足节点之间链接的转换在语法上是正确的。根据第4节中描述的质量标准检查模型。验证在模型中发现了几个错误。首先，在WAG中不存在一个标有私有财产的国家，因此财产：AG（property=login->EF（property=private））并不满意。此外，在登录之后，应该可以执行注销操作，但是模型检查器通过以下规范验证了WAG中不存在注销AG（property=login->AG（type=window->（EX（（EX（property=logout）|（property=error））|EF（property=login）这一点没有得到证实。为了解决这个问题，有必要引入一个链接到页面的注销操作下面的图4显示了WAGF.M. Donini等人/理论计算机科学电子笔记151（2006）1929错误W错误PWp，误差主页W主页P登录Wpa、登录联系我们page1New1指数LpWppage2New2联系我们pWL图三. WAG对应于图2所示的UML模型。见图4。在第一次验证后，WAG进行了修改。这是第一步验证的结果。因此，进行了第二个验证阶段。其他规范未得到验证，例如，关于登录操作的规范：AG（property=logout）->A[property！=私人Uproperty=login]）因为缺少到HomepageW的链接，该链接可以允许跟随链接到登录动作。最后，为了满足有关误差管理的性质，必须修改模型以下30F.M. Donini等人/理论计算机科学电子笔记151（2006）19错误W错误P错误链接Wp，误差L注销网站首页主页P登录a、注销Wpa、登录联系我们page1New1指数Lp，私有w，私有ppage2New2联系我们pWL图五.在验证后修改了WAG。不符合质量标准：AG（property=error -> A[property！= private U property=login]）statename=HompageW A[property！= private U property=login] AG（type=window property=private）->EX（property=private））在注销之后，必须能够再次登录，因此模型检查器系统发现缺少将注销状态连接到主页的弧。图5显示了在检查所有属性之后修正的模型。相应的UML设计模型如图6所示。7结论和今后的工作在本文中，我们提出了一个正式的模型验证的UML设计WA。该方法基于模型检查，并且在模型上要验证的属性以CTL表示所提出的方法已被验证，通过实施一个原型系统，嵌入SMV模型检查器。 系统解析作为UML设计工具的输出获得的XMI代码，并构建SMV模型，其中属性被验证。验证结果证明了该方法的益处。我们目前正在努力扩展该模型的用户特征。 正在扩展要检查的属性，以便验证可访问性。F.M. Donini等人/理论计算机科学电子笔记151（2006）1931见图6。根据验证过程纠正UML模型。引用[1] E.M.克拉克，O.M. Grumberg和D.A. Peled。模型检查。MIT Press，1999.[2] J·科纳伦使用UML构建Web应用程序。艾迪森·韦斯利出版公司，Reading，Masssetts，2002.[3] L.德·阿尔法罗万维网模型检查。在第13届计算机辅助验证国际会议（CAV'01）的会议记录中[4] G. Di Lucca和M.迪潘塔一种识别重复网页的方法。第26届国际计算机软件和应用年会，第481 -486页[5] M.迪彭塔湾安东诺夫湾Casazza和E.梅洛通过队列模型建立Web维护中心模型。第五届欧洲软件维护和再工程会议，第131 - 139页[6] D.施瓦布湾Garzotto，P. Paolini.基于模型的超文本应用程序设计方法。ACM TOIS，11（1）：1[7] P. Tonella F.瑞卡Web应用程序的测试过程。软件工程年鉴，14（1）：93[8] D. Florescu，A.题名其余部分：A.万维网数据库技术综述。SIGMODR，27（3）：59[9] P. 兄弟开发数据密集型网络应用程序的工具和方法：综述。ACM Computing Survey，31（3）：227[10] M.R.A. Huth和M.D.瑞恩计算机科学中的逻辑剑桥大学出版社，1999年。[11] J. 姜阿义李维F. Fernandez，D.Florescu和D.苏丘用果馅卷搭船在ACM-SIGMOD，第414-425页[12] K.L.麦克米兰SMV系统，1992年2月。http://www.cs.cmu.edu/搜索modelcheck/smv/smvmanual.r2.2.ps。[13] A.克劳斯·N科赫基于uml的web工程的表现力。在IWOOST '02，2002的Proc.32F.M. Donini等人/理论计算机科学电子笔记151（2006）19[14] G.麦加P.Atzeni和P.Meriado。 设计和维护数据密集型网站。 在Proc. of EDBT-98，第436-450页[15] G. Rossi和D.施瓦布Web应用程序模型中的面向对象设计结构软件工程年鉴，13（1）：97-110，2002。[16] P.Fraternali S.Ceri和Maristella Matera。数据密集型web应用的概念建模。IEEE InternetComputing，6（4）：20[17] E. Di Sciascio，F M. Donini，M. Mongiello和G.皮斯泰利Anweb：一个自动支持Web应用程序验证的系统。Seke '02的Proc.ACM，纽约，2002年7月。[18] E. Di Sciascio，F.M. Donini，M. Mongiello和G.皮斯泰利基于符号模型检测的Web应用程序设计与维护 在proc 的CSMR '03，第63-72页，意大利贝内文托，2003年3月26-28日。美国电气与电子工程师协会。[19] 警局斯托茨和JC古田作为自动机的超文档：通过模型检查验证基于跟踪的浏览属性。TOIS，16（1）：1[20] E.斯托尔Isakowitz和P. Balasubramanian。结构化超媒体设计方法论。ACM，38（8）：34