Skip to Main Content
 

Global Search Box

 
 
 
 

Files

File List


ucin1201537607.pdf (718.9 KB)

ETD Abstract Container

Abstract Header

FORMAL VERIFICATION OF TIME CONSTRAINED UAV TASK ALLOCATION USING MODEL-CHECKING

KASAM, SUMAN
http://rave.ohiolink.edu/etdc/view?acc_num=ucin1201537607

Abstract Details

2008, MS, University of Cincinnati, Engineering : Computer Engineering.
Real-time constrained systems are part of the everyday life. These are computer systems subjected to timing constraints along with non-timing constraints. They can be found in cars, aeroplanes, washing machines, toasters, chemical plants, power stations; anywhere that systems are used to control or interact with an environment where time is important. Many of them are safety critical systems where failure is unacceptable. Clearly, the need for reliable systems is critical. This reliability can be improved by exhaustive verifcation of the systems. Formal verifcation of real-time constrained systems has gained attention in the last few decades because of their efficiency in unveiling design errors not found by humans. However, formal verifcation methods are limited by their inability to control the state space explosion problem. The problem of state space explosion gets even more complex with timed systems. Numerous methods have been proposed to address the state space explosion problems with timed systems. However, existing techniques do not eliminate the problem of state space explosion, but mitigate the problem of state space explosion. For arger systems, the problem still persists. These real-time constrained systems include real-time constrained task allocation systems. Most of these real-time constrained task allocation problems are solved by modeling them as constrained optimization problems which use a set of constraint variables, linear constraint equations, and an optimization function. The problem of state space explosion is very high in such systems because of the large number of constraint variables. Thus, verifcation of such real-time constrained task allocation systems is still harder. In this thesis, we present a novel method to verify such real-time constrained task allocation systems using formal methods. The method verifies the task allocation (result) from the LP solver instead of the algorithms involved in the solver or the constraints. We then proposed techniques to divide the huge state space into smaller state spaces to solve the problem of state space explosion with large problems.
Dr. Ranga Vemuri (Advisor)
131 p.

Recommended Citations

Citations

  • KASAM, S. (2008). FORMAL VERIFICATION OF TIME CONSTRAINED UAV TASK ALLOCATION USING MODEL-CHECKING [Master's thesis, University of Cincinnati]. OhioLINK Electronic Theses and Dissertations Center. http://rave.ohiolink.edu/etdc/view?acc_num=ucin1201537607

    APA Style (7th edition)

  • KASAM, SUMAN. FORMAL VERIFICATION OF TIME CONSTRAINED UAV TASK ALLOCATION USING MODEL-CHECKING. 2008. University of Cincinnati, Master's thesis. OhioLINK Electronic Theses and Dissertations Center, http://rave.ohiolink.edu/etdc/view?acc_num=ucin1201537607.

    MLA Style (8th edition)

  • KASAM, SUMAN. "FORMAL VERIFICATION OF TIME CONSTRAINED UAV TASK ALLOCATION USING MODEL-CHECKING." Master's thesis, University of Cincinnati, 2008. http://rave.ohiolink.edu/etdc/view?acc_num=ucin1201537607

    Chicago Manual of Style (17th edition)

ucin1201537607
546
© 2008, all rights reserved.
This open access ETD is published by University of Cincinnati and OhioLINK.