计算机科学 ›› 2016, Vol. 43 ›› Issue (2): 113-117.doi: 10.11896/j.issn.1002-137X.2016.02.026
李艳春,李晓娟,关永,王瑞,张杰,魏洪兴
LI Yan-chun, LI Xiao-juan, GUAN Yong, WANG Rui, ZHANG Jie and WEI Hong-xing
摘要： 空间总线(SpaceWire)协议是应用于航空航天领域的高速通信总线协议, 保证其可靠性至关重要。但是由于通信系统具有队列量、分布控制和并发性等特点,传统仿真模拟的验证方法存在不完备性的问题,采用模型检测方法对高层次属性进行验证时,通常会出现状态爆炸的问题。基于xMAS模型对SpaceWire通信系统中的信誉逻辑进行形式化建模、验证,xMAS模型既保留了底层的结构信息,又可以验证高层次的属性。对通信系统中信誉逻辑进行抽象进而建立了xMAS模型,提取了可发送性、可接收性和数据一致性等3个关键属性,运用定理证明工具ACL2对关键属性的正确性进行了自动验证。该方法为验证指导下的系统设计提供了有效的参考。
| [1] ECSS.Space Engineering:SpaceWire-Links,nodes,routers,and networks(ECSS-E-50-12A)[S].The Netherlands:ESA Publications Division ESTEC,2003 [2] Chatterjee S,Kishinevsky M.Automatic Generation of Inductive Invariants from High-Level Microarchitectu-ral Models of Communication Fabrics[J].Formal Methods in System Design,2012,40(2):147-169 [3] Verbeek F,Schmaltz J.Hunting deadlocks efficiently in microarchitectural models of communication fabrics[C]∥Formal Me-thods in Computer-Aided Design(FMCAD).2011:223-231 [4] Chatterjee S,Kishinevsky M O.Quick formal modeling of communication fabrics to enable verification[C]∥High Level Design Validation and TestWorkshop (HLDVT).IEEE,2010:42-49 [5] Gotmanov A,Chatterjee S,Kishinevsky M.Verifying deadlock-freedom of communication fabrics[C]∥Verification,Model Checking,and Interpretation (VMCAI).2011:214-231 [6] Ray S,Brayton R K.Scalable Progress Verification in Credit-Based Flow-Control Systems[C]∥Design,Automation & Test in Europe Conference & Exhibition(DATE).2012:905-910 [7] Borrione D,Helmy A,Pierre L,et al.A generic model for formally verifying NoC communication architectures:a case study[C]∥Networks-on-Chip (NOCS).2007:127-136 [8] Verbeek F.Formal Verification of on-Chip Communication Fabrics[M].Radboud University Nijmegen,2013 [9] van Gastel B,Schmaltz J.A formalisation of XMAS[C]∥Electronic Proceeding in Theoretical Computer Science(EPTCS).2013:111-126 [10] Kaufmann M,Moore J S,Manolios P.Computer-Aided Reaso-ning:An Approach[M].Norwell,MA:Kluwer Academic Publishers,2000 [11] Kaufmann M,Moore J S,Manolios P.Computer-Aided Reaso-ning:ACL2 Case Studies[M].Norwell,MA:Kluwer Academic Publishers,2000 [12] Joosten S J C,Verbeek F,Schmaltz J.WickedXmas:Designing and Verifying on-chip Communication Fabrics[C]∥Design and Implementation of Formal Tools and Systems(DIFTS).2014:1-8 [13] Kishinevsky M,Gotmanov A,Viktorov Y.Challenges in Verifying Communication Fabrics[C]∥Interactive theorem proving (ITP).2011:18-21 [14] Zhang Yu-peng,Shi Zhi-ping,Guan Yong,et al.Formal Verification of SpaceWire Decoding Circuit in HOL4[J].Journal of Chinese Systems,2013,8:1959-1963(in Chinese) 张玉鹏,施智平,关永,等.SpaceWire译码电路在HOL4中的形式化[J].小型微型计算机系统,2013,8:1959-1963 [15] Dong Ling-ling,Guan Yong,Li Xiao-juan,et al.Verification for SpaceWire error detection mechanism by LTL model checking [J].Computer Engineering and Applications,2012,8(22):88-94(in Chinese) 董玲玲,关永,李晓娟,等.用LTL模型检验的方法验证SpaceWire检错机制[J].计算机工程与应用,2012,8(22):88-94 |
| No related articles found! |
|
||
首页