...
  • 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>Science of Computer Programming >Experiences with formal engineering: Model-based specification, implementation and testing of a software bus at Neopost
【24h】

Experiences with formal engineering: Model-based specification, implementation and testing of a software bus at Neopost

机译：正规工程方面的经验：Neopost上基于模型的规范，软件总线的实现和测试

获取原文
获取原文并翻译 | 示例
           
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

We report on the actual industrial use of formal methods during the development of a software bus. During an internship at Neopost Inc., of 14 weeks, we developed the server component of a software bus, called the XBus, using formal methods during the design, validation and testing phase: we modeled our design of the XBus in the process algebra mCRL2, validated the design using the mCRL2-simulator, and fully automatically tested our implementation with the model-based test tool JTorX. This resulted in a well-tested software bus with a maintainable architecture. Writing the model (m_(dev)), simulating it, and testing the implementation with JTorX only took 17% of the total development time. Moreover, the errors found with model-based testing would have been hard to find with conventional test methods. Thus, we show that formal engineering can be feasible, beneficial and cost-effective. The findings above, reported earlier by us in (Sijtema et al., 2011) [1], were well-received, also in industrially oriented conferences (Ferreira and Romanenko, 2010) [2] and [3]. In this paper, we look back on the case study, and carefully analyze its merits and shortcomings. We reflect on (1) the added benefits of model checking, (2) model completeness and (3) the quality and performance of the test process. Thus, in a second phase, after the internship, we model checked the XBus protocol-this was not done in [ 1 ] since the Neopost business process required a working implementation after 14 weeks. We used the CADP tool evaluator4 to check the behavioral requirements obtained during the development. Model checking did not uncover errors in model m_(dev), but revealed that model m_(dev) was neither complete nor optimized: in particular, requirements to the so-called bad weather behavior (exceptions, unexpected inputs, etc.) were missing. Therefore, we created several improved models, checked that we could validate them, and used them to analyze quality and performance of the test process. Model checking was expensive: it took us approx. 4 weeks in total, compared to 3 weeks for the entire model-based testing approach during the internship. In the second phase, we analyzed the quality and performance of the test process, where we looked at both code and model coverage. We found that high code coverage (almost 100%) is in most cases obtained within 1000 test steps and 2 minutes, which matches the fact that the faults in the XBus were discovered within a few minutes. Summarizing, we firmly believe that the formal engineering approach is cost-effective, and produces high quality software products. Model checking does yield significantly better models, but is also costly. Thus, system developers should trade off higher model quality against higher costs.
机译：我们报告了在软件总线开发过程中正式方法在工业上的实际使用情况。在Neopost Inc.进行的为期14周的实习期间，我们在设计，验证和测试阶段使用正式方法开发了软件总线的服务器组件，称为XBus：在流程代数mCRL2中对XBus的设计进行了建模。 ，使用mCRL2-simulator验证了设计，并使用基于模型的测试工具JTorX全自动测试了我们的实现。这导致了具有可维护架构的经过良好测试的软件总线。编写模型（m_（dev）），对其进行仿真以及使用JTorX测试实现仅花费了总开发时间的17％。此外，使用传统的测试方法很难发现基于模型的测试中发现的错误。因此，我们表明正式工程是可行，有益和具有成本效益的。上述发现，早些时候由我们在（Sijtema et al。，2011）[1]中报道，在以工业为导向的会议中也受到了好评（Ferreira and Romanenko，2010）[2]和[3]。在本文中，我们回顾了案例研究，并仔细分析了它的优缺点。我们思考（1）模型检查的附加好处，（2）模型完整性和（3）测试过程的质量和性能。因此，在第二阶段，实习后，我们对XBus协议进行了模型化-在[1]中未完成此操作，因为Neopost业务流程需要14周后才能正常工作。我们使用了CADP工具评估程序4来检查在开发过程中获得的行为要求。模型检查未发现模型m_（dev）中的错误，但显示模型m_（dev）既未完成也未优化：尤其是缺少对所谓的恶劣天气行为（异常，意外输入等）的要求。 。因此，我们创建了几个改进的模型，检查了是否可以验证它们，并使用它们来分析测试过程的质量和性能。模型检查非常昂贵：大约花费了我们的时间。总共需要4个星期，而整个实习期间，整个基于模型的测试方法需要3个星期。在第二阶段，我们分析了测试过程的质量和性能，同时研究了代码和模型的覆盖范围。我们发现，在大多数情况下，可以在1000个测试步骤和2分钟内获得较高的代码覆盖率（几乎100％），这与在几分钟之内发现XBus的错误这一事实相吻合。总而言之，我们坚信正式的工程方法具有成本效益，并且可以生产高质量的软件产品。模型检查确实可以产生更好的模型，但代价也很高。因此，系统开发人员应权衡较高的模型质量与较高的成本。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号