@InProceedings{ALAS2014,
  Title                    = {Temporal Precedence Checking for Switched Models and its Application to a Parallel Landing Protocol},
  Author                   = {Parasara Sridhar Duggirala and Le Wang and Sayan Mitra and Cesar Munoz and Mahesh Viswanathan},
  Booktitle                = {International Conference on Formal Methods (FM 2014), Singapore},
  Year                     = {2014},

  Abstract                 = {We present an algorithm for checking temporal precedence properties of nonlinear switched systems. This class of properties subsume bounded safety and capture requirements about visiting a sequence of predicates within given time intervals. Our algorithm handles nonlinear predicates that arise from dynamics-based predictions used in alerting protocols for state-of-the-art transportation systems. It is sound and relatively complete for nonlinear switch systems that robustly satisfy the given property. The algorithm is implemented in our Compare Execute Check Engine (C2E2) using validated simulations. As a case study, we consider NASA's Adjacent Landing Alerting System (ALAS), which is an alerting protocol for closely spaced parallel runways.Using our approach, we study the performance of the ALAS protocol with respect to false and missed alerts for different operating conditions such as initial velocities, bankangles, initial longitudinal separation, and runway configurations.},
  Keywords                 = {Verification, Aerospace},
  Pdfslidesurl             = {research/presentations/2014/PSD-FM.pdf},
  Pdfurl                   = {research/2014/alas2014.pdf},
  Url                      = {http://link.springer.com/chapter/10.1007%2F978-3-319-06410-9_16}
}

{"_id":"SpguXpuDAysLriDkr","bibbaseid":"duggirala-wang-mitra-munoz-viswanathan-temporalprecedencecheckingforswitchedmodelsanditsapplicationtoaparallellandingprotocol-2014","downloads":0,"creationDate":"2017-10-05T05:28:26.978Z","title":"Temporal Precedence Checking for Switched Models and its Application to a Parallel Landing Protocol","author_short":["Duggirala, P. S.","Wang, L.","Mitra, S.","Munoz, C.","Viswanathan, M."],"year":2014,"bibtype":"inproceedings","biburl":"http://mitras.ece.illinois.edu/research/sayan.bib","bibdata":{"bibtype":"inproceedings","type":"inproceedings","title":"Temporal Precedence Checking for Switched Models and its Application to a Parallel Landing Protocol","author":[{"firstnames":["Parasara","Sridhar"],"propositions":[],"lastnames":["Duggirala"],"suffixes":[]},{"firstnames":["Le"],"propositions":[],"lastnames":["Wang"],"suffixes":[]},{"firstnames":["Sayan"],"propositions":[],"lastnames":["Mitra"],"suffixes":[]},{"firstnames":["Cesar"],"propositions":[],"lastnames":["Munoz"],"suffixes":[]},{"firstnames":["Mahesh"],"propositions":[],"lastnames":["Viswanathan"],"suffixes":[]}],"booktitle":"International Conference on Formal Methods (FM 2014), Singapore","year":"2014","abstract":"We present an algorithm for checking temporal precedence properties of nonlinear switched systems. This class of properties subsume bounded safety and capture requirements about visiting a sequence of predicates within given time intervals. Our algorithm handles nonlinear predicates that arise from dynamics-based predictions used in alerting protocols for state-of-the-art transportation systems. It is sound and relatively complete for nonlinear switch systems that robustly satisfy the given property. The algorithm is implemented in our Compare Execute Check Engine (C2E2) using validated simulations. As a case study, we consider NASA's Adjacent Landing Alerting System (ALAS), which is an alerting protocol for closely spaced parallel runways.Using our approach, we study the performance of the ALAS protocol with respect to false and missed alerts for different operating conditions such as initial velocities, bankangles, initial longitudinal separation, and runway configurations.","keywords":"Verification, Aerospace","pdfslidesurl":"research/presentations/2014/PSD-FM.pdf","pdfurl":"research/2014/alas2014.pdf","url":"http://link.springer.com/chapter/10.1007%2F978-3-319-06410-9_16","bibtex":"@InProceedings{ALAS2014,\n Title = {Temporal Precedence Checking for Switched Models and its Application to a Parallel Landing Protocol},\n Author = {Parasara Sridhar Duggirala and Le Wang and Sayan Mitra and Cesar Munoz and Mahesh Viswanathan},\n Booktitle = {International Conference on Formal Methods (FM 2014), Singapore},\n Year = {2014},\n\n Abstract = {We present an algorithm for checking temporal precedence properties of nonlinear switched systems. This class of properties subsume bounded safety and capture requirements about visiting a sequence of predicates within given time intervals. Our algorithm handles nonlinear predicates that arise from dynamics-based predictions used in alerting protocols for state-of-the-art transportation systems. It is sound and relatively complete for nonlinear switch systems that robustly satisfy the given property. The algorithm is implemented in our Compare Execute Check Engine (C2E2) using validated simulations. As a case study, we consider NASA's Adjacent Landing Alerting System (ALAS), which is an alerting protocol for closely spaced parallel runways.Using our approach, we study the performance of the ALAS protocol with respect to false and missed alerts for different operating conditions such as initial velocities, bankangles, initial longitudinal separation, and runway configurations.},\n Keywords = {Verification, Aerospace},\n Pdfslidesurl = {research/presentations/2014/PSD-FM.pdf},\n Pdfurl = {research/2014/alas2014.pdf},\n Url = {http://link.springer.com/chapter/10.1007%2F978-3-319-06410-9_16}\n}\n\n","author_short":["Duggirala, P. S.","Wang, L.","Mitra, S.","Munoz, C.","Viswanathan, M."],"key":"ALAS2014","id":"ALAS2014","bibbaseid":"duggirala-wang-mitra-munoz-viswanathan-temporalprecedencecheckingforswitchedmodelsanditsapplicationtoaparallellandingprotocol-2014","role":"author","urls":{"Paper":"http://link.springer.com/chapter/10.1007%2F978-3-319-06410-9_16"},"keyword":["Verification","Aerospace"],"downloads":0,"html":""},"search_terms":["temporal","precedence","checking","switched","models","application","parallel","landing","protocol","duggirala","wang","mitra","munoz","viswanathan"],"keywords":["hybrid systems","verification","aerospace systems","aerospace"],"authorIDs":["59d5c2fab06428b81f000015"],"dataSources":["yMXZF3wFnctJRohbP"]}