| id |
ndltd-OhioLink-oai-etd.ohiolink.edu-ucin1201537607
|
| record_format |
oai_dc
|
| spelling |
ndltd-OhioLink-oai-etd.ohiolink.edu-ucin12015376072021-08-03T06:12:23Z FORMAL VERIFICATION OF TIME CONSTRAINED UAV TASK ALLOCATION USING MODEL-CHECKING KASAM, SUMAN 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. 2008-04-18 English text University of Cincinnati / OhioLINK http://rave.ohiolink.edu/etdc/view?acc_num=ucin1201537607 http://rave.ohiolink.edu/etdc/view?acc_num=ucin1201537607 unrestricted This thesis or dissertation is protected by copyright: all rights reserved. It may not be copied or redistributed beyond the terms of applicable copyright laws.
|
| collection |
NDLTD
|
| language |
English
|
| sources |
NDLTD
|
| author |
KASAM, SUMAN
|
| spellingShingle |
KASAM, SUMAN
FORMAL VERIFICATION OF TIME CONSTRAINED UAV TASK ALLOCATION USING MODEL-CHECKING
|
| author_facet |
KASAM, SUMAN
|
| author_sort |
KASAM, SUMAN
|
| title |
FORMAL VERIFICATION OF TIME CONSTRAINED UAV TASK ALLOCATION USING MODEL-CHECKING
|
| title_short |
FORMAL VERIFICATION OF TIME CONSTRAINED UAV TASK ALLOCATION USING MODEL-CHECKING
|
| title_full |
FORMAL VERIFICATION OF TIME CONSTRAINED UAV TASK ALLOCATION USING MODEL-CHECKING
|
| title_fullStr |
FORMAL VERIFICATION OF TIME CONSTRAINED UAV TASK ALLOCATION USING MODEL-CHECKING
|
| title_full_unstemmed |
FORMAL VERIFICATION OF TIME CONSTRAINED UAV TASK ALLOCATION USING MODEL-CHECKING
|
| title_sort |
formal verification of time constrained uav task allocation using model-checking
|
| publisher |
University of Cincinnati / OhioLINK
|
| publishDate |
2008
|
| url |
http://rave.ohiolink.edu/etdc/view?acc_num=ucin1201537607
|
| work_keys_str_mv |
AT kasamsuman formalverificationoftimeconstraineduavtaskallocationusingmodelchecking
|
| _version_ |
1719432710093537280
|
