Title: Formal Specification and Reachability Analysis of ICAROUS Software Architecture
Speaker: Camilo Rocha, NIA Visitor
Date: Thursday, December 1, 2016
Time: 10:30am
Location: NIA, Room 141
Host: C. Munoz, NASA/LaRC
Abstract: ICAROUS is a software library that includes a collection of formally verified and configurable algorithms supporting the implementation of safe and autonomous unmanned aircraft applications and missions. This talk reports on preliminary research on the formal specification of ICAROUS software architecture in the Maude System. The ultimate research goal of this effort is twofold. On the one hand, the aim is at mechanically verifying important reachability properties of the architecture such as deadlock freedom and absence of race conditions. On the other hand, the aim is at complementing the existing library of formally verified algorithms with assurances about the way they are composed and integrated in the ICAROUS infrastructure. In this research, the newly developed rewriting modulo SMT technique will be used to produce a symbolic and executable semantics of the ICAROUS software architecture that can be exercised against symbolic constraints representing, potentially, infinitely many input data.
Bio: Camilo Rocha is an Associate Professor in the Department of Electronics and Computer Science at the Pontificia Universidad Javeriana (Cali, Colombia). He earned a B.Sc. and a M.Sc. degree in Informatics from the Universidad de los Andes (Bogotá, Colombia), and a M.Sc. degree in Mathematics and a Ph.D. degree in Computer Science from the University of Illinois (Urbana, USA). He is currently working on developing symbolic techniques and tools for reachability analysis in rewriting logic. Prof. Rocha has been a regular visitor at NIA where he has been involved, mainly, in efforts towards the formal semantics and verification of NASA’s PLEXIL language. Details and more information about his research can be found at his personal webpage: http://camilorocha.info.