高技术通讯
高技術通訊
고기술통신
Chinese High Technology Letters
2015年
4期
350-356
,共7页
一致性测试%实时性%并发性%形式化方法%精化关系
一緻性測試%實時性%併髮性%形式化方法%精化關繫
일치성측시%실시성%병발성%형식화방법%정화관계
conformance test%real-time%concurrency%formal method%refinement
基于时间通信顺序进程(TCSP)语言——一种用于建模、验证实时并发系统的形式化语言,进行了一种新型实时并发系统测试方法的研究,以提高测试的覆盖率和完整度.首先研究了实时并发系统的输入、输出一致性关系,然后在时间迹、时间拒绝两种框架下,分别定义了最小不满足时间迹、最小拒绝集合,分情况研究了其测试过程.在TCSP的稳定失效模型下,将输出事件加入拒绝事件集合,最后提出了基于通信顺序进程(CSP)精化关系,且辨别输入、输出事件的实时测试模型,因此测试时不仅能精确地表示系统属性及行为,而且能利用该语言的精化关系定义测试的一致性测试关系.
基于時間通信順序進程(TCSP)語言——一種用于建模、驗證實時併髮繫統的形式化語言,進行瞭一種新型實時併髮繫統測試方法的研究,以提高測試的覆蓋率和完整度.首先研究瞭實時併髮繫統的輸入、輸齣一緻性關繫,然後在時間跡、時間拒絕兩種框架下,分彆定義瞭最小不滿足時間跡、最小拒絕集閤,分情況研究瞭其測試過程.在TCSP的穩定失效模型下,將輸齣事件加入拒絕事件集閤,最後提齣瞭基于通信順序進程(CSP)精化關繫,且辨彆輸入、輸齣事件的實時測試模型,因此測試時不僅能精確地錶示繫統屬性及行為,而且能利用該語言的精化關繫定義測試的一緻性測試關繫.
기우시간통신순서진정(TCSP)어언——일충용우건모、험증실시병발계통적형식화어언,진행료일충신형실시병발계통측시방법적연구,이제고측시적복개솔화완정도.수선연구료실시병발계통적수입、수출일치성관계,연후재시간적、시간거절량충광가하,분별정의료최소불만족시간적、최소거절집합,분정황연구료기측시과정.재TCSP적은정실효모형하,장수출사건가입거절사건집합,최후제출료기우통신순서진정(CSP)정화관계,차변별수입、수출사건적실시측시모형,인차측시시불부능정학지표시계통속성급행위,이차능이용해어언적정화관계정의측시적일치성측시관계.
