Sismic-用于状态图执行和测试的Python库

+软件X 12（2020）100590原始软件出版物Sismic-用于状态图执行和测试的Python库Alexandre Decan，Tom Mens比利时蒙斯大学软件工程实验室ar t i cl e i nf o文章历史记录：收到2019年收到修订版2020年3月9日接受2020年保留字：Statechart可执行模型行为驱动的开发契约式运行时验证a b st ra ctStatecharts是一种众所周知的可视化建模语言，用于表示复杂的基于事件的反应式系统的可执行行为。状态图模型的本质复杂性要求对高级模型测试和验证技术的需求，例如测试驱动的开发、行为驱动的开发、契约设计以及用于在状态图执行期间监视违反行为属性的属性状态图。Sphinx是一个开源Python库，提供了一个工具套件，可以使用所有上述技术来定义，模拟，执行和测试状态图©2020作者（S）。由爱思唯尔公司出版这是CC BY许可下的开放获取文章（http://creativecommons.org/licenses/by/4.0/）中找到。当前代码版本代码元数据当前代码版本1.4.1（提交d61e748）用于此代码版本的代码/存储库的永久链接https://github.com/ElsevierSoftwareX/SOFTX_2019_181Code Ocean compute capsule不适用GNU Lesser General Public Licence version 3.0（LGPLv3）使用git的代码版本控制系统使用Python的软件代码语言、工具和服务编译要求，操作环境依赖性Python 3.5;ruamel.yaml，schema，behave，typing如果可用，链接到开发人员文档/手册https://sismic.readthedocs.io问题支持电子邮件alexandre. lexpage.net当前可执行软件版本软件元数据当前软件版本1.4.1此版本可执行文件的永久链接https://github.com/AlexandreDecan/sismicGNU Lesser General Public Licence version 3.0（LGPLv3）计算平台/操作系统Linux，OS X，Microsoft Windows安装要求依赖性Python 3.5+;ruamel.yaml，schema，behave，typing如果可用，链接到用户https://sismic.readthedocs.io问题支持电子邮件alexandre. lexpage.net1. 动机和意义Statecharts是一种可视化的可执行建模语言，由David Harel[1]引入，作为具有Mealy和Moore*通讯作者。电子邮件地址：alexandre. umons.ac.be（A.Decan），tom. umons.ac.be（T.Mens）。https://doi.org/10.1016/j.softx.2020.100590自动机Statecharts是UML标准的一部分，它构成了一种流行的符号，用于表示复杂的基于事件的反应式系统的可执行行为。它们经常在工业中用于实时系统和嵌入式系统的开发，依赖于商业工具，如IBM RationalRhapsody ， The MathworksStateflow ， itemisYakinduStat-echartTools，IARSystemsvisualSTATE和QuantumLeapsQM。这些工具中的大多数都支持状态图的可视化、修改和模拟，以及从状态图生成代码2352-7110/©2020作者。 由Elsevier B.V.出版。这是一篇开放获取的文章，使用CC BY许可证（http://creativecommons.org/licenses/by/4.0/）。可在ScienceDirect上获得目录列表SoftwareX期刊主页：www.elsevier.com/locate/softxA. Decan和T. 男士软件X 12（2020）1005902模型更高级的工具还支持模型调试和模型验证。各种各样的测试技术和相关工具可用于开发编程语言的源代码这些技术包括测试驱动开发（TDD）[2]，行为驱动开发（BDD）[3]和契约设计（DbC）[4]。这些技术已经证明了它们对“经典”编程语言的有用性。由于状态图形式主义是图灵完备的[5]，因此这些技术在可执行状态图的开发过程中也是为了这个目的，我们开发了一个模块化的Python库，用于执行、测试和验证可执行的状态图，它基于TDD、BDD、DbC和属性状态图的技术Sockets的目标是有兴趣在软件开发项目中探索和实践这些技术的研究人员和从业者。Sunday提供了一个灵活的API，以方便在常规Python代码中使用，或方便其他研究人员对其进行扩展。在[6]中，已通过受控用户研究验证了SSPRIT，并由多家公司使用。2. 软件描述Python是一个用于Python（3.5或更高版本）的状态图库，提供了一组工具来定义，执行和测试状态图。该库通过Python包索引分发。1它的源代码可以在GitHub2上获得，开源许可证为LGPLv3。sign在sismic上有大量的文档。我的意思是，我的意思是，我的意思是，io并附带了一个具有高代码覆盖率的广泛测试套件。文档中的测试、示例和代码片段作为持续集成过程的一部分自动执行。2.1. 软件功能基于对人类友好的YAML标记语言，Sort提供了一种简单的方法来定义和导入状态图。这些状态图的可视化是通过PlantUML接口实现的。Sunday默认解释器使用内部优先/源状态和运行到完成语义（也称为bigstep语义[7]），但是可以通过子类化该解释器来将其调整为其他语义。为了支持定时事件，解释器配备了可控制的模拟时钟，支持实时和模拟时间。Statechart动作和保护可以使用常规Python代码作为动作语言来表达，但是Sort也可以扩展为支持其他动作语言。Sign还支持状态图之间的通信，以及允许从状态图内部调用常规Python代码，反之亦然。关于状态图测试，Sunday支持状态图的常规单元测试; DbC方法来指定状态和转换的不变量，前置和后置条件[4]; BDD [3];以及对表示为状态图本身的行为属性的运行时检查1 pypi.org/project/sismic网站。2 github.com/AlexandreDecan/sismic网站。2.2. 软件构架Scrum提供了一个模块化的、易于扩展的体系结构，如图1所示 。 1. 一 、 有 经 验 的 Python 开 发 人 员 可 以 选 择 通 过 sis-mic.modelAPI直接创建和操作状态图。在实践中，使用基于文本的标记编辑器或外部可视化编辑器创建统计图表，并通过sismic.io导入这些模型会更方便。此API支持将状态图导出到PlantUML（plantuml.com），以便通过自动布局功能对其进行可视化 这就是Fig. 2已生成。social为了执行状态图模型，必须实例化解释器。这个解释器依赖于一个动作代码计算器以执行状态图规范的动作或保护中包含的任何代码。模块sismic.code提供了这样一个求值器来使用常规Python表达动作代码。该解释器支持对合约执行的运行时监控。使用操作代码计算器支持的语言，将协定直接指定为状态图描述的一部分，并且可以使用一系列预定义的谓词。该解释器还提供了内置的支持运行时监控表示为状态图属性。这些属性被表示为状态图，状态图根据被消耗或发送的事件，或者根据被监视的状态图进入或退出的状态，来表示预期行为的功能属性。最后，模块sismic.bdd通过提供一种灵活的方式来定义、映射和执行BDD场景，从而提供对BDD的支持。3. 说明性示例为了说明SNOW的使用，考虑图2中简化的微波控制器的例子，它是用PlantUML可视化地呈现的。下面的代码片段显示了此状态图的YAML描述的一部分：状态图：名称：简易微波控制器根状态：名称：微波控制器初始：门关闭onentry：timer =0states：-名称：开门进入时：send-event：door_closedtarget：doorclosed这个状态图可以通过API调用Sundayfrom sismic.io import import_from_yamlfrom sismic.interpreter import解释器statechart = import_from_yaml（filepath在解释器中断言合约被定义为状态图的一部分在运行时，解释器将验证合约指定的条件。下面的示例显示了微波炉的“烹饪"状态的合同合同：- 前一个：计时器> 0- after：received（'door_opened'）or timer == 0A. Decan和T. 男士软件X 12（2020）1005903Fig. 1. 高级架构概述。图二. 简化的微波控制器的可视化表示。Sodium支持BDD，由领域专家用自然语言表达场景或测试用例。这使设计师能够专注于模型的目的，而不是技术细节。给定适当的映射，以下场景可以由Synchronous使用命令行实用程序sismic-bdd执行和检查：场景：烹饪时加热打开，如果我打开门我把东西放进烤箱关上门当我按下开始按钮时，我按下增加计时器按钮5次然后打开暖气4. 影响我们已经进行了一项受控用户研究，以评估使用Sockets定义、验证和测试可执行状态图的可行性、有用性和充分性[6]。该研究的13名参与者表示，Sunday实施的技术易于使用。收到的反馈提供的证据表明，BDD场景和运行时监控合同和属性状态图是有益的状态图设计。大多数参与者表示，他们很可能在未来使用这些技术来创建新的状态图，或验证或修改现有的。几家公司正在成功地使用Socks，特别是用于模型在环测试和仿真，用于工作流和业务流程支持，以及用于并发分布式状态图的执行和验证。我们还在课堂上使用Score来向本科生教授可执行的行为建模。由于Python是状态图执行引擎的纯Python实现，因此其性能主要取决于底层Python引擎的性能。通过建设，是解释器中的解释器，因此，与普通Python代码相比有一些开销。到目前为止，还没有任何一个用户报告过与性能相关的任何限制。可以通过对状态图测试的更高级的自动化支持来扩展状态图，例如从场景生成状态图，为给定状态图生成合同（类似于在程序上自动生成合同[8]），从合同规范生成测试[9]，在状态图级别使用突变测试和concolic测试[10，11]，检测和改进状态图和合同规范中的质量问题，以及等等5. 结论总而言之，Python是一个开源和可扩展的Python库，完全支持定义和执行statecharts，这些statecharts可以使用一系列技术进行验证，包括单元测试，行为驱动开发，契约设计和属性statecharts，用于监视执行期间违反行为属性的竞合利益作者声明，他们没有已知的竞争性财务利益或个人关系，可能会影响本文报告的工作确认本文是在FNRS资助的优秀科学项目O.0157. 18F-RG 43“SECO-Assist '"的背景下进行的A. Decan和T. 男士软件X 12（2020）1005904引用[1] 哈雷尔湾关于视觉形式主义。Commun ACM 1988;31（5）：514网址：//dx.doi.org/10.1145/42411.42414网站。[2] 贝克湾测试驱动开发的例子。Addison-Wesley; 2002年，http：//dx.doi.org/10.5555/579193网站。[3] 北湾行为修正：行为驱动开发的演变。Better Softw2006.[4] 迈 耶 湾 使 用 “ 契 约 式 设 计 ” 。 IEEE Comput 1992;25 （ 10 ） ： 40-51.http://dx.doi.org/10.1109/2.161279网站。[5] 卢华，于世.关于国家统计局的计算能力。 在：计算机科学基础国际会议（FCS）的程序。Citeseer; 2011，p. 1.一、[6] Mens T，Decan A，Spanoudakis NI.一种用于测试和验证可执行状态图模型的方法。软件系统模型2019;18（2）：837网址：//dx.doi.org/10.1007/s10270-018-0676-3网站。[7]Esmaeilsabzali S，Day NA，Atlee JM，Niu J.解构语义学 一种大型建模语言。Requir Eng 2010;15（2）：235网址：//dx.doi.org/10.1007/s00766-010-0102-z网站。[8]Ernst MD，Perkins JH，Guo PJ，McCamant S，Pacheco C，Tschantz MS，Xiao C.用于动态检测可能不变量的daikon系统。 科学计算计划2007;69（1-3）：35-45. http://dx.doi.org/10.1016/j.scico的网站。2007.01.015。[9] 迈 耶 湾 合 同 驱 动 的 发 展 。 In ： Int'l conf. fundamental approaches tosoftware engineering （ FASE ） . Lect. notes in computer science ， vol.4422 ， Springer; 2007 ， p. 11.http://dx.doi.org/10.1007/978-3-540-71289-3_2.[10] Fabbri SCPF，Maldonado JC，Sugeta T，Masiero PC.突变测试应用于验证基于状态图的规范。In：Int'l symp.软件可靠性工程（ISSRE）IEEEComputerSociety;1999，p.210-9.http://dx.doi.org/10.1109/ISSRE.1999.809326网站。[11]森·K Concolic测试In：Int'l conf.自动化软件工程。 ACM; 2007年，第571-2页。http://dx.doi.org/10.1145/1321631.1321746网站。