This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Analytic Verification of Flight Software
September/October 1998 (vol. 13 no. 5)
pp. 45-49
In the realm of space exploration, the biggest obstacle to widespread application of autonomy in flight software is not technical feasibility; it is doubt about its trustworthiness as a replacement for human-in-the-loop decision-making. Autonomous control systems raise difficult verification and validation issues because, unlike conventional sequencer-based open-loop systems that perform transactions visible through uplink and downlink communications, they close many control loops and arbitrate many resources onboard with specialized reasoning in multiple concurrent threads. V&V techniques are needed that significantly increase confidence in these decision-making control systems. This article shows two ways of applying analytic verification: at design time using model checking to guarantee that specific conditions are never violated, and at runtime using embedded behavior auditors to verify that the implemented integrated system respects similar conditions. This approach suggests two changes in software-development practice: modeling the high-level design formally enough to enable model checking through tools such as Spin, and codeveloping operational code along with auditor specifications.
Citation:
Michael Lowry, Daniel Dvorak, "Analytic Verification of Flight Software," IEEE Intelligent Systems, vol. 13, no. 5, pp. 45-49, Sept.-Oct. 1998, doi:10.1109/5254.722359
Usage of this product signifies your acceptance of the Terms of Use.