Integrating the PVSio-web modelling and prototyping environment with Overture
Integrating the PVSio-web modelling and prototyping environment with Overture
复制标题
将 PVSio-web 建模和原型环境与 Overture 集成
DOI：
--
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
P. Larsen
中科院分区：
文献类型：
--
作者：
P. Masci;P. Curzon;P. Larsen;L. Couto;L. Couto;P. Larsen
需要克服阻碍开发团队使用正式核查技术的障碍的工具。本文介绍了我们将PVSiO-Web与VDM的Overture开发分析环境相结合的工作。PVSIO-Web是一个用于对交互系统进行建模和原型制作的图形环境。在PVSiO-web中开发的原型可以非常类似于真实系统的视觉外观和行为。原型的行为完全由可执行的正式模型驱动。这些正式模型可以从Emuchart自动生成，Emuchart是基于Statechart表示法的图形化图表。Emucharts方便地隐藏了形式语法的一些方面，这些方面给不熟悉正式方法的开发人员和领域专家造成了障碍。在这里，我们介绍了一个用于Emucharts的VDM-SL模型生成器的实现。文中给出了一个基于医疗器械的实例。它展示了使用Emucharts开发正式模型的好处，如何使用PVSiO-Web执行轻量级形式分析，以及如何使用开发的VDM-SL模型生成器来生成可以在Overture中进一步分析的模型。
Tools are needed that overcome the barriers preventing development teams using formal verification technologies. We present our work integrating PVSio-web with the Overture development and analysis environment for VDM. PVSio-web is a graphical environment for modelling and prototyping interactive systems. Prototypes developed within PVSio-web can closely resemble the visual appearance and behaviour of a real system. The behaviour of the prototypes is entirely driven by executable formal models. These formal models can be generated automatically from Emucharts, graphical diagrams based on the Statechart notation. Emucharts conveniently hides aspects of the formal syntax that create barriers for developers and domain experts who are new to formal methods. Here, we present the implementation of a VDM-SL model generator for Emucharts. An example is presented based on a medical device. It demonstrates the benefits of using Emucharts to develop a formal model, how PVSio-web can be used to perform lightweight formal analysis, and how the developed VDM-SL model generator can be used to produce a model that can be further analysed within Overture.