微信服务号

微信订阅号

2025-4-15- 3
Home > Archive>Volume 26, Issue 2, 2015 >181-201. DOI:10.13328/j.cnki.jos.004775
PDF HTML XML Export Cite reminder
Avionics System Testing Based on Formal Methods
Author:
Affiliation:

  • Article
    • | |
  • Metrics
    • |
  • Reference [20]
    • |
  • Related [20]
    • |
  • Cited by [1]
    • | |
  • Comments
    Abstract:

    With the rapid development of aviation models, the degree of digitalization of avionics systems becomes higher and higher, and the proportion of the software in those systems becomes larger and larger. In this paper, software architecture and formal modeling of avionics systems are discussed. Further, a system level integrated testing method based on formalization for avionics system from static and dynamic aspects is proposed. At last, the effectiveness of the proposed approach is evaluated through an integrated testing system designed and implemented in this research.

    Reference
    [1] Zheng ZM, Ma SL, Li W, Wei W, Jiang X, Zhang ZL, Guo BH. Dynamical characteristics of software trustworthiness and their evolutionary complexity. Science in China (Series F: Information Sciences), 2009,52(8):1328-1334.[doi: 10.1007/s11432-009-0137-2]
    [2] Zheng ZM, Ma SL, Li W, Jiang X, Wei W, Ma L, Tang ST. Complexity of software trustworthiness and its dynamical statistical analysis methods. Science in China (Series F: Information Sciences), 2009,52(9):1651-1657.[doi: 10.1007/s11432-009-0143-4]
    [3] Li YM, Wang JQ, Zheng JG, Wang CQ. About standard avionics ATE of overseas. Computer Measurement & Control, 2004, 12(1):1-5 (in Chinese with English abstract).[doi: 10.3321/j.issn:1671-4598.2004.01.001]
    [4] Liu JF, Wang H. Study on architecture of overseas avionics ATS. Measurement & Control Technology, 2002,21(1):5-8 (in Chinese with English abstract).[doi: 10.3969/j.issn.1000-8829.2002.01.002]
    [5] Yu JS, Li XS. Future trends of the U.S. military ATS. Measurement & Control Technology, 2001,20(12):1-3 (in Chinese with English abstract).[doi: 10.3969/j.issn.1000-8829.2001.12.001]
    [6] Cai XB, Wang H, Wang HW. Development of French universal automatic test equipment. Measurement & Control Technology, 2000,19(6):1-4 (in Chinese with English abstract).
    [7] Wen XS, Xu YW, Yi XS, Chen X. Intelligent BIT Theory and Application. Beijing: National Defense Industry Press, 2002 (in Chinese).
    [8] Tong J, Cai YW, Bo W, Ren JT. Analysis of development and application of BIT technology. Ordnance Industry Automation, 2008, 27(4):5-7 (in Chinese with English abstract).[doi: 10.3969/j.issn.1006-1576.2008.04.002]
    [9] Guo YM, Cai XB, Zhang BZ, Zhai ZJ. Review of prognostics and health management technology. Computer Measurement & Control, 2008,16(9):1213-1216 (in Chinese with English abstract).
    [10] Byington CS, Roemer MJ, Galie T. Prognostic enhancements to diagnostic systems for improved condition-based maintenance. In: Proc. of the 2002 IEEE Aerospace Conf. 2000.[doi: 10.1109/AERO.2002.1036120]
    [11] Scheuren W. Safety & the military aircraft joint strike fighter prognostics & health management. In: Proc. of the AIAA. 1998.
    [12] Zhang T. Research on formal verification methods of model of complicated information system[Ph.D. Thesis]. Harbin: Harbin Engineering University, 2011 (in Chinese with English abstract).
    [13] Praxis AH. Using formal methods to develop an ATC information system. IEEE Software, 1996,13(2):66-76.[doi: 10.1109/52.50 6463]
    [14] Introduction to TCAS II, version 7.1[Z]. Version 1.2, U.S. Department of Transportation, Federal Aviation Administration, 2014.
    [15] Vassev E, Hinchey M. Developing experimental models for NASA missions with ASSL. In: Proc. of the Workshop on Formal Methods for Aerospace (FMA) EPTCS 20. 2010. 88-94.
    [16] Zhu Y, Geng XT, Gao XG. The modelling and analysis of integrated avionics system based on stochastic Petri net. Fire Control and Command Control, 2006,31(1):41-44 (in Chinese with English abstract).[doi: 10.3969/j.issn.1002-0640.2006.01.013]
    [17] Miller SP, Greve DA, Wilding MM, Collins R, Rapids C, Srivas M. Formal Verification of the AAMP-FV Microcode. NASA/CR-1999-208992, Menlo Park: SRI Int'l, 1999.
    [18] Bieber P, Castel C, Seguin C. Combination of fault tree analysis and model checking for safety assessment of complex system. In: Proc. of the 4th European Dependable Computing Conf. LNCS 2485, Berlin, Heidelberg: Springer-Verlag, 2002. 19-31.[doi: 10. 1007/3-540-36080-8_3]
    [19] Wiels V, Delmas R, Doose D, Garoche PL, Cazin J, Durrieu G. Formal verification of critical aerospace software. Journal of Aerospace Lab, 2012,4.
    [20] Chu WK, Zhang FM, Fan XG. Overview on software architecture of integrated modular avionic systems. Acta Aeronauticaet Astronautica Sinica, 2009,30(10):1912-1917 (in Chinese with English abstract).[doi: 10.3321/j.issn:1000-6893.2009.10.020]
    Comments
    Comments
    分享到微博
    Submit
Get Citation

李睿,连航,马世龙,黎涛.基于形式化方法的航空电子系统检测.软件学报,2015,26(2):181-201

Copy
Share
Article Metrics
  • Abstract:
  • PDF:
  • HTML:
  • Cited by:
History
  • Received:June 23,2014
  • Revised:October 31,2014
  • Online: February 06,2015
Links:Institute of Software, CASChina Computer FederationCASNSFC
You are the first2035071Visitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address：4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code：100190
Phone：010-62562563 Fax：010-62562533 Email：jos@iscas.ac.cn
Technical Support：Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063