符号实时系统测试的测试用例合成方法

理论计算机科学电子笔记130（2005）79-100www.elsevier.com/locate/entcs符号实时系统Ahmed Khoumsi Ahmed Khoumsi1，2舍布鲁克大学电气与计算机工程系Sherbrooke J1K2R1，加拿大摘要我们研究符号实时系统的测试用例合成。通过符号，我们的意思是被测实现（IUT）的规范包含变量和参数。实时是指IUT的规格包含时序约束。我们的方法结合并推广了以前的工作中提出的两种测试方法，即：1）（非符号）实时系统的测试用例合成方法，和2）（非实时）符号系统的测试用例合成方法关键词：测试用例综合，实时测试，符号测试，时间输入输出符号自动机，测试体系结构。1介绍一致性测试（或更简单地说，测试）旨在检查被测实现（IUT）是否符合IUT所需行为的正式规范。测试活动包括：根据规范合成（或生成）测试用例，并在IUT上执行。我们研究的合成阶段，但我们也提出了一个测试架构的执行阶段。在现有的测试工作中，我们对以下两项互补工作感兴趣：[1]这项工作是在我9月访问法国雷恩的IRISA时开始的。 2002年至2003年8月。2电子邮件：Ahmed. USherbrooke.ca1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.03.00680A. Khoumsi/Electronic Notes in Theoretical Computer Science 130（2005）79实时系统的测试（或实时测试）：IUT的规范包含IUT与其环境之间交互的顺序和时间约束。在过去的几年中，已经开发了几种实时测试方法[7，24，4，21，9，20，5，6，16，19]。符号系统测试（或符号测试）：IUT的规格包含变量和参数。已经开发了一些符号测试方法[23，22，8]。这些方法旨在避免生成所有变量都被实例化的测试用例。请注意，符号技术也在测试以外的其他领域得到了发展，例如，模型检验[3]和诊断[26]。我们提出了一种测试综合方法，它结合了实时测试和符号测试，从而扩展了它们.我们的动机是希望为不需要实例化变量的实时系统（即，不需要枚举它们的可能值）。我们首先定义了时间输入输出符号自动机（Tiosa）模型，增加了时间到IOSTS模型[23]，并用于建模规范的IUT。我们采用两步走的方法：步骤1：我们将测试问题表达为非实时形式，通过将Tiosa转换为称为Set-Exp-IOSA（SEiosa）的自动机。SetExp表示这样的变换，并且SetExp（A）表示通过Ti osaA的变换获得的SEi osa。SetExp基本上向Tiosa的结构中添加了两种额外类型的操作：分别对时钟的设置和过期进行建模的Set和Exp第1步：我们采用[23]的非实时符号测试方法。正如我们将看到的，我们的方法的优点是它的简单性，因为实时方面的主要处理集中在一个步骤中。本文其余部分的结构如下。节2描述了用于描述IUT规格的Tiosa模型。节中 3、我们正式定义了要解决的测试问题。节 4介绍了SE iosa模型和“Se tE xp：T i o sa › → SE i o s a“转换。 在Sect中。 5.提出了一种测试体系结构，并给出了与SetExp相关的定理。节6呈现一种基于SetExp的测试方法。在第7节中，我们结束了论文。2定时IOSA（Tiosa）在本节中，我们将介绍用于描述IUT及其规范的时间输入输出符号自动机（Tiosa）。TIOSA是[16]的时间自动机和[23]的输入输出符号转换系统（IOSTS）A. Khoumsi/Electronic Notes in Theoretical Computer Science 130（2005）79812.1时钟及相关概念时钟Ci是实变量，其值可以随着动作的发生而重置（到0），并且使得在两次重置之间，其导数（w.r.t.时间）等于1。设H={c1，···，cNc}是一组时钟.时钟保护（CG）是形式为“c i k“的公式的合取< CG可以是常量True（空合取）。令ΦH是使用H的时钟的CG的集合。时钟复位是H的子集，2H表示时钟复位的集合2.2数据和相关概念变量是一种数据，其值可以随着动作的发生而设置设V是一组变量。常数是在初始时间设置一次值的数据。 设C是一组常数。（通信）参数是作为动作的参数传输的数据。设P是一组参数。Data Guard（DG）是一个布尔表达式，使用D=V C P的数据。令ΓD表示数据保护的集合（我们认为True∈ΓD）。变量赋值（VA）是赋值v：=E的集合，其中v∈ V并且E是依赖于D的表达式。 设ΛD为VA的集合。每个x∈ D的定义域记为Type（x）。2.3蒂奥萨省TIOSA由（L，l0，H，D，I，T）定义，其中：L是位置的有限集合，l0是初始位置，H是时钟的有限集合，D=V <$C <$P是数据的有限集合，I是依赖于V <$C的布尔表达式，称为初始条件，A是一个有限的动作集合，T 这是一个过渡关系。对于每个a∈与表示为θa的参数（可能为空）的元组（p1，···，pk）相关联。a的签名表示为Sig（a），定义如下：⎧Type（p1）···Type（pk）如果a是输入或输出Sig（a）=如果a是内部操作，则为空元组有三种动作：接收包含元组θi的输入i，写？i（θi）;发送包含元组θo的输出o，写！o（θo）;以及内部作用a的发生，记作θa。θi和82A. Khoumsi/Electronic Notes in Theoretical Computer Science 130（2005）79θo在为空时省略。 接收输入和发送输出是可观察的动作，而内部动作的发 生 是 不 可 观 察 的 动 作 。 TIOSA 的 转 移 定 义 为Tr=q;r;σ;θσ;CG;Zσ;DG;VAσ，其中：q和r是起点和终点位置;σ是形式为？我，！o或a;θσ是与σ相关的参数元组（可能为空）;CG和Zσ是时钟保护和时钟复位;DG和VA是数据保护和变量赋值，定义为V Cθσ。3Zσ中的下标σ意味着跃迁的时钟重置仅取决于其动作。这个限制保证了Tiosa的可确定性[16]。图 1 通 过 一 个 例 子 说 明 了 Tiosa 位 置 由 节 点 表 示 ， 并 且 过 渡Tr=θq;r;σ;θσ;CG;Zσ;DG;VAσ由连接q和r的箭头表示，并以3行标记为：σ（θσ），（CG;Zσ）和（DG;VA）。CG和DG True以及Zσ或VA的不存在由“-"指示n ={φ，α，β，ρ}，H={c1}，V={x}，C={p}，P={m}，并且x，p，m是整数。φ不能是内部动作，因为它包含参数m，其他动作可以是任何类型。Fig. 1. 例如，Tiosa2.4TIOSA的语义在时间τ0= 0时，T i osaA=（L，l0，H，D，I，T，T）在位置l0处，其中所有时钟等于0，并且变量和常数取使得I评估为真的值。当q是当前位置并且CG和DG两者均评估为时，A的转变Tr = Δq; r; σ; θ σ; CG; Z σ;DG; VAσ被启用。否则，Tr被禁用。从该位置q，仅当Tr被使能4时才可以执行动作σ（包含θσ的参数）;并且在执行σ：到达位置r之后，重置Zσ中的时钟（如果有的话），并且应用VA中的分配（如果有的话）3注意，过渡Tr =∑q;r;σ;θσ;CG;Zσ;DG;VA的DG和VA定义为：V <$C <$θσ而不是在整个D= V <$C <$P中4 但是当Tr被使能时，σ不一定被执行。L3（m）l0（− ; −）（）下一页− ;x：=mL1（−;{c1}）（− ;L2（c1>3;−）（− ; −）L4A. Khoumsi/Electronic Notes in Theoretical Computer Science 130（2005）7983一一对于图1的示例，设δu，v是动作u和v之间的延迟：• 蒂奥萨最初在位置10。 在φ（m）出现时，位置l1变量x被赋值为m。• 从l1开始，在α出现时，Tiosa达到l2。• 从l2开始，在β出现时，Tiosa达到l3或l4。只有当δα，β3和x≥p时才能达到l3，只有当δα，β>2和x≤p时才能达到l4。我们看到当2<δα，β 3和x=p时存在非决定性。当达到L4• 从13层开始，蒂奥萨什么都不执行• 从l4开始，在ρ出现时，Tiosa达到l1。我们有δα，ρ>3。TiosaA的语义也可以由A接受的定时迹集来定义。以下是一些必要的定义：定时动作是一对（e，τ），其中e是动作，τ是e发生的时刻。当e是一个输入时（（1）“行”是“行”，“行”是“行”。定时输出、定时内部）动作。定时序列是定时动作的（有限或无限）序列<<<<“（e1，τ1）···（ei，τi）···“，其中0τ1···τi···。定时跟踪是通过删除定时序列的所有定时内部操作从定时序列中获得的。对给定的时间序列λt=（e1，τ1）（e2，τ2）···，对e1，e2，··· ∈τ，可接受.设n是λt的长度（n可以是无限的），λti=（e1，τ1）···（ei，τi）是长度为i的λt的前缀，其中0≤i≤n（i是有限的）。λt被A i接受<$λt是空序列λt0或A有一个长度为n的连续转移序列Tr1 Tr2···，从l0开始，使得Tri= 1， 2，···，n：Tri的动作是ei，在执行λti−1之后，Tri在时间τi被使能。直观地说，λt对应于A的一次执行。接受定时迹：设μt=（e1，τ1）（e2，τ2）···为定时迹。μt被A接受i μt是通过删除A接受的定时序列的所有定时内部动作而获得的。直觉，μt对应于对A的执行的观察。定义2.1TiosaA（TOLTiosa）的时间可观察语言是A接受的一组定时跟踪。也就是说，TOLTIOSA对可观察的A的行为。我们将考虑的Tiosa类满足以下假设：假设2.1T iosa A接受的无限时间序列是非zeno的，即，无限数量的动作不能在有限的时间间隔内执行84A. Khoumsi/Electronic Notes in Theoretical Computer Science 130（2005）79SUniv一注2.2与[1]不同，在我们的模型中，连续的动作不能同时发生。实际上这并不是一个限制，因为我们认为如果一个动作e后面跟着一个动作f，那么e和f不是同时的。3待解决的为了严格定义要解决的测试问题，有必要正式定义Tiosa和测试目的概念之间的一致性关系。检验假设也是必要的。3.1Tiosa和一些相关引理之间的关联关系在下面的公式中：I和S表示在同一个字母表上的两个Ti osa s，并且o是一个输出动作。我们定义以下一致性关系：定义3.1I confTIOSAS表示，λ∈TOLTiosa：（λ·（o，τ）∈ TOLTiosa）（λ·（o，τ）∈ TOLTiosa）.I S如果IUT由I建模，则为了给配置Tiosa一个更简单的定义，让我们首先定义T iosa的输入完成。让我？是字母表的输入集合，Univ是一个“通用”T iosa，接受上的所有定时迹。也就是说，TOLTIOSA包含了每个定时跟踪超过。下面的定义是从[11，12]中得到的启发。定 义 3.2TiosaA= （ L ， l0 ， H ， D ， I ， T ， T ） 的 输 入 完 成 是 TiosaInpComp（A），它包含A的所有定时迹线，以及通过执行A不接受的输入而从A的定时迹线偏离的所有定时迹线。形式上，InpComp（A）是TIOSA，使得：蒂奥萨InpComp（A）2019 -05-2200：00：00w∈TOLTiosa，a∈N，w·a/∈TOLTiosa，x∈TOLTiosaw·a·x）。一个？一UnivA表示输入完成i A=InpComp（A）。Intuitable，一个完整的输入TIOSA随时接受所有输入。引理3.3（IconfTiosaS）惠（IconfTiosaInpComp（S））.引理3.3意味着我们可以在检查Ti osaI是否符合它之前用它的输入完成来替换Ti osaS，w.r.t. 请与我联系。然而，Def. 3.2不是建设性的，我们不知道如何计算InpComp（S））在一般情况下从一个TIOSAS因此，我们将使用以下假设：TOLA. Khoumsi/Electronic Notes in Theoretical Computer Science 130（2005）7985假设3.1在“I confTiosa S” ， 我们 假设 S 输入 完成。注意引理3.3和Hyp.3.1是从它们的非实时和非符号（即，没有时钟和数据）版本[11]。引理3.4假设3.1：I confTS惠TOLTiosaTOLTiosa.约萨引理3.4意味着在假设3.1中，confTiosa被简化为包含T iosa的时间可观察语言。3.2测试目的和测试假设为了定义测试目的，让我们首先定义完成陷阱：定义3.5ATiosaA=（L，l0，H，D，I，I，T）被称为是完备的：对于每个可能的时钟值和数据值，在l中启用e。直观地说，一个完整的Tiosa在任何时候都接受每一个（输入，输出或内部）动作。定义3.6陷阱位置q是这样一个位置，在该位置上，对于每个事件σ ∈θ，都存在一个自环转换Tr = σq; q; σ; θ σ; True;True。也就是说，当到达陷阱时，它永远不会离开，并且任何时候都可以从它执行每个操作定义3.7测试目的是用于选择要测试的行为的TiosaTP通过与[10，23，16]类比，TP是完整的，确定性的，并配备了两组陷阱位置A和R（接受和拒绝）。在测试活动中要考虑的定时序列是那些终止于位置A且不经过位置A的定时序列，而要忽略的定时序列是那些经过或终止于位置R的定时序列。测试目的用于在应用测试生成方法之前选择规范的一部分（因此，忽略其余部分）下面的测试假设来自[25]：假设3.2 IUT可以用（可能未知的）输入完整来蒂奥萨IUT。3.3测试问题给定相同字母表上的两个Tiosa sSpec和TP，分别描述规范和测试目的，目标是合成自动机CTG（完整测试图），从中可以提取并执行测试用例，以确定是否：IUT配置TiosaSpec。86A. Khoumsi/Electronic Notes in Theoretical Computer Science 130（2005）79我们假设Spec输入完成（参见Hyp. 3.1）。CTG是一个有趣的自动化工具，因为它包含了与TP相对应的Spec的所有测试用例。测试系统通过忽略Spec接受的IUT（即，λ∈TOLTiosa），并且：aIUTSpecTPTP的位置R可以由λ到达，或者TP的位置A不可达在λ之后，通过Spec.4将Tiosa转化为SEiosa一种称为SetExp的变换在[18]中给出，并在[13，16，17，14，15]中应用。SetExp基本上通过向TA的结构添加两种额外类型的动作将时间自动机（TA）转换为有限状态自动机：Set和Exp，它们捕获TA的时间方面。在本文中，我们将SetExp应用于Tiosa而不是TA。当将SetExp应用于Tiosa时，数据及其DG和VA的语义被忽略，也就是说，它们像操作标签一样被处理在使用（解释、处理等）时，应考虑后者由SetExp产生的称为SEiosa的自动机。我们的测试问题将在Sect中解决6使用设置经验在本节中，我们介绍了SEiosa模型，并通过示例说明了SetExp（SetExp的详细描述可以在[18]中找到设A是一个字母表上的Ti osa，SetExp（A）是通过变换得到的SEi osa4.1操作集和失效Set（ci，k）意味着：时钟ci被重置（为0），并且当其值等于k时将到期。更一般地，Set（ci，k1，k2，···，kp）意味着ci被重置，并且当它的值分别等于k1，k2，···，kp时，将多次过期我们不失一般性地假设k1 ;−）图二、 从图1的T1osa A获得的SE 1osa SetExp ㈧。1;x++）（（>;−）;x++）（A. Khoumsi/Electronic Notes in Theoretical Computer Science 130（2005）7989BB4.5塞奥萨省设A=（L，10，H，D，I，T）是一个T i osa，B=SetExp（A）是相应的SE i osa. B 的语法可以由B =（Q，q0，D，I，Λ，λ）定义，其中：Q是状态的有限集合，q0是初始状态，Λ是标记B的转换的有限字母表，λ是转换关系，并且D和I是转换关系。与A的定义相同。B的转换在语法上定义为TR =q;r;µ;DG;VA，其中：q和r是起源和目的地状态;µ是TR的动作;DG和VA是数据保护和变量赋值。DG和VA对于类型1的转换始终为空（参见第4.3和4.4）。Λ是一个字母表，由类型1，2和3的转换标签组成（见第二节）。4.3）。4.6SEIOSA的语义让我们定义一个SEiosaB=（Q，q0，D，I，Λ， λ）的语义初始时，B处于状态q0，H的所有时钟都等于0，变量和常数取值使得I的值为真。转换TR = Σq; r; μ; DG; VAΣ当q为当前状态且DG（如果有）计算为true时启用;否则，TR禁用。从这个状态q开始，只有当TR被启用时，才执行µ（由一个或多个操作组成）;执行µ之后：达到状态r，并应用VA中的赋值（如果有的话）设序列E1，E2，···，∈ Λ表示序列E1E2·· ·，并设从序列E1，E2，···，∈ Λ中去掉其所有内部作用得到让我们通过B接受的序列和迹的集合来定义SEiosaB=（Q，q0，D，I，Λ，λ）的语义：接受（有限或无限）序列λ=E1E2·· ·，对于E1，E2，··· ∈Λ.设n是λ的长度（n可以是无限的），λi=E1E2···Ei是长度为i的λ的前缀，其中0≤i≤n（i是有限的）。λ被B i接受，λ是空序列λ0或：存在一个长度为n的B的跃迁序列Tr1 Tr2···，使得i= 1， 2，···，n：Tri标记为Ei，在执行λi−1之后，Tri被使能。直觉上，λ对应于B的执行。一个迹的可接受性μ：μ被B接受，i μ通过去除B接受的序列的内部动作而获得。直觉，μ对应于对B的执行的观察。我们现在可以引入SEiosa的可观察语言的概念：定义4.3 SE iosaB（OLSEiosa）的可观察语言是B接受的迹的集合。也就是说，OLSEiosa对B的可观察行为进行建模。90A. Khoumsi/Electronic Notes in Theoretical Computer Science 130（2005）79BSetExp（A）一给定一个SEiosaB，可以注意到OLSEiosa隐含地尊重以下条件，称为一致性条件：每个Set（c，k）及其相应的Exp（c，k）分别由时间k分开。我们通过介绍SetExp的一个基本属性来结束本节。令TL=AddTime（L）是通过将时间与每个动作相关联而从语言L获得的定时语言，使得遵守一致性条件。让RmvSetExp（TL）通过移除所有Set和Exp动作（如果有的话）从定时语言TL获得。我们有以下等价定理：定理4.4 RmvSetExp（AddTime（OLSE10sa））= TOLT10sa。直觉上，定理4.4指出，从行为的角度来看，对于没有看到（或忽略）Set和Exp动作的观察者，A和SetExp（A）之间没有区别。从某种意义上说，SetExp（A）除了向A添加一些新的动作（Set和Exp）之外什么也不做，这些动作捕捉A的相关时态方面。正如我们将在下一节中看到的，在我们的测试方法中，这些Set和Exp是由测试系统产生的物理动作5测试架构和一个定理给定相同字母表上的两个Tiosa的Spec和TP，回想一下，目标是合成自动机CTG，从CTG中可以提取并执行测试用例，以确定IUT是否符合Spec中对应于TP的部分。CTG将不会直接在Tiosa的Spec和TP，而是基于从两个Tiosa计算的SEiosa。为了在CTG和IUT之间建立联系，我们使用了我们现在提出的特定测试架构[16]它在Fig.中表示第三章：Clock-Clock接收Set事件并发送Exp操作。(It符合一致性条件）。测试控制器向IUT发送输入，从IUT接收输出，向时钟控制器发送设置动作，并从时钟控制器接收Exp动作。我们定义以下一致性关系confSEiosa，它只是SEiosa的可观察语言的包含：定义5.1设IJ和SJ是同一字母表上的两个SEiosa（IJconfSJ）（OLSEiosaOLSEiosa）.约萨东南IJSJ我们有以下定理，其中SUT（被测系统）由IUT和时钟组成：A. Khoumsi/Electronic Notes in Theoretical Computer Science 130（2005）7991测试-控制器集合（c，k）Exp时钟−输入输出SUTIUT定理5.2设S是输入完备T i osa。如果Test-Controller仅在SetExp（S）接受Set操作时才生成Set操作，则：（IUTconfTiosaS）优惠（假设SUT接受SUT的行为，使得SUT配置SetExp（S））。上述定理意味着我们可以检查我们已经将实时符号系统的测试转换为非实时形式，因此，我们可以（也将）使用并采用符号测试生成（STG）的非实时方法[23]。图三.测试架构此体系结构仅适用于执行内部（即，不可观察的）动作不会重置时钟。事实上，为了生成Set操作，Test-Controller需要观察与时钟重置相关联的每个操作。因此有以下假设：假设5.1执行内部动作的跃迁不会重置时钟。嗨5.1意味着相对于内部动作没有时间限制。6测试生成我们的测试方法结合了[23]和[16]中分别提出的两种互补测试方法，从而扩展了这两种方法。它由图4中概述的四个步骤组成，并在6.1至6.4小节中进行了描述。它的输入是Spec（input- complete，来自引理3.3和Hyp.3.1）和TP（完成，从定义。3.7）。在第一步中，我们计算一个TiosaSpecTP，它接受（所有且仅接受）Spec的定时序列，并指示与位置对应的位置TP的A和R部分。然后，我们在三个步骤（2到4）中合成一个完整的测试图（CTG），从中可以提取一组测试用例并在IUT上执行，以确定是否： SpecTP。的指示A和R用于忽略IUT的每次执行到位置R或从其不能到达位置A。 (See Sects. 3.2和92A. Khoumsi/Electronic Notes in Theoretical Computer Science 130（2005）79SpecTP步骤1步骤2同步SpecTP转换SpecTPSEA步骤3可见行为SpecTPSEA步骤4VIS计算产品SetExp完全测试图CTG3.3更多详情）TP是确定性的和完整的这一事实意味着Spec是输入完整的，而SpecTP是输入完整的。我们的方法的优点是它的简单性，因为实时方面的主要处理集中在步骤2中。步骤1、3和4构成了（非实时）符号测试生成器（STG）的轻微调整[23]。5见图4。 试验方法图5表示在字母表中的Spec和TP ={？φ，？σ，！用于说明试验方法的步骤。Spec的数据为H1={c1}，V1={x}，C1={p}，P1={m}，其中x，p，m为整数.TP数据为H2=V2=C2= N，P2={n}，其中n为整数.x表示任何动作从x到x的最大值，以及？表示任何输入∈什么？φ或？σ）。Spec最初不是输入完整的，我们用虚线箭头表示已添加以使Spec输入完整的部分（参见Hyp. 3.1）。仅由动作标记的转换意味着：它们的（时钟和数据）保护等于常数True，并且它们不重置时钟，也没有变量赋值。这个例子中的TP意味着：我们有兴趣测试Spec的执行，并在第一次出现时终止！不经过位置TL的ρ。这个TP的例子非常简单（没有时间限制），以便阐明不同步骤的操作。即使在一个具体的案例中，TP也应该相对简单，因为它的使用目的是选择规范的一个相对小的部分，以便只集中在规范的某些方面5实际上，STG是一个软件工具。但在这里，STG表示作为工具基础的理论方法。A. Khoumsi/Electronic Notes in Theoretical Computer Science 130（2005）79930σ图五.试验方法举例6.1步骤1：Spec和TP目的是计算等价于Spec的Ti osaSpecTP，使得对应于位置A（分别为R）也被表示为A（分别地，R）。为此，我们需要定义两个Tiosa的同步乘积。设Ai=（Li，li，Hi，Di，Ii，Di，Ti），其中Di=Vi<$Ci <$Pi，i=1，2，是两个Ti。A1和A2的同步产品，写作A 1A 2，受到TA [ 2 ]和IOSTS [ 23 ]的同步产品的启发（但不同）。 A1及A2的定义为满足以下四个条件：(i)1=2。因此，通用字母表将被表示为。这个条件可以很容易地放宽[23]，但为了简单起见，我们将保留它(ii)H1<$H2=H[2]。(iii)（V1<$P1）<$（V2<$P2）=<$，（C1<$P1）<$P2=<$，（C2<$P2）<$P1=<$[23]。(iv)每个动作a∈A在A1和A2中具有相同的签名[23]。假设满足上述四个条件，则A1<$A2由（L，l0，H，D，I，N，T）定义，使得：L=L1×L2，l0=（l1，l2），H=H1<$H2，00D=V <$C <$P，V=V1<$V2，C=（C1<$C2）\V，P=P1<$P2，I=（I1<$I2），而转移的集合T被定义如下：对于每一对跃迁（∑qi;ri;σ;θi;CGi;Zi;DGi;VAi∈ Ti，i= 1， 2：σσ如果θ1和θ2是空元组，则有一个转移σ σ<$（q1;q2）;（r1;r2）;σ;<$;CG1<$CG2;Z1<$Z2;DG1<$DG2;VA1<$VA2<$∈T.σ σ如果θ1和θ2不为空：设DG1，2（分别为1、2）表示表达式-σ σ通过替换DG2（分别 VA2）来自θ2的每个参数L3（m）l0（− ;−）（）下一页− ;x：=mL1（−;{c1}）（− ;L2中文（简体）一（m）L4RTPSpecTL（c1>3;−）（− ; −）一 B94A. Khoumsi/Electronic Notes in Theoretical Computer Science 130（2005）79σSpec由θ1的相应的相同位置参数;则有一个过渡<$（q1;q2）;（r1;r2）;σ;θ1;CG1<$CG2;Z1<$Z2;DG1<$DG1，2;VA1<$σσ σVA1，2∈ T. 这一过程受到了[23]的启发。在步骤1中，我们计算SpecTP=Spec_TP，其位置对应于位置A（分别为R）的TP由A（resp.R）。TP的完整性意味着Spec和SpecTP在观测上是等效（即， TOLTiosa蒂奥萨SpecTP ）.TP和输入的完整性Spec的完整性意味着SpecTP是输入完整的。的影响规范验证TP将在规范中确定分别对应于位置A和R对于图5的Spec和TP，我们获得图6的SpecTP。位置L1和A1是等价的，因为它们可以产生相同的行为。这两个位置之间的区别是，只有A1对应-响应TP的位置A。请注意，根据同步产品的定义，TP的参数n已被删除，取而代之的是Spec的参数m。见图6。 步骤1：从图1的Spec和TP获得的SpecTP。56.2步骤2：将TiosaSpecTP转换为 SEiosa我们通过计算SpecTPSEiosa=SetExp（SpecTP）将问题转化为非实时形式。对于图6的SpecTP，我们获得图7的SpecTPSE10a。集合2.3表示？Set（c1，2，3），Expi表示！Ex p（c1，i）. SpecTP SEiosa的状态 这与位置A（resp .）相关。 R）由A（resp. R），（Expi， n）表示Expi与任意x∈n同时出现，由虚线连接的节点表示相同的状态6.图7的状态A1等同于状态S1，区别在于S1不对应于TP的位置A。6 为了清楚起见，重复了这些内容。一(m)(− ; −)（）下一页（−;{ c1}）（− ;−）− ;x：=mA（− ;{c1}）（− ;一（m）（c1>3;−）（− ; −）（c1>3;−）（− ;−）一R A忽略部分=TOLA. Khoumsi/Electronic Notes in Theoretical Computer Science 130（2005）7995在图7和随后的图中，如果DG在转换中评估为真，VA为空，则（DG;VA）不表示。见图7。 步骤2：SpecTPSEiosa 从图6的SpecTP获得6.3步骤3：提取SpecTPSEiosa我们构建了SpecTP SE iosa的可见行为 分三个子步骤：子步骤3a：通过投影到可识别的字母表中来消除内部动作。为此，我们可以采用[23]中提出的方法结果表示为Vis（SpecTPSE10sa）。自适应包括一个预先步骤，其中简单地擦除类型3的转换中的内部动作。在此之后，我们可以使用[23]的程序，因为剩余内部动作在它们的转换中是“单独的”。（回想一下，我们只考虑内部动作不重置时钟的情况子步骤3b：通过使用[23]中提出的启发式来确定Vis（SpecTPSE10sa）结果表示为Det（Vis（SpecTPSE10sa））。子步骤3c：注意，Det（Vis（SpecTPSE10sa））的每个状态对应于SpecTPSE10sa的一个或多个状态。共和国R和A国Det（Vis（SpecTPSE10sa））选择如下：• 我们将对应于SpecTPSE10a的至少一个状态R的每个状态称为R。直观地说，我们忽略了每个可以对应于序列的执行不需要测试。• 我们可以将A称为与SpecTPSE10a的无状态R和至少一个状态A相对应的每个状态。 直观地说，我们接受每一个执行，其中：1)不能对应于一个序列不被测试，和2）可以corre-spond到一个序列被测试。另一种方式，似乎更现实，R实验实验2R实验实验3R？*？*？*实验3实验2实验3（m）（−;x：=m）S实验3实验3A 1.....1电子邮件*实验2？*（m）？*？*？*？*RRRExp2实验经验值R实验ExpRR实验Exp323R布;x++）（拉瓜>拉瓜布>96A. Khoumsi/Electronic Notes in Theoretical Computer Science 130（2005）79VISVISVISVISVISVISVISVISVIS在每个状态中调用A，该状态仅对应于SpecTPSE10a的状态A。实际上，只有当我们确信它对应于一个要测试的序列时，我们才接受一个执行结果表示为SpecTPSE10sa。对于SpecTPSEiosa 在图7中，我们获得SpecTPSE10a， 图8 .第八条。见图8。步骤3：从图1的SpecTPSE10sa获得的SpecTP SE 10sa。76.4步骤4：计算完整测试图（CTG）回想一下，SE10a的跃迁被标记为形式（E）或以下四种形式之一：（σ），（σ，S），（E，σ），（E，σ，S），以及（DG;VA）。假设与[10，16，23]类比我们构造一个完全测试图（CTG）如下：• 设