小型微型计算机系统
小型微型計算機繫統
소형미형계산궤계통
MINI-MICRO SYSTEMS
2013年
9期
2025-2029
,共5页
李月星%李晓娟%关永%王瑞%张杰%魏洪兴
李月星%李曉娟%關永%王瑞%張傑%魏洪興
리월성%리효연%관영%왕서%장걸%위홍흥
SpaceWire%概率模型检测%马尔科夫决策过程%PRISM
SpaceWire%概率模型檢測%馬爾科伕決策過程%PRISM
SpaceWire%개솔모형검측%마이과부결책과정%PRISM
SpaceWire%probabilistic model checking%Markov decision processes%PRISM
SpaceWire是应用于航空航天领域的高速通信总线标准,保证其设计的可靠性和正确性至关重要.本文通过概率模型检测的方法对SpaceWire的交换层设计进行形式化建模与量化分析.基于马尔科夫决策过程(MDP)对交换层的链路初始化及正常运行过程建立形式化概率模型,模型包括发送方、接收方和信道,提取SpaceWire交换层的4个关键属性,用概率计算树逻辑(PCTL)进行描述,运用PRISM平台对SpaceWire交换层设计进行验证和分析;并获得信道丢包概率不同情况下,链路初始化成功以及正常运行时数据包正确传输的概率,这种定量形式化分析结果可为SpaceWire的设计和实现提供参考依据.
SpaceWire是應用于航空航天領域的高速通信總線標準,保證其設計的可靠性和正確性至關重要.本文通過概率模型檢測的方法對SpaceWire的交換層設計進行形式化建模與量化分析.基于馬爾科伕決策過程(MDP)對交換層的鏈路初始化及正常運行過程建立形式化概率模型,模型包括髮送方、接收方和信道,提取SpaceWire交換層的4箇關鍵屬性,用概率計算樹邏輯(PCTL)進行描述,運用PRISM平檯對SpaceWire交換層設計進行驗證和分析;併穫得信道丟包概率不同情況下,鏈路初始化成功以及正常運行時數據包正確傳輸的概率,這種定量形式化分析結果可為SpaceWire的設計和實現提供參攷依據.
SpaceWire시응용우항공항천영역적고속통신총선표준,보증기설계적가고성화정학성지관중요.본문통과개솔모형검측적방법대SpaceWire적교환층설계진행형식화건모여양화분석.기우마이과부결책과정(MDP)대교환층적련로초시화급정상운행과정건립형식화개솔모형,모형포괄발송방、접수방화신도,제취SpaceWire교환층적4개관건속성,용개솔계산수라집(PCTL)진행묘술,운용PRISM평태대SpaceWire교환층설계진행험증화분석;병획득신도주포개솔불동정황하,련로초시화성공이급정상운행시수거포정학전수적개솔,저충정량형식화분석결과가위SpaceWire적설계화실현제공삼고의거.
