SPHIN：基于SPIN的可重构混合系统模型检测器

理论计算机科学电子笔记145（2006）167-183www.elsevier.com/locate/entcsSPHIN：一个基于SPIN的Hosung Song1威斯康星大学绿湾分校信息与计算科学系美国威斯康星州格林湾Kevin J.威廉·C. 第3回合密歇根大学电气工程与计算机科学系美国密歇根州安娜堡摘要我们提出了SPHIN，一个可重构混合系统的模型检测器的基础上的模型检测器SPIN。我们观察到，物理（模拟）移动性可以以与通过通道名称传递在π演算中建模逻辑（离散）移动性相同的方式建模。我们选择SPIN是因为它支持通道名传递，并且可以对重构进行建模。 我们扩展了PROMELA的语法和基于预期语义的验证算法。 我们通过建模和验证可重构混合系统来展示该工具的 功 能 。保留字：形式化方法，模型检验，SPIN，混合系统，移动性。1介绍可重构混合系统是数字和模拟组件的集合，其中数字组件嵌入模拟组件并与之1电子邮件：hosungs@umich.edu。部分由密歇根大学EECS系CSE分部的HMHP资助。2电子邮件：kjc@umich.edu3 电子邮件地址：rounds@mac.com1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.10.011168H. Song等人/理论计算机科学电子笔记145（2006）167组件及其配置可以通过组件的物理或逻辑移动性来改变。无人驾驶飞行器[5]、解锁代理[18]和机器人自动化装配工厂系统[12]是安全关键型可重构混合系统的示例。它们的模拟动态由具有离散控制模式的数字程序控制，并且它们的形式根据它们的物理位置而改变对它们来说，保持安全关键特性（如避免碰撞）非常重要SPHIN为这种可重构的混合系统提供了一个正式的验证框架它基于模型检查器SPIN [11]。SPIN已经支持动态进程创建，通过局部变量隐藏信息，以及通过允许消息传递中的通道名称来建模移动性4的能力，这是用于移动性建模的π演算[14SPHIN可以通过允许模拟变量的声明模拟这些声明可以与动态过程创建相结合，以便模拟组件也可以在本地和动态地实例化以这种方式定义的模拟组件也可以通过将模拟名称作为消息传递来在过程之间交换。通过这种方式，SPHIN可以对模拟元件的移动性以及基于π演算的分立元件的传统移动性进行模拟状态和时间序列由凸多面体和相关操作表示PPL（Parma Polyhedra Library）[4]就是用于这个目的。安全性验证的可达性分析算法和活性验证的LTL模型检验算法都根据新引入的模拟元件进行了扩展SPHIN的可用性证明了一些案例研究，包括经典的混合动力系统的例子和可重构的混合动力系统的例子。据我们所知，这是SPIN的第一个混合扩展 （ 在 密 集 时 域 SPHIN 可 通 过 访 问 www.example.com 获 得http://sphin.webhop.net/。1.1相关工作我们最初的动机是Klavins和Koditschek他们的建模形式是对Petri网的混合扩展，主要用于无死锁的有限验证和从产品装配图自动合成这些要素我们希望为可重构混合系统建立一个更通用的建模和验证框架我们的出发点是π演算，因为它被证明是简单的（只需添加最少的新算子）和足够的（能够表达所有的迁移率4我们可以互换使用机动性和可重构性。H. Song等人/理论计算机科学电子笔记145（2006）167169方面）用于移动系统。由此我们发展了φ-演算[15]，这是基于环境和环境作用概念的π-演算的混合扩展这些构成了SPHIN的语法扩展和语义的基础对于验证部分，我们专注于模型检查方法，因为在模拟动力学存在的情况下，互模拟已经非常难以显示在[17]中，我们观察到SPIN可能是模型检查某些π演算过程的合适基础。SPHIN是从这个实验中得到的φ演算的自然有许多混合动力系统验证工具，如HyTech [10]，CHARON [2]和d/dt[8]。它们适用于没有可重构性的混合系统SPIN在RT-SPIN [19]中被扩展到（密集）实时系统，在[6]中被扩展到离散时间混合系统2PROMELA-Hybrid：SPHIN建模语言PROMELA-Hybrid 是 SPHIN 模 型 检 查 器 的 输 入 语 言 。 它 扩 展 了PROMELA，输入语言的模型检查器SPIN，与一些原语描述混合动力过程与模拟动态。有关PROMELA的详细信息，请参阅[11]。2.1语法在这一小节中，给出了PROMELA- Hybrid中混合扩展的完整语法.基本上，语法扩展是基于以下两个原则定义的。• 每个PROMELA语句都是PROMELA-Hybrid语句。这是自然的，因为混合系统的集合包含离散系统的集合• 每 一 个 PROMELA 语 句 都 可 以 用 模 拟 分 量 进 行 扩 展 ， 这 样 得 到 的PROMELA-Hybrid语句就可以在φ演算中表达一个有效的混合动作：受保护的模拟条件可以触发模拟变量的重置动态。在这方面，PROMELA-Hybrid中的语句要么是PROMELA语句，要么是混合语句，混合语句是PROMELA语句后跟类似子句。在巴科斯范式中，顶层语法规则如图1所示。混合语句总是包含一个when子句，用于检查模拟变量的条件，以及一个reset子句，用于重置模拟变量的动态when子句由关键字when和list引导的条件被括在大括号中。重置子句由关键字reset和reset列表被括在花括号中。此外，应该有一个用于声明模拟变量的构造一170H. Song等人/理论计算机科学电子笔记145（2006）167语句：：= promela语句|hybridstatementhybridstatement：：= promela statement when子句reset子句when子句：：=when{cond list}reset子句：：=reset{reset list}vardcl：：= promela var dcl |analog vardcl analog var dcl：：=模拟复位图1.一、PROMELA-Hybrid的顶级语法（图。23显示后续级别的语法condlist：：=/* empty-null list */|cond list non nullcond list non null：：= cond |cond list非null，condcond：：=varrefininterval重置列表：：=/* 空-空列表 */|重置列表非空重置列表非空：：=重置|重置列表非空，重置reset：：=varref={interval，interval，interval}图二. PROMELA-Hybrid的中级文法变量声明var dcl是PROMELA中已经定义的变量声明，或者是一个新的模拟变量声明analog var dcl，它由关键字analog后跟reset组成。重置将在图2中与cond及其列表形式一起简短地条件列表是由逗号分隔的零个或多个条件组成的列表。类似地，重置列表是由逗号分隔的零个或多个重置的列表一个条件是varref引用的变量的值是否属于给定的区间。重置尝试重置变量的三个组成部分，也称为varref：当前值，变量的导数值和变量的不变条件。这就是为什么重置是一个变量赋值，后面跟着三个用花括号括起来这些都对应于φ-演算中的混合动作的语法。间隔可以是开放的或封闭的（在任一端）。开边界由括号表示，闭边界由括号表示。实际的边界值可以省略，表示在相应的一侧没有边界。边界可以是PROMELA表达式（仅涉及整数常数和离散变量）或仅涉及模拟变量的线性表达式。为了完全支持有理系数，对于仅具有整数系数的整个线性表达式，可以存在整数分母因此，lin expr现在要么是基本项（只是模拟变量varref或其常数倍数或整数常数），要么是加法H. Song等人/理论计算机科学电子笔记145（2006）167171interval：：=/* 空interval */|l paren bound，bound rparen l paren：：=（|的rparen：：=）|]的一种bind：：=/* 空绑定 */|普罗梅拉快车|直线快递| int const / int const line expr：：=term|term + linexpr|term − lin expr|term − lin exprterm：：= int const |varref |− varref |int const变量ref图三. PROMELA-Hybrid的底层文法或者减去一项和更小的线性表达式。这样，任何有理系数的线性表达式都可以用一个简单的文法有效地表示出来例2.1[PROMELA-Hybrid语句]下面的模拟变量声明模拟x = {[0，1），[1/3，1/2]，（，-2]};模拟y ={[-1，1]，[1-x，1-x]，[0，）};定义两个模拟变量x和y（有时写为x（t）和y（t）来表示它们的时间依赖性），在每个变量的实例化时，它们的初始值x（t0）和y（t0）给出为：0 ≤x（t0）<1，−1≤y（t0）≤1。更改x参 数 和 变 量 参 数的特性已得到验证1/3≤xs t e c （t）≤1/2，ystec（t）=1−x。它们也有不变量：任何可能的转换都必须满足的变量条件他们是x（t）≤ − 2，y（t）≥0。以下PROMELA-Hybrid语句ch！msg when {xin（，0]， yin [x-1，5）}[1，2]}};是一个消息传递语句ch！msg仅在when子句中给出的模拟条件为true时可执行，并伴有reset子句指定的模拟复位操作。下一节将详细说明这一声明的含义。Q172H. Song等人/理论计算机科学电子笔记145（2006）167从语法上讲，可以将线性表达式放置到三个区间中的任何边界值。然而，为了在当前基于凸多面体的实现中得到有意义的结果，在Cowow条件下，只能给出边界的常数。2.2语义PROMELA-Hybrid的形式语义在[16]中基于[19]和[11]中给出的符号给出由于篇幅所限，本文仅给出简单的例子。总之，PROMELA-混合模型的状态是模拟估值和离散部分的集合，还具有关于模拟如何随时间演变的信息。由于新引入的模拟器件，有两种可能一种是重置模拟变量的动态，同时执行相关的SPIN操作。另一种方法是让时间按照模拟动态变化，而不执行任何SPIN操作。例2.2[PROMELA-Hybrid中的离散动作转换]考虑下面的PROMELA-Hybrid语句ch？msg when {x in[，3]， y in（0，）}重置{ x = {，[-1，-1]，}，y = {[0，1]，（，4]};根据以下评价Xx = 1，y = 2用下面的雷诺方程xstec=2，y stec= 1在以下不变条件下x≤ 3，y≥ 0。当x≤3y> 0在模拟变量的当前估值下为真时，when 由于x和y的当前赋值满足谓词，因此仅当消息接收语句ch？msg已启用。假设在缓冲器中有一个用于信道ch的消息。则整个混合语句被启用，因此它的执行也会随之离散部分的执行（ch？msg）将由于消息传递而导致变量msg中的新内容。模拟部分的执行将导致以下估值。x = 1，y∈ [0，1].H. Song等人/理论计算机科学电子笔记145（2006）167173这里，y可以是[0，1]中的任何值，因为y的值被指定为重置为区间[0，1]中的值。 x的值不会改变，因为 在x对应的reset子句中没有值重置部分。将计算公式改为：xstec = −1，y stec = 1。在此，y的降序方程不改变，因为在y的对应重置子句中不存在降序重置部分。最后，不变条件将改为：x≤ 3，y≤ 4。例2.3[时间流转换]考虑以下混合状态qH模拟变量x和y。（q，{x=1，y=2}，{xstec=1，ystec=2}，{x≥0，y≤7}）。在2秒之后，混合状态可以进行到以下混合状态的时间转换（q，{x=3，y=6}，{xstec=1，ystec=2}，{x≥0，y≤7}）。这种转变是可能的，因为最终值与具有指定初始值的微分方程的解相匹配，并且所有中间轨迹点都满足不变条件。然而，qH不能进行持续时间为3秒的湍流转变，因为在2.5秒之后，y将大于7，并且这不满足不变条件。在这里，我们可以看到不变条件主要是为了阻止时间的无限流动3验证算法与PROMELA验证一样，PROMELA-Hybrid验证任务显式搜索状态空间。然而，如前一节所述，PROMELA混合模型的状态可以具有实值模拟变量的假设实数集是稠密的，并且有无限多的实数不能以有限的方式表示，很明显，PROMELA-Hybrid模型的状态的直接枚举不是进行状态空间搜索的合适方法。一个新的方法来处理这个问题最初是由Bertur在[1]中提出的。整个n维向量空间被划分为有限个区域，每个区域代表一组状态，可能是174H. Song等人/理论计算机科学电子笔记145（2006）167y y y4 4 43 3 32 2 21 1 101 2 3 4 5X012345X012345X(a) 初始区域(b) 应用时间流转换(c) 应用不变条件见图4。 用多面体表示模拟量赋值的区域在许多的。一个区域中的状态应该是时间抽象的双相似的，因为当抽象出后续转换中的实际时间信息时，它们的未来行为应该是双相似的该想法以类似的方式推广到混合动力系统[ 3 ]，并在混合动力系统的我们在PROMELA-Hybrid中采用了类似的方法本节详细介绍了这些方法。3.1模拟态的多面体表示和时间流跃迁3.1.1初始状态和时间流转换注意到模拟变量的每个初始条件都以区间（开或闭，有界或无界）的形式给出，很容易看出PROMELA-Hybrid模型中模拟变量的所有初始值的集合在n维向量空间中形成多面体。例如，考虑如下定义的2个模拟变量x和y模拟x = {[1，3]，[1，2]，[，4]};模拟y ={[1，2]，[1，2]，[，（10-x）/2]};定义中的初始条件为1≤x≤ 3和1≤y≤2，很明显，条件可以用多面体表示在二维空间中，如图4（a）所示。初始条件中的界不仅可以是常数，还可以是关于模拟变量的任意有理系数的线性线性表达式仍然会导致向量空间中的多面体。当时间流条件区间中的边界都是常数时，可以通过考虑从初始状态区域点开始的所有时间流跃迁来扩展初始状态区域。这是通过将射线附加到初始多面体的每个角点来完成的。在这里，射线被定义为模拟变量的增长率之比。在该示例中，最大比率是2/1 = 2，并且最小比率是1/2 = 0。5.将此射线添加到每个点并取最外边界，将生成区域多面体，如y=（10-x）/2X=4H. Song等人/理论计算机科学电子笔记145（2006）167175y=3x=2y y y4 4 43 3 32 2 21 1 101 2 3 4 5X(a) 初始多面体y4012345X(b) 当条件适用时y4012345X(c) 应用值重置3 32 21 101 2 3 4 5X(d) 时间流转换012345X(e) 应用不变条件图五、处理混合动作的多面体操作步骤图4（b）。这个多面体包含了从初始区域多面体中的任何一个点开始，通过采取任意时间长度的时间流转换可到达的所有点这只能在以下情况下进行：当连续流条件区间中的边界为常数时。由于不变量条件，并非上述扩展区域中的所有点都是可能的在上面的例子中，x必须是x≤4，y必须是y≤（10−x）/2。这些形式仍然其他多面体，并需要与前一个多面体重叠，导致最终显示在图4（c）中。通过这种方式，可以以有限的方式表示相同离散状态分量下所有模拟变量的所有赋值这个想法起源于Halbwachs，他在20世纪70年代后期使用线性关系对程序进行抽象后来在20世纪90年代，他将这一思想应用于混合系统分析，如[9]。它也被Zhair，Henzinger和Ho采用[3]。3.1.2混合行动假设在图4（c）所示的模拟变量的可能估值下启用以下混合动作a = 1，当{ xin [2，]， yin [3，]}重置{ y= { [y-2，y-2]，[1，1]，[，3]}};混合作用的when条件在二维空间中形成另一个多面体。因此，在二次多面体中的赋值使when条件成为可能。只有在第一个多面体中的估值将经历y ′ = y-2X=4y=3176H. Song等人/理论计算机科学电子笔记145（2006）167在reset子句中指定的reset操作。reset子句声明y这在二维空间中很容易被看作是幅值为2的负y在更一般的设置中，由于可能的重置如上所示，我们必须为要重置的变量添加新的维度（例如上面的表达式yJ=y− 2中的yJ），通过将新多面体投影到其他维度来删除旧变量（y），然后将新变量（yJ）映射到旧变量（y）。在此之后，新的多面体将在新的时间流条件(here，ystec = 1，其最初为1≤y stec≤ 2）。然后，最后更新的不变量（这里，y≤3，最初是y≤（10−x）/2）被应用于形成所有可能估值的最终多面体图5显示了这些步骤参与任何混合行动PROMELA-Hybrid的任何一个过渡序列都可以表示为一个离散状态序列，并伴随着应用上述运算得到的多面体。3.2达性分析可达性分析主要用于安全验证。安全属性的验证确定不安全状态是否可达。可达性分析是通过系统地搜索整个状态空间来完成的。由于内存空间的限制，深度优先搜索优于广度优先搜索。随着搜索的继续，它存储以前访问过的状态。如果新访问的状态在先前访问的状态集中，则不再采用该分支，并且搜索移动到另一个分支或回溯到其前任。因此，在可达性分析中，比较两个状态是否相同是非常必要的在PROMELA和SPIN中，状态信息中只存在离散分量，因此状态比较可以归结为正确排列的状态向量的逐位比较。在PROMELA-Hybrid和SPHIN中，状态信息中不仅有离散的分量，而且模拟量的赋值也聚成一个多面体。在搜索PROMELA-Hybrid模型的混合状态空间时，很可能存在两个具有相同离散分量但不同多面体的状态例如，假设（st，P1）被访问，然后过了一段时间，（st，P2）被访问。这里，st是离散状态分量，并且P1和P2是离散状态分量。P2是模拟多面体.如果P2/P1，那么算法不能回溯，因为离散部分ST先前被访问过。搜索只能在访问（st，P3）时回溯，其中P3<$P1<$P2.在这里，我们看到了存储凸多面体的并集的必要性，这些多面体不必是凸的，作为访问区域。PPL库以清晰的方式支持这些联合操作和数据结构。此外，我们可以选择仅将这些并集的近似值 SPHIN目前H. Song等人/理论计算机科学电子笔记145（2006）167177支持用于此目的的凸包近似所有这些修改都包含在DFS可达性算法中，如第页的图8.2所示170 [11]。最后，我们陈述了上述可达性分析的正确性通过正确性，我们的意思是，如果使用多面体表示的深度优先搜索的可见区域与目标区域具有非空交集，则实际上存在从初始状态开始到目标区域中的状态的定时跟踪定理3.1（可达性分析的正确性）设PRO-MELA-Hybrid模型M以（d1，A1）作为其可能的初始状态的区域（di是离散状态，Ai是离散状态di处模拟变量的所有可能赋值的凸多面体），以（dt，At）作为目标区域。如果SPHIN中的深度优先搜索算法报告了与（dt，At）的非空交集，则存在从初始状态M到（dt，At）中的状态的定时迹。我的律师。该过程是构造时间执行transc（d， a）→δ1（d，AJ）→1 1 11δ2（d，a） （d，aJ）→. →（dδn，a）（d，aJ）（与d=d，δ∈R+，a和2 2→22n n→nnn t i iaJ是模拟估值，设为一个SPHIN输出（反例），I nple）序列（d1，A1），.，（dn，An）（Ai是凸多面体，由下式计算根据转换的定义语义的DFS算法）。这个构造可以通过对n的归纳来完成。由于篇幅限制，我们省略了完整的证明细节，可以在[16]中找到Q3.3LTL模型检验更复杂的性质，如活性，可以通过对更复杂的LTL公式进行模型检查来验证。例如，通常的安全性要求由简单的LTL公式Qp表示（其中p是针对当前时间实例的安全性），而对于请求之后的实际确认的典型活性要求LTL公式Q（p→Qq）（p表示请求，q表示确认）。像往常一样，要求的LTL公式φ首先被否定，然后被转化为一个等价的Bu？hi自动机A<$φ，它精确地接收满足被否定的LTL公式<$φ的输入序列。然后将模型自动机AM和否定的需求自动机A<$φ组合，得到AM，<$φ，检查它以查看在包含一个接受状态，并且可以从初始状态到达。 众所周知，否定的要求LTL公式<$φ是可满足的，当且仅当这样一个循环存在于具有约束的布希自动机AM，<$φ[11，第7章]。 换句话说，M |= φ当且仅当AM，<$φ包含可达接受圈。178H. Song等人/理论计算机科学电子笔记145（2006）167为了将这一思想应用于SPHIN中的混合系统，我们要求LTL公式中的原子命题仅由离散状态分量组成这是必需的，因为周期检测仅对状态的离散分量起作用。SPIN中用于LTL模型检验的嵌套深度优先搜索算法[11，第7章]也进行了修改，以适应新引入的模拟区域。访问状态空间中的每个个体状态用多面体的并集来扩充，并且种子状态也用多面体区域来扩充最后的加法是检查种子状态是否再次被重新访问。它应该伴随着检查种子区域多面体和当前区域多面体的相交是否不为空。下面的定理说明了算法的正确性。定理3.2（LTL模型检验算法的正确性）如果修改后的嵌套DFS算法发现了一个循环并返回它，那么存在一个被底层混合体Buüchiau toma ton接受的PROMELA-Hybrid模型的时间迹。证据 因篇幅限制而省略。 详情见[16]。Q4案例研究在本节中，我们将介绍三个使用模型检查器SPHIN进行验证的案例研究3机器人铲斗旅是需要可重构性的另外两个是标准的混合系统示例，不需要可重构性，并且已经使用其他现有工具进行了建模和验证PROMELA-混合源代码 和 本 节 所 述 示 例 的 验 证 结 果 均 在 SPHIN 分 布 中 提 供 ， 网 址 为http://sphin.webhop.net/。4.1列车闸机控制器铁路交叉口的模型是混合系统验证研究的经典玩具示例。在模型中有三个组件-列车、门和门控制器。变量x代表火车的距离从大门。虚线变量xtec表示x的一阶导数，相对于时间t，也就是火车的速度。最初，列车距离门2000米，并以40至50m/s的当列车通过1000米点时，它会向控制器发送一个应用程序它也可以将速度范围改变到30和50 m/s之间列车通过闸机，距离闸机100米后，发出出站信号H. Song等人/理论计算机科学电子笔记145（2006）167179向控制器通知其退出。为了重复上述过程，列车还将其距离重置为2000米，其速度重置为40至50米/秒，其方向接近列车。变量g表示门相对于地平线的度数初步全面开放（g= 90）和不移动（gstec = 0）。如果门接收到一个较低的信号，它会以-9度/秒的速度降低杆，直到它与地平线平行。如果闸门收到上升信号，它将以9度/秒的速度提升杆直到它垂直于地平线。最后，控制器接收来自列车的信号（应用程序或出口），并向闸门发出信号（升高或降低）。为了对与控制器和门相关联的延迟进行建模，控制器在从接收到app（相应地退出）信号的时间起经过预定义延迟之后发出升高（相应地降低）信号对于系统的精确混合自动机模型，读者可以参考[16]或[10]的原始模型。该系统最重要的安全要求是，每当列车在一定距离内时，闸门应关闭。也就是说，如果预定义的距离被称为D，那么不应该发生x是小于或等于D，同时g大于0。因此，问题是检查对于任何离散控制位置l，不安全区域（l，x≤Dg>0）是否可达。需求可以编码为监视器自动机中的assert（）语句主动程序型监视器{assert（false）when { xin（，D]，gin（0，）}reset{}}由于monitor进程中的assert（）语句的参数为false，并增加了关于模拟变量的when条件，因此当when条件变为true时，将引发assertSPHIN分布中的验证结果表明，如果D是350. 但是，它们也表明，如果D大于350.导致这种违规的执行跟踪也由SPHIN验证器生成。4.2费希尔另一个经典的混合系统的例子是费舍尔[13]中给出的原始协议是基于所有进程中的时钟以相同速率前进的在[3]中，作者通过允许不同和漂移的时钟速率将该协议扩展到混合系统每个进程Pi（i= 1， 2）执行以下算法。180H. Song等人/理论计算机科学电子笔记145（2006）167机器人带零件2r在出来0123工作空间见图6。 3-机器人铲斗组重复重复等待k =0k：=i延迟b直到k =i{临界截面}k：=0永远存在一个共享的离散变量k，当且仅当k=i时，过程Pi可以进入临界区。每个进程都有一个本地时钟，可能有不同的和漂移的时钟速率。该协议假设对共享变量的写访问（即，对于赋值k：=i）的延迟高达一个时间单位此外，该协议还要求在分配后再延迟b个时间单位。SPHIN分布包含两种情况的SPHIN代码i）当a= 2且b= 3时，ii）当a= 5且b= 6时。时钟频率相同：[0。8，1]对于P1，和[1，1. 1]为P2。这里的验证任务是检查安全（互斥）要求。safety属性在单独的monitor进程中表示，如果两个进程都处于其临界区，则会引发断言。验证结果表明，a= 2和b= 3时满足安全要求，而a= 5和b= 6时不满足安全4.33-机器人铲斗组这个例子是我们在第1节中提到的最初动机。图6示出了该示例的图示。有三个机器人排成一排。第一个机器人从零件送料器中取出一个零件，将其转发给第二个机器人。然后第二个机器人对第三个机器人做同样的事情。最后，第三个机器人将零件放入输出箱。 在[12]中，Klavins和Koditschek在他们的TPN（Threaded Petri Nets）形式主义中使用具有完全非线性模拟动力学的域和目标区域的概念来在SPHIN模型中，每个机器人为了模拟重复的H. Song等人/理论计算机科学电子笔记145（2006）167181在零件传送过程中，零件送料器和输出仓的作用通过一个过程结合起来，输出仓的输出零件被送回零件送料器。SPHIN分布包含了这种建模旅系统的活性验证结果。建立最终和无限零件转移的两个LTL公式，求反，然后检查求反后的需求公式是否存在令人满意的轨迹验证是成功的，证明旅系统满足活性要求。到目前为止，每一次处决都是在短时间内完成的。5结论在本文中，我们提出了SPHIN，可重构混合系统的模型检测器语法和语义扩展是精心完成的，以实现模拟组件（全局或局部）和一般移动性的建模能力。对验证算法进行了修改，以用凸多面体来表示模拟状态和时间流，从而适应这些扩展我们提出了一些案例研究来证明SPHIN的可用性，包括经典的混合系统示例和3机器人铲斗旅的可重构混合系统示例 SPHIN可在www.example.com上获得http://sphin.webhop.net/。在SPHIN中有很多东西需要改进第一，更有效的整数可达性分析应采用合理的近似表示在文献[16]中，提出了一种用欧拉方法数值分析常微分方程（ODE）动力学的近似方法该近似严重受限于基于GMP5（Gnu Multiple Precision arithmetic library）的当前实现这给出了精确的验证结果，但在许多情况下，由于任意精度和近似值导致计算困难，结果不可用，而没有任意精度表面，如安全验证。其次，建模语言中的物理域概念是非常可取的，因为大多数重构都是基于局部物理邻域中的代理进行的我们认为将Ambient演算[7]中的管理域概念引入φ演算和PROMELA-Hybrid是一个很好的最后，SPHIN还可以添加许多方便的功能，例如使用带有定时信息的生成反例的引导仿真5 http://www.swox.com/gmp/182H. Song等人/理论计算机科学电子笔记145（2006）167模拟状态可视化仿真，以及对SPHIN的GUI支持（类似于xspin）。确认我 们要 感谢 匿 名评 论 者的 全面 和 有益 的 意见 。我 们 还要 感 谢GerardHolzmann博士提供的模型检查器SPIN，使源代码可用，并在回答我们的问题时提供支持。引用[1] 巴尔河，C. Courcoubetis和D. L. Dill，Model Checking in Dense Real-Time，Information andComputation104（1993），pp. 2-34[2] 巴尔河，R.格罗苏岛Hur，V. Kumar和我。Lee，CHARON中混合系统的模块化规范，在：HSCC，2000年，pp. 6比19[3] 巴尔河，T. A. Henzinger和P. -H. 何，嵌入式系统的自动符号验证，IEEE软件工程学报22（1996），pp.181-201.[4] 巴尼亚拉河P. M. Hill和E. Za Zahanella，“Thehttp://www.cs.unipr.it/ppl/Documentation/ppl-user-0.6.1-print.pdf,2004年[5] Bayraktar，S.，G. E. Fainekos和G. J. Pappas，固定翼无人机，第43届IEEE决策与控制会议论文集，2004年。[6] Bosnacki，D.，Toward modeling of hybrid systems in PROMELA and SPIN，1998，pp. 75-96，also available as：H. Bowman，G. J-P Katoen，D. Latella和M. Massink[7] 卡尔代利湖和A. D. Gordon，Mobile ambients，in：Foundations of Software Science andComputation Structures：First International Conference，FOSSACS[8] 天啊T 论文，INPG，Verimag（2000年）。[9] Halbwachs，N.，Y.-- E. Proy和P. Raymond，通过凸近似验证线性混合系统，国际静态分析研讨会，SAS[10] Henzinger，T.一、P. - H. Ho和H.Wong-Toi，HyTech：混合系统的模型检查器，在：第九届计算机辅助验证国际会议（CAV460-463[11] Holzmann，G. J.，“The SPIN Model Checker,” Pearson Education,[12] Klavins，E.和D. E.陈文辉，机器人系统的动态行为分析，国立成功大学机械工程研究所硕士论文（1999）。[13] 兰波特湖，一种快速互斥算法。，ACM Trans.Comput. 系统5（1987），pp.1比11[14] 米尔纳河，《通信与移动系统：π-演算》，剑桥大学出版社，1999年。H. Song等人/理论计算机科学电子笔记145（2006）167183[15] 圆形，W。C. 和H.宋，φ-演算：一种用于可重构嵌入式系统的分布式控制语言，在：O。Maler和A. Pnueli ， editors ， Hybrid Systems ： Computation and Control ， 6th InternationalWorkshop，HSCC 2003，Lecture Notes in Computer Science2623（2003）. 435-449[16] 宋，H.，“可重构混合系统的形式规范和验证”，博士。Thesis，The University of Michigan（2005）.[17] 宋，H.和K. J. Compton，PROMELA翻译的π-演算过程，技术报告CSE-TR-472-03，密歇根大学，Ann Arbor，Michigan（2003）。[18] Tanner，H.G.，A. Jadbabaie和G.J. Pappas，移动代理的稳定锁存第二部分：动态拓扑，2，2003，pp.2016-2021年。[19] Tripakis，S.和C. Courcoubetis，Extending PROMELA and SPIN for real time，in：ToolsandAlgorithms for Construction and Analysis of Systems ， Proceedings of the SecondInternational Workshop（TACAS329-348