基于模型的测试应用于卫星模拟器的软件组件

文摘

运行模拟器在太空计划有一个基本的角色。卫星运行期间,这些模拟器主要用于验证关键策略,测试新的车载软件版本,支持异常的诊断。重用的目的操作模拟器,巴西国家空间研究所提出了一个新的标准规范的组件,必须集成在他们的内部开发的模拟器。新标准描述卫星的行为相关的子系统使用因果表遥控,电子开关、设备工作状态、能耗、遥测和子系统的操作模式。使用这个新标准作为输入,这项工作提出了一种方法,将基于模型的测试和模型检查来验证正确的新组件的实现卫星模拟器。验证方法包括提取状态机从因果表,用它来自动获取测试用例套件。为了验证这个提议,我们应用这三种不同的卫星子系统和评估结果的测试活动。在所有三个案例中,该方法识别错误模拟器组件起初未检测到的传统测试方法用于巴西国家空间研究所。

1。介绍

使用模拟器渗透卫星生命周期的所有阶段,从卫星的任务分析处理。在这项工作中,我们的方法的问题验证软件组件组成卫星操作模拟器,用于培训新运营商的卫星发射后,验证操作规程,测试新版本的车载软件,支持异常的诊断(1,2]。

由于高成本和精力需要开发一个操作模拟器,国家空间研究所(INPE)在巴西投资开发卫星操作模拟器,可以重用从一个任务到另一个地方,用最小的定制工作。为此,模拟器被组织在一个模块化的体系结构,模拟引擎,称为模拟器的核心,分开的软件组件相关卫星子系统、地面站、空间环境。这个体系结构如图1并采用模拟器的CBERS(中巴地球资源卫星)。

同时引入模拟器模块化的体系结构,采用一个新的规范标准在INPE描述模拟器组件与卫星相关子系统。本标准使用因果表相关的遥控、电器开关、设备工作状态、能耗、遥测和卫星子系统的运作模式。一般来说,因果表,也被称为决策表或投入产出表,输入相关条件和/或事件输出状态和/或事件。因果表规范语言的选择成为联合提议的系统工程和软件工程团队。已经成功地使用它作为一个共同语言在不同专家所涉及在INPE卫星的发展,如机械、电气和控制工程师。

使用因果表规范语言的优势是非常容易理解。它不需要特定的造型语言和知识可以共享所有的参与者之间的空间项目,包括内部专家、分包商、合作伙伴和利益相关者。相反,采用因果表作为规范语言引起测试工程师明确限制条件的测试用例描述表的行。结合序列的命令往往是被忽视和错误在模拟器上实现可能通过未被发现。这些错误可能会导致不安全的执行的命令序列在卫星的卫星,并可能导致损坏或甚至完全丧失的使命。这个问题已经观察到INPE,卫星模拟器组件的验证已经完成手册和特别的方式和强烈依赖测试人员的经验。

为了克服这个限制,这项工作提出和评估基于模型的测试方法来源于CoFI(一致性和故障注入)测试方法3]。方法接收卫星作为输入组件规范根据国家标准编写的。提出了一种循序渐进的方法翻译因果表在有限状态机中,然后提交正式的验证UPPAAL模型检测工具。最后,状态机用于生成一组测试用例,然后应用到仿真器组件。

为了评估建议的方法,我们使用三种不同的软件组件的SIMCBERS模拟器CBERS卫星(中巴地球资源卫星)的家庭。在模型检查活动,生成的测试用例套件及其应用模拟器的自动计算工具的帮助下;我们观察到的翻译方法是人工进行的,为了提供第一次实验的评价方法。工具来支持完整的流程自动化正在发展。

我们工作的主要贡献是在合并现有的验证方法和适应他们的特异性应用程序域(卫星模拟器)为了使其使用可行的产业。它考虑的限制规范语言(因果表)域,采用选定的共识专家来自不同学科中所涉及的发展卫星(热、电、轨道控制等)。

剩下的纸是组织如下:部分2简要介绍了两种验证技术建议的方法的基础。然后,部分3描述了我们的方法的步骤,而部分4分析的结果应用的三个组件SIMCBERS模拟器。部分5讨论发表作品,跟我们的建议和结果进行比较。最后,部分6得出一些结论。

2。UPPAAL CoFI方法和模型检查

CoFI基于模型的测试方法结合了一致性测试验证和故障注入。它指导建设一套粉状态机(4)代表组件的行为,与一对相关的转换(输入和输出)。状态机是用于测试用例的自动生成、后(即“黑匣子”的方法。,只有使用可控输入和可观测输出)。老渔夫执行的测试用例自动生成工具(5]。所有测试用例初始状态的开始和结束。测试用例规范包含的输入序列,以及预期的输出(oracle)的测试。图2礼物的一个例子粉状态机和两个相应的测试用例生成的老渔夫的工具。

所使用的算法ConDado始于FSM的可达性树,包含所有FSM转换。然后,对于每个树的分支,它补充了分支路径,以机器最终状态(在这个例子中,最终状态是巧合的初始状态)。考虑到数据的FSM2和3黑色所示,初始可达性树从FSM获得。灰色的过渡和节点说明的路径添加到返回初始状态S1。因此,ConData 4测试用例生成。

CoFI [3)方法论指导测试人员描述系统行为分为不同的类:正常行为,指定异常,偷偷路径和容错。每个类是一组不同的状态机模型,模型规模维持在一个可以理解的水平。在这项工作中,我们尤其关心偷偷路径。它描述了系统中会发生什么当已知输入收到意想不到的时刻。以前的作品(6,7]表明,测试用例来源于偷偷路径模型是那些最有助于识别系统在测试中的错误。偷偷路径的主要原因是没有明确规范中所描述的,因此,通常不被认为是在系统中实现。

第二个验证模型检查技术考虑我们的建议,基于状态空间模型的探索。给定一个状态转换模型和财产,模型检测算法探索详尽的状态空间模型,以确定是否满足检查属性。在我们的工作中,我们使用UPPAAL首先模拟,然后正式验证状态机获得了因果的手工表规范的文档。UPPAAL提供了一个模型,仿真和验证框架,用于实时系统(8]。在UPPAAL,系统建模为一个时间自动机网络扩展的时钟和数据类型。他们之间的交流时间自动机通过渠道和共享变量。用于验证目的,必须指定为系统需求模型属性中定义的细胞毒性t淋巴细胞(计算树逻辑),然后提交模型检测引擎。

尽管本文中给出的案例研究没有明确包括时间间隔,我们选择UPPAAL由于我们的方法扩展到实时系统的可能性。此外,UPPAAL有友好的用户界面,我们可以很容易的建立CoFI和UPPAAL之间的直接通信模型,如图所示(9),探讨了自动翻译的FSM UPPAAL自动机。

3所示。验证的方法

该方法接收作为输入的规范软件组件,它模拟卫星子系统,旨在验证后相应的实现集成到卫星模拟器。

这种方法分为4个主要步骤如图4。第一步包括提取粉从规范卫星子系统的状态机。为此,提出了手动提取方法。在下面,第二步旨在补充状态机溜路径的转换,它代表的行为系统当收到意想不到的输入。在步骤3中,粉状的状态机转换为UPPAAL的自动机和验证模型检测工具。最终规范的修正错误暗示,粉状的状态机和/或UPPAAL模型。在步骤4,粉状的抽象状态机是用于自动生成测试用例。最后,在步骤5中,抽象的测试用例自动转换为可执行的测试用例和应用于模拟器。结果分析,不合格品输出为纠正规范提供反馈,状态机,UPPAAL模型或仿真器实现。

之后,我们首先介绍标准的采用INPE描述卫星子系统的行为,如在模拟器中实现组件。然后我们详细的步骤方法,使用作为一个例子(DCS) CBERS数据采集子系统。

3.1。卫星子系统规范

卫星子系统输入文档的规范的验证过程。它由以下部分组成10]:(我)物理视图:它描述了卫星子系统的物理组件作为一个框图,包括冗余。图给出了一个例子5并说明了DCS子系统的物理架构的一部分。它是由以下设备:两个冗余转发器(Eq-A1和Eq-A2)、一个发射机盒内部冗余(Eq-B),一个天线共用器箱内部冗余(Eq-C),和两个天线(Eq-D和Eq-E)。(2)逻辑视图:礼物之间的逻辑连接遥控(确认为TCnn),电气开关(确认为SWnn)和遥测(确认为TMnnn)卫星子系统。遥控命令从地面站发送,关于卫星状态而遥测信息发送到地面站。逻辑视图是互补的物理架构和显示逻辑根据接收到的命令行是否精力充沛遥控和相应的开关状态。它还显示了如何修改遥测结果开关的状态。图6说明了配电电路的一部分,控制天线共用器,作为一个例子。开关由TC02 TC01 SW01关闭和打开。遥测TM006提供其输出的状态。(3)操作模式和工作状态:它定义了子系统的操作模式(确认为OMnn)子系统设备的操作模式(确认为EM_xx_ii)和设备的工作状态的内部组件(确认为WK_xx_ii)。子系统的操作模式是其设备操作模式的结果,这是一个组件的工作状态的结果。在DCS子系统为例,表中1提出了两种DCS的操作模式,表2展示了Eq-A1的可能的操作模式和表3带来Eq-A1组件的工作状态(应答器1和振荡器1)。(iv)能耗的观点:它描述了配电(PW)根据设备的操作模式。表4DCS子系统带来的一个例子。(v)子系统的行为:它包含因果表指定如何遥控,外部参数和开关影响遥测,组件工作状态,设备操作模式,子系统的操作模式。以下指定因果表:(一)TC⟶SW:遥控如何影响开关(在表的例子5)。(b)慢波睡眠⟶工作:交换机如何影响组件工作状态(在表的例子6)。(c)星期⟶TMs:组件工作状态如何影响遥测(例子在表7观察,不可能都同时转发器,强加的子系统设计约束)。(d)星期⟶EM:组件的工作状态如何影响设备操作模式(在表的例子8)。(e)EMs⟶OM:设备操作模式如何影响子系统的操作模式(例子在表9)。

3.2。第一步:提取状态机

第一步的验证过程包括建立一组有限状态机基于子系统的规范。这是一个手工活动,为了引导,我们提出一种提取9组成的指导活动,如图7。

我们描述每个活动如下:(我)活动1:确定子系统的操作模式(OM)。(2)活动2:把每个操作模式(OM)粉状的状态机的状态。(3)问题1系统冗余设备/频道吗?如果是的,去活动3,如果不去活动4。“渠道”这个词表示一组设备,提供了一个特定的功能和可能的冗余。在DCS的例子中,子系统有两个通道,如图5。(iv)活动3:识别冗余选项为每个子系统的操作模式。多余的选项取决于设备的系统架构,允许组合。他们的物理视图中指定子系统。复制状态的状态机的操作模式,根据冗余选项的数目。(v)活动4:确定设备操作模式(EMs)、组件工作状态(星期)和开关(慢波睡眠)配置相应状态的状态机。我们观察到这些信息添加到模型中,使更容易下一个活动。状态标签不是正式的组件的FSM和不影响测试用例生成。(vi)活动5:识别子系统之间的可能的转换操作模式(OM)。添加相应的过渡到状态机。(七)活动6:识别遥控(TCs)导致系统从一个状态到另一个地方。(八)活动7:把每个转换的输入/输出。输入是遥控(TC)中确定活动6,和输出设备操作模式(EMs),组件工作状态(星期),开关(慢波睡眠)配置中确定活动5。(第九)活动8:确定的初始位置开关(慢波睡眠)和定义相应的状态作为初始状态的粉状的状态机。

图8介绍了粉状的DCS子系统的状态机,使用描述提取获得的指导。大胆的圆表示初始和最终状态。我们观察到工作,西南、EM和OM变量是省略了为了保持模型的可读性。

3.3。步骤2:添加偷偷路径的转换

第二步是继承了CoFI方法。它由补充粉状态机有异常或意想不到的行为。为此,我们建立了通路的表。它定义了预期的输出子系统接收一个意想不到的输入,即。,任何TC没有考虑。表10提出了一种局部视图的偷偷路径表,与新的州OM02_CH1和OM04_CH1过渡。对于这两个国家,这导致增加3个新的故障状态到粉机(OMf01-CH1、OMf02-CH1 OMf07-CH1)和12个新的意想不到的转变。这些新的状态和转换时通常不覆盖测试是基于系统规范和这项工作的一个重要贡献。

偷偷的模型路径的转换呈现在图9。我们观察到工作,西南、EM和OM变量是省略了为了保持模型的可读性。

3.4。步骤3:在UPPAAL验证

第三步是将粉状的状态机转换为一个在UPPAAL自动机和验证它。转换中使用以下规则:(我)一个布尔变量中创建为每个TM UPPAAL,西南,周和OMs。(2)为每个TC创建一个频道。(3)一个自动机构建相同的粉机的状态和转换。(iv)创建第二个自动机,它可以发送TCs在任何序列,如图10。

(v)粉机转换的输入是模仿作为UPPAAL频道标有“?”,对应于一个同步转换发射由TC生成器。粉机的每个转换的输出转换为一个动作在UPPAAL更新遥测值(TMs)和其他变量(),如图11。

图12说明了导致UPPAAL模型。至于图10周,EM, OM变量是省略了为了保持模型的可读性。初始状态是OM2_CH2标有一个双重循环。这是第一次使用仿真验证。形式验证是由提交属性来检查每个状态变量值的一致性,所有状态的可达性,以及缺乏僵局。属性的例子验证使用模型检查表11。

相对应的验证过程发现25错误,不完整或错误的转换输出。一个例子是如果声明TM005 = 1是缺少一个过渡的输出,然后检查其相应的属性值在OM01_CH2是错误的。为了纠正这个错误,UPPAAL允许用户请求一个诊断跟踪会显示一系列过渡解雇使房地产虚假。通过分析,我们可以发现错误和丢失的声明添加到相应的过渡。错误和矛盾中发现UPPAAL必须纠正UPPAAL模型和粉状的状态机。

3.5。第四步:生成测试用例

一旦粉机已经纠正,这是老渔夫工具用于生成测试用例。在DCS子系统,ConDado生成444个测试用例。然而,老渔夫工具提供了抽象的测试用例,然后必须被转换成可执行的测试用例。这个活动是测试环境的强烈依赖。

在这项工作中,专用工具开发执行这个转换的情况下SIMCBERS模拟器。它有两个主要功能:(1)执行测试用例转换成适当的格式在SIMCBERS操作模拟器和(2)比较模拟器输出和相关测试神谕通过老渔夫工具自动生成。

3.6。第五步:执行测试用例

在步骤5中,我们具体的测试用例应用于卫星模拟器和寄存器输出。然后我们把输出测试用例甲骨文,由ConDado提供。比较的结果可以“成功”,说明整合模拟器产生的输出和输出测试的甲骨文,或“失败”,表示不信奉国教或失败。最后,我们分析差异来识别问题是否规范,状态机模型,或模拟器。

在DCS子系统为例,444个测试用例的执行在CBERS模拟器导致23不合格,9所造成的错误。确认表提供了错误的例子12。

4所示。案例研究和结果

为了评估该方法的贡献,我们不仅适用于DCS还从SIMCBERS另外两个子系统,CBERS[的模拟器11]。在所有三个案例中,子系统的实现在模拟器上已经提交到通常的测试活动采取在INPE SIMCBERS模块,它是由定义的一组测试基于经验的测试工程师,覆盖子系统规范的目的。

总的来说,以下CBERS子系统进行测试:(我)DCS(数据采集子系统):介绍了早期,它对应于子系统负责收集数据从数据平台散布在地面和电源地面站。(2)OBDH(车载数据处理子系统):它对应于卫星车载计算机系统。(3)SYSC(系统电路子系统):它对应于电路负责向负载提供电力。

表13总结了三种情况下的结果。它提供了测试用例的数量、测试失败,并使用该方法实现错误检测。在所有的情况下,测试活动识别实现错误SIMCBERS起初未检测到的电流检测方法。有趣的是,DCS和SYSC子系统提供了类似的结果,测试用例失败的比例相对较低。相对,OBDH很高百分比误差测试failure-this子系统实现中,由于缺少变量导致的系统性缺失信息测试用例输出。另一个有趣的观察是测试失败之间的比率的变化和实现错误。一个测试失败可以识别多个错误,或者一个错误会导致失败在多个测试用例。这是因为相关的错误通常是一个过渡。因此,所有的测试用例,执行错误的过渡将影响和失败。类似地,如果一个测试用例激活两个错误的过渡,那么都将影响测试用例的输出。

我们观察到的数量错误显示在表13不包括这些错误之前UPPAAL验证过程中检测到的,一旦他们被纠正之前的测试用例生成。

此外,我们比较获得的结果与我们的方法(方法)来获得使用原始CoFI方法(方法B),提出了(3]。测试用例从这两种方法应用于卫星模拟器。这项研究的结果发表在表14表明,在所有的3个案例研究,这项工作中提出的方法(方法一)导致大量的“失败”,因此,在检测到大量的错误。

有什么不同在B方法相比,方法是利用UPPAAL。虽然FSM的方法被UPPAAL验证,方法B没有。方法B的FSM是不完整的,缺少信息输入/输出事件的转换。因此,一些方法我们没有检测到错误的观察,虽然方法a和B的FSM是不同的,差异都在输入和输出事件相关的转换。因此,测试用例的数量是相同的这两种方法因为老渔夫工具生成的路径是一样的。路径被修改的数量只有当我们改变源或最终状态的过渡,或添加或删除从FSM的转变。补充表14和15介绍了建模错误识别在UPPAAL模型检测验证。

这两种方法的结果进行了分析使用卡方测试,以验证以下假说H₀或拒绝它(这意味着验证假说H₁)。H₀:失败测试活动中发现的数量不依赖上的方法。H₁:失败测试活动中发现的数量取决于上的方法。

我们汇总的观察和期望频率的方法,以验证假设。表16显示了期望频率,计算根据方程(1)[12对于每个案例研究: 在哪里是预期的频率,笔行吗(成功或失败),列的总和吗(方法A或B), :的所有行和列。

鉴于预期的频率,下一步是计算的预期对于每个单元格 ,根据以下方程: 在哪里是预期的频率(从表16),是观察到的频率(从表14),卡方值细胞吗 。

由此产生的问_计算与每个案例研究相关联的总和的案例研究。结果在表17为每个子系统。为了测试这个假说,问_计算是相对于问_{至关重要的}3.84,等于95%的置信度。

在DCS和OBDH的情况下,问_计算>问_{至关重要的}。这表明假设H₀强烈反对,证实该方法有助于识别更多的失败。SYSC,问_计算<问_{至关重要的},这表明,在这种情况下,该方法并没有导致故障识别的显著改善。的一个因素,可以解释子系统之间的区别是SYSC子系统的低复杂度相比OBDH和DCS。

5。相关工作

本节讨论发表作品相关的两个主要主题,结合我们的方法:因果表,也称为决策表和基于模型的测试。关于因果的表,我们现在的几个例子,从80年代早期到最近几年,这说明因果表的使用规范,实现和验证的目的。他们还表明,因果表被广泛使用和容易理解来自不同背景的人。关于基于模型的测试,我们关注的是作品,讨论他们的适用于特定的工业领域,如我们的方法。

哈里森(13)提倡使用因果表规范和系统的实现。比较我们的工作,他提出了一个逆的方法,由推导的因果表状态机。表被用作一种有效的方式实现了相应的软件。Traverso [14)提出了使用因果表获取系统的规范,然后,详尽的验证系统。他提出一个方法来获得一个完整的表与所有可能的输入和预期输出和直接从表中获取测试用例。该方法应用于铁路运输领域的案例研究。程等。15)使用I / O表来表示从FMEA分析结果。表包含正常和失效行为,被用来作为一种方法来自动获取故障树和推导测试。

在最近的工作中,Huysmans et al。16]分析了不同的造型语言的可理解性(因果表,决定真命题规则和斜规则)。作者进行了一项实验来访问终端用户认为每种语言的方式。它测量精度、响应时间和回答信心当用户需要执行不同的需要使用模型。这表明因果表在所有三个标准的表现较佳,并达显著程度,易于使用。Huysmans等人的结果证实使用因果的选择由INPE专家表来描述卫星子系统。

关于基于模型的测试,很多的文学作品描述了集成的方向努力执行基于模型的测试技术。

自动生成和执行测试套件在分布式基于组件的软件(AGEDIS)是一个由欧盟资助的为期三年的项目(17)调查的自动化软件测试活动。5在三个不同的公司进行了案例研究:IBM、电信(法国),和Intrasoft。工程结果表明,创建工具来执行和记录大量的测试用例的主要挑战时引入基于模型的测试。有关我们的工作,我们开发了一个专用工具将抽象测试用例转换成可执行的测试用例,协助测试用例执行和结果分析,克服困难与大量的测试用例相关联。

Pretschner et al。18)研究了基于模型的测试方法是否可行的在质量和成本方面,基于案例研究来自汽车行业。就质量而言,基于模型的测试用例比较手动生成测试用例。结论是基于模型的测试没有确定比手工测试用例执行失败。相反,作者观察到从模型生成的测试导致显著增加缺陷的检测要求。在工作的局限性的事实不相容的测试用例的结果手动检查,由于缺少自动工具。Pretschner等人的另一个观察是测试人员考虑了一些测试用例自动生成的模型作为“无稽之谈”,因为一开始的测试用例系统应该是一个不寻常的条件。为了避免这个问题,我们的工作中使用的工具实现了开关覆盖法,保证所有生成的测试用例离开状态机的初始状态,从而避免测试用例没有意义。

关于具体CoFI的使用基于模型的测试方法,Mattiello-Francisco et al。19),同时et al。20.]描述教训CoFI的移植方法从空间到汽车工业。指出由作品的一个挑战是细化的需要确定一个适当的水平的模型,所以他们不是很复杂,导致行不通的测试用例的数量,也不能太简化,导致表面系统的验证。另一个限制是难以解释的规范,因为规范是用自然语言编写的,给予模棱两可的空间。在我们的工作中,问题相关的细节层次模型克服了系统的规范明确地列出了输入和输出的造型。自然语言的歧义规范规避了因果表的使用,而造型困难减少通过该方法将因果表转换成状态机。

最后,两个Anjos et al。7和连接部分等。6)结合使用CoFI UPPAAL模型检测方法。但是,与我们的工作,独立的技术应用,没有任何模型的重用。在我们的工作中,模型检测是用来验证CoFI所使用的模型,对模型的正确性用于自动测试用例生成。

6。结论

这项工作提出了一个系统化的方法为组件生成测试用例的卫星模拟器是一个新的规范标准阐述了由巴西国家空间研究所(INPE)。规范是基于因果表来定义因果关系在遥控,遥测、开关、和设备状态。使用因果表的选择是来自共享规范的需要在不同领域、不同背景的人。

虽然他们很容易理解,但因果表诱导测试工程师的缺点限制的测试用例套件只有最明显的序列的遥控,危害验证过程。为了克服这个限制,这项工作提出了获得状态机从因果表,然后使用状态机模型自动生成测试用例,覆盖不同组合的事件。从因果表创建状态机的过程目前手动执行支持和CoFI方法和UPPAAL模型检查器。

CoFI方法有助于造型过程中加入新的状态和转换与意想不到的行为,结果从接收遥控意想不到的事件。他们保证卫星模拟器的鲁棒性。UPPAAL模型检查器有助于验证模型的一致性,将用于生成测试用例,避免不必要的返工由于建模误差。

一旦卫星组件对应的状态机验证,老渔夫抽象工具用于生成测试用例。专用工具开发测试用例转化为具体的测试用例,并把它应用到卫星模拟器。

为了验证该方法,我们应用它SIMCBERS三个子系统,中巴地球资源卫星的模拟器,在INPE发达。所有的三个子系统已经在INPE使用传统的测试方法在实践中验证。结果表明,在所有三个案例中,我们的方法是能够识别更多的错误,导致模拟器的鲁棒性。因此,我们可以确认,我们的方法在INPE补充目前在使用的方法,通过识别问题和错误在模拟器上实现以前未发现。

此外,比较与原CoFI方法论也为了确定UPPAAL的贡献进行验证。两个子系统,测试用例失败的数量的增加,由于模型检测被认为是具有统计学意义。在一个案例中,它不是重要的。我们相信,结果的差异是由于复杂的子系统。当造型一个子系统与冗余设备,大量的遥控,开关,和操作模式,分析员更容易引入错误。

总结该方法的贡献,引入建模步骤,将因果表转换为一个状态机,突出了系统的动态行为从多个因果表的结合。而一个因果表显示了单个事件对系统状态的影响,状态机明确显示了一系列事件的影响。使用基于模型的测试方法,如CoFI,确保测试用例覆盖多明显的命令序列相关系统的正常行为。在INPE当前使用的方法比较,我们的方法确保测试用例的集合的覆盖降低了操作者经验的依赖。

数据可用性

以下数据支持本研究的发现:卫星子系统的规格,UPPAAL模型、有限状态机、测试用例,以及测试用例的结果。DCS规范,UPPAAL模型,FSM可从相应的作者。剩余的可用性数据没有授权的国家空间研究所(INPE)由于安全的原因,因为它关系到操作卫星。

的利益冲突

作者宣称没有利益冲突。

确认

作者要感谢SIMCBERS INPE开发团队,斗篷,CNPq 306408/2014-7(过程)。

引用

1. 金龟子ECSS-European合作空间标准化、“航天工程:系统建模和仿真,”技术报告ECSS-E-TM-10-21A, ESA-ESTEC,位于荷兰,2010年。视图:谷歌学术搜索
2. j . Eickhoff“模拟航天器系统”施普林格系列在航空航天技术施普林格科学与商业媒体,柏林,德国,2009年。视图:谷歌学术搜索
3. A . m . (e·马丁斯n . l . Vijaykumar和美国诉卡瓦略,“空间应用软件服务的一致性测试过程,”《航空计算、信息和通信(JACIC),3卷,不。4、146 - 158年,2006页。视图:出版商的网站|谷歌学术搜索
4. t . Sudkamp语言和机器:介绍计算机科学的理论皮尔森,伦敦,英国,第3版,2005年版。
5. e·马丁斯,s . b . Sabiao和a . m . Ambrosio”ConData:自动化的工具基于规范的测试用例生成通信系统,”软件质量日报,8卷,不。4、303 - 320年,1999页。视图:出版商的网站|谷歌学术搜索
6. r·p·连接部分p·c·维拉a . m .(和大肠的同时,“贡献模型检查和CoFI嵌入式软件方法学的发展空间,“经验软件工程,19卷,不。1,页39 - 68,2012。视图:出版商的网站|谷歌学术搜索
7. j . m . s . Anjos g·k . Coracini和大肠的同时,“建议和验证基于虚拟仪器软件体系结构的多功能机器人末端执行器,”工程软件的进步卷,55 32-44,2013页。视图:出版商的网站|谷歌学术搜索
8. g .代表答:大卫,和k·g·拉森,“对UPPAAL教程,”第四届国际学校学报》在正式方法设计的计算机,通信和软件系统(04 SFM-RT”)Bertinoro卷。3185年,意大利,2004年9月。视图:谷歌学术搜索
9. 大肠的同时,r . p .连接部分,g . k . Coracini和a . m . Ambrosio”集成模型检测和基于模型的测试软件开发工业,”计算机在工业领域卷,104年,第102 - 88页,2018年。视图:出版商的网站|谷歌学术搜索
10. j . Tominaga c . Cerqueira j .河野,a .(“指定操作模拟器,卫星的行为”SESP学报》2012:模拟和EGSE设施空间规划馆内进行,位于荷兰,2012年9月。视图:谷歌学术搜索
11. p·d·b·席尔瓦,“Sistematizacao做证人de组件de simuladores de卫星“硕士论文,航空技术研究所、圣荷西dos坎波斯,巴西,2017年。视图:谷歌学术搜索
12. a . Agresti介绍分类数据分析新泽西州霍博肯市约翰·威利& Sons,美国,第二版,2007年版。
13. p·g·哈里森,“有效的表驱动的有限状态机实现,”系统和软件杂志》上,卷2,不。3、201 - 211年,1983页。视图:出版商的网站|谷歌学术搜索
14. A . m . Traverso”规范的工具分析:完整的决策表,“IFAC诉讼卷,18卷,不。12日,53-56,1985页。视图:出版商的网站|谷歌学术搜索
15. h . c . y . l . Cheng Wei, j .元,”I / 0表的建立故障树的自动化合成、”可靠性工程和系统安全,40卷,不。3、311 - 318年,1993页。视图:出版商的网站|谷歌学术搜索
16. j . Huysmans k . Dejaegerμ,j . Vanthienen b . Baesens,“可理解性的实证评价决策表,树和基于规则的预测模型,”决策支持系统,51卷,不。1,第154 - 141页,2011。视图:出版商的网站|谷歌学术搜索
17. 克拉格,m·萨迪斯,t . Heuillard”Agedis案例研究:基于模型的测试行业,”模型驱动的软件工程学报》1日欧洲会议2003年12月,德国纽伦堡。视图:谷歌学术搜索
18. a . Pretschner w . Prenninger s .瓦格纳et al。“一个基于模型的测试评价及其自动化”软件工程学报》第27届国际会议上,页392 - 401年,圣路易斯,密苏里州,美国,2005年5月。视图:谷歌学术搜索
19. m·f·Mattiello-Francisco大肠的同时,e·马丁斯t .南美洲b·科埃略,a . m . Ambrosio”技术转移的经验CoFI方法汽车领域,”学报第六拉丁美洲的研讨会上可靠的计算(LADC),1卷,页1 - 4,里约热内卢,巴西,2013年4月。视图:谷歌学术搜索
20. 大肠的同时,a . m . (t . a .南美洲m . v . o . Araujo和e·马丁斯,“从学术界到行业:从一个基于模型的测试经验,挑战和经验教训”学报》第45届IEEE /联合会国际会议上可靠的系统和网络(DSN 2015),1卷,页研究,里约热内卢,巴西,2015年6月。视图:谷歌学术搜索

版权

版权©2018年保罗迭戈巴博萨da Silva等。这是一个开放的分布式下文章知识共享归属许可,它允许无限制的使用、分配和复制在任何媒介,提供最初的工作是正确引用。