12.1.16 Rocha

12.1.16 Rocha

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:



100 Exploration Way
Hampton, VA 23666