利用自动机理论模型检验算法,检验车站联锁逻辑的有色Petri网模型是否满足预期的性能.通过采用带标签的广义Büchi自动机(LGBA)构建线性时态逻辑,有效地解决了模型检验中的状态空间爆炸问题.该方法的研究增强了有色Petri网的分析和验证能力,利用该方法对车站联锁逻辑的实际问题进行了性能验证.

维普资讯

5第 3卷第 1期 3V1 3 o. 3

计

算

机

工

程

20 0 7年 8月Aug t20 7 us 0

No. 5 1

Co p t rEn i e rn m u e gn e i g

博士论文

文章号 1 o 3 8 o )— 3_ 3缡： o _ 4 ( o 1 03 0 o - 22 75 _ _

文标码： 献识 A

中分类 T 3 圈号： P1 1

联锁逻辑形式化模型检验的研究杜军威，徐中伟宋，波(.同济大学电子与信息工程学院，上海 203;2青岛科技大学信息科学技术学院，青岛 2 66; 1 03 1 . 60 13上海大学计算机学院，上海 2 0 7 ) . 002

摘

要：利用自动机理论模型检验算法，检验车站联锁逻辑的有色 Pt网模型是否满足预期的性能。 ei r通过采用带标签的广义 Bi i ih自动机 c性时态逻辑，有效地解决了模型检验中的状态空间爆炸问题。该方法的研究增强了有色 P t网的分析和验证能力，利用该 ei r

(G A￣ L B )

方法对车站联锁逻辑的实际问题进行了性能验证。

关健词：有色 Pt网；线性时态逻辑；带标签的广义 Bi i ei r th自动机；联锁逻辑 c

Re e r h 0 r a o e e k n f nt r o k n g c. s a c n Fo m l M dl Ch c i g 0 e l c i g Lo i IDU u . i, J n we XU o g we S Zh n . i, ONG Bo f. c o l f l t nc& Ifr t nE gn eig T n jUnv ri, h n h i 0 3 l 2 S h o Ifr t nS i c n eh oo y, 1 S h o Ee r is nomai n ier, o gi iest S ag a 0 3; . c o l nomai ce eadT c n lg o co o n y 2 f o o nQig a nvri cec n eh oo y Qig a 6 0 13 Sh o f mp tr ce c, h n h i iesy S a g a 20 7 ) n d oU ies yo S i eadT cn lg, n d o2 6 6; . c o l Co ue ine S ag a v ri, hn hi 0 0 2 tf n o S Un t

[ b ta t A src]A to b u uo t— ert d l h cigi pee td T i me o s ei epo et

oo ern t C N) me da o t tma t oei moe ekn rsne . hs t diu e t vr yt rp r o c lr t es P h a ah c c s h s dO fh yf P i (mo e o nel c n o i.S a p c x o i o a e s le fii t y c n t cig l e r i e o a lgc L L d l f itr k g lgc tt s a e e p s i n c n b ov d ef e l b o s u t i a— me tmp rl o i( T )wi a e d oi e t cny r n n t h t lb l e g n rl e i h a tma n L A) n mo e h c n . hsme o r v stea a s d c e kn N. p a t a c s er l a e eai d B i i uo t ( GB i d l e k g T i z c o c i t di o e n l i a h c go CP A rci l aeo t a w y h mp h y sn i f c f h ii tro k n o i sc e ke y t i t o n e l c g l g ci h c d b sme d. i h h

[ ywo d]c lrdPt e;ie—mee oa gclb ldgn rl e f h uo tn itr c n gc Ke r s ooe ernt l a t mp rlo i;aee eeai dB c i tma;nel k gl i i s nr i t l z i a o oi o

计算机联锁系统是一种典型的安全苛求系统 (aey sft— ciclss m) r i y t。这类系统根本特征是将安全性视为第 1特 ta e

计算、系统的可靠性和安全性分析等诸多领域。为了使用 L L T对 C N模型进行验证分析，需要将 C N构建的模型转化为 P P

性，使用形式化方法开发和测试联锁系统被证明是提高系统的可靠性和安全性的一种有效手段。有色 P t er i网 (ooe clrd

描述变迁的 K ik r e形式。下面给出 C N的 K ik p P r e结构的形 p式描述：

P t e, P er ntC N)是非常有效的形式化建模工具，它可对复杂 i

定义 1 P N的 K ik C r e结构 p三元组^<, S>义为有色 P t, R,定 _ 0 er i网{ P AⅣCⅡ,,,’,

系统的模型进行有效的化筒，从而降低

了系统的复杂性。文献【】 1讨论了如何利用 C N对联锁逻辑进行建模，但对联锁 P系统形式化模型的性能分析与验证的文献较少。通常对 C N模型的分析验证方法分有两类 J P:可达集分

E GM0 ( P的具体定义见文献【】 K ik结构，中，,,}C N 2) r e的 p其 S和 R的含义归纳如下： o() O M0 ; 1 S-∈

析法和矩阵方程分析法，可达集分析法可以解决各种属性分析的问题，它的缺陷在于是一种穷尽方法，存在状态空间爆炸问题。矩阵方程分析法通过关联矩阵和相应的状态方程来

() 2如果 M∈S而且 M— J ( _ M’即经过迁移 f ) (,M的扫状态转移到 M’,则 M’,而且< M’ )∈S M,>∈R; () 3 S和除了() 2两种情况外，不包含其它元素。 1和() K ik r e结构可以表示为一有向图，通常是用来描述迁移 p系统，而且 K ik结构又可看作是一个有限状态机，可以按 r e p照自动机乘积算法实现 K ik r e结构和 Bih p i i自动机的积，从 c而来验证 P t网模型的性能。 er i

研究网的性质，但它仅限于对结构属性进行分析。而对系统模型的形式规约往往以某种逻辑形式给出，本文采用的是线性时态逻辑，它能描述系统行为的时间变化，这一点更适合描述具有离散性、时序性的安全联锁系统。针对这一点，本文提出了一种将 C N建模方法与 L L形式验证有机结合的 P T方法。该方法使用基于自动机判空算法，可以有效地解决在模型检验过程中状态空间爆炸的问题，从而能够从实际上解决像联锁逻辑系统这样复杂模型的分析问题，提高联锁逻辑 C N模型的可靠性和安全性。 P

1线性时态逻辑与 B t i . 2￣ h自动机 c线性时态逻辑 (n a—me e oa lgc T )由 1 eri t i t mp rl o i,L L是

P u l在 17年提出的，是计算机科学领域中命题 L L最 n ei 9 7 T常用的版本。线性时态逻辑现已被广泛地用于有限状态系统的行为描述” J。 Bi i自动机是6自动机的一种，广泛应用到模型检测 ih c 0基金项目：国家自然科学基金资助项目(0704 6640)

1相关的概念1有色 P t两的 K i e . 1 ei r r k结构 p本文采用的 C N是参考 K rJ s给出的

定义拉， P P ute e n n]C N是一种具有完善理论基础的形式化语言，同时又具有图形结

作者简介：杜军威(94 ), 17 -,男博士研究生、讲师，主研方向：安全软件形式化技术，安全软件测试，安全软件模型检验；徐中伟， 博士、教授、博士生导师；宋波，士研究生博

构并带有很强直观意义的建模工具。C N已为许多实际应 P成用领域建模的一种有效工具，其应用涉及到柔性制造、并行

收稿日期：20—22 061—5

Ema:dj@13 o - i _w 6. m l c3— 3

一