计算机科学
計算機科學
계산궤과학
COMPUTER SCIENCE
2014年
5期
254-262,269
,共10页
数据约束%实时系统%连续时间%MARTE%ZIA%模型检测
數據約束%實時繫統%連續時間%MARTE%ZIA%模型檢測
수거약속%실시계통%련속시간%MARTE%ZIA%모형검측
Data constraints%Real-time system%Continuous-time%MARTE%ZIA%Model checking
带数据约束的实时系统是指一种既带有时间约束又带有数据变量约束的计算系统.目前将离散数据约束和连续时间约束统一在一个模型中的规范及验证研究较少.文中提出了一种既带有连续数据约束又带有离散数据约束的规范——基于连续时间的ZIA规范,并给出它的时序逻辑.MARTE是UML在嵌入式实时系统领域的建模规范,在工业界的应用非常广泛,但是目前对其模型检测的研究较少.在MARTE的基础上扩展Z,提出了Z-MARTE,并将Z-MARTE转换为基于连续时间的ZIA模型,在实现对连续时间ZIA模型检测的同时,也实现了对Z-MARTE的模型检测.最后通过一个实例进行验证,说明此方法可行有效.
帶數據約束的實時繫統是指一種既帶有時間約束又帶有數據變量約束的計算繫統.目前將離散數據約束和連續時間約束統一在一箇模型中的規範及驗證研究較少.文中提齣瞭一種既帶有連續數據約束又帶有離散數據約束的規範——基于連續時間的ZIA規範,併給齣它的時序邏輯.MARTE是UML在嵌入式實時繫統領域的建模規範,在工業界的應用非常廣汎,但是目前對其模型檢測的研究較少.在MARTE的基礎上擴展Z,提齣瞭Z-MARTE,併將Z-MARTE轉換為基于連續時間的ZIA模型,在實現對連續時間ZIA模型檢測的同時,也實現瞭對Z-MARTE的模型檢測.最後通過一箇實例進行驗證,說明此方法可行有效.
대수거약속적실시계통시지일충기대유시간약속우대유수거변량약속적계산계통.목전장리산수거약속화련속시간약속통일재일개모형중적규범급험증연구교소.문중제출료일충기대유련속수거약속우대유리산수거약속적규범——기우련속시간적ZIA규범,병급출타적시서라집.MARTE시UML재감입식실시계통영역적건모규범,재공업계적응용비상엄범,단시목전대기모형검측적연구교소.재MARTE적기출상확전Z,제출료Z-MARTE,병장Z-MARTE전환위기우련속시간적ZIA모형,재실현대련속시간ZIA모형검측적동시,야실현료대Z-MARTE적모형검측.최후통과일개실례진행험증,설명차방법가행유효.
