Formal Modeling and Verification of Operational Flight Program in a Small-Scale Unmanned Helicopter
Publication: Journal of Aerospace Engineering
Volume 25, Issue 4
Abstract
Formal verification has played an important role in demonstrating correctness of safety-critical systems. Small-scale unmanned helicopters have been increasingly developed for various purposes such as scientific exploration and commercial or defense applications. The HELISCOPE project in Korea aims to develop a small-scale unmanned helicopter and its onboard embedded computing system for flight control and real-time transmission of multimedia data. This paper shares the authors’ experience on the formal verification of the operational flight program (OFP) developed in the project. Because the OFP provides real-time controls on various sensors and actuators, demonstration of its correctness through formal verifications has been strongly recommended. This paper focuses on real-time process communications among sensing processes, a monitoring process, and a controller process. They all share a common data area. Two different formal models were developed for the OFP and verified with the SPIN and UPPAAL model checkers. While the SPIN model checker is widely used for modeling and verifying communication protocols, the real-time behavior of the OFP controller needs more advanced techniques that can handle real-time properties explicitly, i.e., timed automata and the UPPAAL verification system. The verification of the OFP found several safety-critical faults; they were all reported to development teams and fixed.
Get full access to this article
View all available purchase options and get full access to this article.
Acknowledgments
This research was supported by the MKE (The Ministry of Knowledge Economy), Korea, under the ITRC (Information Technology Research Center) support program supervised by the NIPA (National IT Industry Promotion Agency) (NIPA-2011-C1090-1131-0003) and (NIPA-2011-C1090-1131-0008).
References
Alur, R., and Dill, D. L. (1994). “A theory of timed automata.” Theor. Comput. Sci., 126(2), 183–235.
Bengtsson, J., Larsen, K. G., Larsson, F., Pettersson, P., and Yi, W. (1995). “UPPAAL—A tool suite for automatic verification of real-time systems.” Hybrid systems, Springer, Heidelberg, Germany, 232–243.
Berard, B., et al. (2001). Systems and software verification: Model-checking techniques and tools, Springer, Heidelberg, Germany.
Brayton, R. K., et al. et al.(1996). “VIS: A system for verification and synthesis.” Computer aided verification, R. Alur and T. A. Henzinger, eds., Springer, Heidelberg, Germany, 428–432.
Chaudemar, J.-C., Bensana, E., and Seguin, C. (2010). “Model based safety analysis for an Unmanned Aerial System.” Proc., Dependable Robots in Human Environments 2010, IEEE Robotics and Automation Society, Toulouse, France.
Clarke, E., Grumberg, O., and Peled, D. (1999). Model checking, MIT Press, Cambridge, MA.
Clarke, E. M., Emerson, E. A., and Sistla, A. P. (1986). “Automatic verification of finite-state concurrent systems using temporal logic specifications.” ACM Trans. Program. Lang. Syst., 8(2), 244–263.
Clarke, E. M., Kroening, D., and Lerda, F. (2004). “A tool for checking ANSI-C programs.” TACAS 2004, K. Jensen, A. Podelski, eds., Springer, Heidelberg, Germany, 168–176.
Gordon, M. J. C., and Melham, T. (1993). Introduction to HOL: A theorem proving environment for higher order logic, Cambridge University Press, Cambridge, U.K.
Havelund, K., Lowry, M., and Penix, J. (1998). “Formal analysis of a space craft controller using SPIN.” Proc., 4th SPIN Workshop, 749–765.
Henzinger, T. A., Jhala, R., Majumdar, R., and Sutre, G. (2003). “Software verification with BLAST.” Proc., 10th Int. SPIN Workshop, Vol. 2648, Springer, 235–239.
Holzmann, G. J., (1991). Design and validation of computer protocols, Prentice Hall, Englewood Cliffs, NJ.
Holzmann, G. J. (1997). “The model checker spin.” IEEE Trans. Software Eng., 23(5), 279–295.
Huang, S., and Cheng, K. (1998). Formal equivalence checking and design debugging. Frontiers in electronic testing, Kluwer Academic, Boston.
Kasam, S. (2008). “Formal verification of time constrained UAV task allocation using model-checking. MS thesis, Univ. of Cincinnati, Cincinnati, OH.
Kim, D.-H., Nodir, K., Chang, C.-H., and Kim, J.-G. (2009a). “HELISCOPE project: Research goal and survey on related technologies.” Proc., IEEE 12th Int. Symp. on Object/Component/Service-Oriented Real-Time Distributed Computing in Tokyo, IEEE Computer Society Press, Los Alamitos, CA, 112–118.
Kim, J. G., et al. (2009b). “TMO-eCos2.0 and its development environment for timeliness guaranteed computing.” Proc., 2009 Software Technologies for Future Dependable Distributed Systems, IEEE Computer Society, Washington, DC, 164–168.
Kim, K., and Kopetz, H. (1994). “A real-time object model RTO.k and an experimental investigation of its potentials.” Proc., 18th Int. Annual Computer Software and Applications Conf., 1994 (COMPSAC 94), IEEE, Washington, DC, 392–402.
Kim, S.-G., Song, S.-H., Chang, C.-H., Kim, D.-H., Heu, S., and Kim, J.-G. (2009c). “Design and implementation of an operational flight program for an unmanned helicopter FCC based on the TMO scheme.” Proc., SEUS 2009, Int. Federation for Information Processing, Newport Beach, CA, 1–11.
Lee, D.-A., Yoo, J., and Kim, D. (2010a). “Formal verification of process communications in operational flight program for a small-scale unmanned helicopter.” Proc., 6th Int. Conf. on Intelligent Unmanned Systems (ICIUS), Bali, Indonesia, 91–96.
Lee, D.-A., Yoon, S., Lee, M.-Y., Jin, H.-W., and Yoo, J. (2010b). “Formal verification of protocol stack for most network service using spin.” Proc., Korea Computer Congress, Korean Institute of Information Scientists and Engineers, Seoul, 60–61.
McMillan, K. (1993). Symbolic model checking, Kluwer Academic, Boston.
Owre, S., Rushby, J. M., and Shankar, N. (1992). “PVS: A prototype verification system.” CADE 1992, D. Kapur, ed., 748–752.
Peled, D. (2001). Software reliability methods. Texts in computer science, Springer, New York.
Wing, J. M. (1990). “A specifier’s introduction to formal methods.” Computer, 23(9), 8–22.
Wu, X., Ling, H., and Dong, Y. (2009). “On modeling and verifying of application protocols of TTCAN in flight-control system with UPPAAL.” Proc., 2009 Int. Conf. on Embedded Software and Systems, IEEE Computer Society, Washington, DC, 572–577.
Yoo, J., Jee, E., and Cha, S. D. (2009). “Formal modeling and verification of safety-critical software.” IEEE Software, 26(3), 42–49.
Information & Authors
Information
Published In
Journal of Aerospace Engineering
Volume 25 • Issue 4 • October 2012
Pages: 530 - 540
Copyright
© 2012 American Society of Civil Engineers.
History
Received: Jan 24, 2011
Accepted: Sep 16, 2011
Published online: Sep 19, 2011
Published in print: Oct 1, 2012
Authors
Metrics & Citations
Metrics
Citations
Download citation
If you have the appropriate software installed, you can download article citation data to the citation manager of your choice. Simply select your manager software from the list below and click Download.