Open Access Open Access  Restricted Access Subscription Access

Formal Verification of Process Communications in Operational Flight Program for a Small-Scale Unmanned Helicopter

Dong-Ah Lee, Junbeom Yoo, Doo-Hyun Kim


Formal verification plays an important role in demonstrating safety and correctness of safety-critical systems such as airplanes and helicopters. Small-scale unmanned helicopters have been increasingly developed and deployed for various scientific, commercial and defense applications. The HELISCOPE project is aiming to develop an unmanned helicopter and its on-flight embedded computing system for navigation and real-time transmission of the motion video using wireless communication schemes. This paper introduces our experience on the formal verification of OFP (Operational Flight Program) in the HELISCOPE project. The OFP provides real-time controls with various sensors and actuators, and should be sufficiently verified through formal verification techniques. We focused on the formal verification of process communications between four sensing processes and one controller to access a critical section of shared memory area mutually exclusively.

Full Text:



D. H. Kim, K. Nodir, C.H. Chang, J.G. Kim ”HELISCOPE Project: Research Goal and Survey on Related Technologies”, In the Proceeding of 12th IEEE International Symposium on Object /Component / Service-Oriented Real-Time Distributed Computing (ISORC), pp.112-118, Tokyo, 2009.

S. G. Kim, S.H. Song, C. H. Chang, D. H. Kim, S. Hew, J. G. Kim “Design and implementation of an Operational Flight Program for an Unmanned Helicopter FCC Based on the TMO Scheme”, Proceedings of the 7th IFIP WG 10.2 International Workshop on Software Technologies for Embedded and Ubiquitous Systems(SEUS), pp.1-11, Newport Beach, CA, USA, 2009.

Holzmann, G. J. "The Model Checker SPIN", IEEE Transactions on Software Engineering, Vol. 23, No. 5, May 1997.

D. Harel., “On Visual Formalism,” Communication of ACM, Vo.31, 5, pp.514-530, 1988.


Kim, K.H., Kopetz, H. “A Real-Time Object Model RTO.k and an Experimental Investigation of Its Potentials”, In: 18th IEEE Computer Software & Applications Conference, pp. 392–402, Los Alamitos, 1994

Havelund, K. Lowry, M. Penix, J., “Formal analysis of a space-craft controller using SPIN”, Software Engineering, IEEE Transactions on, Vol.27, 8, pp. 749 – 765, 2001

B. Pell, E. Gat, R. Keesing, N. Muscettola, and B. Smith, “Plan Execution for Autonomous Spacecraft”, In Proceedings of the International Joint Conference on Artificial Intelligence, pp. 1234-1239, Japan, 1997



  • There are currently no refbacks.