Séminaire de Neha RUNGTA à l’IRIT, le jeudi 15 mai à 15h30

Neha RUNGTA, chercheure à la NASA Ames Research Center, California est invitée à l’IRIT.

Elle fera un exposé le jeudi 15 mai à 15h30, à l’auditorium Jacques Herbrand, intitulé :

Ensuring Aviation Safety: Verification of Interactions between Automated Systems and Humans

Abstract:
The on-going transformation from the current US Air Traffic System (ATS) to the Next Generation Air Traffic System (NextGen) will force the introduction of new automated systems and most likely will cause automation to migrate from ground to air. This will yield new function allocations between humans and automation and therefore change the roles and responsibilities in the ATS. Yet, safety in NextGen is required to be at least as good as in the current system. We therefore need techniques to evaluate the safety of the interactions between humans and automation. Current human factor studies and simulation-based techniques fall short in front of the ATS complexity, and we need to add more automated techniques to simulations, such as model checking, which offers exhaustive coverage of the non-deterministic behaviors in nominal and off-nominal scenarios.

At NASA we have developed a verification approach based both on simulations and on model checking for evaluating the roles and responsibilities of humans and automation. Models are created using Brahms (a multi-agent framework) and we show that the traditional Brahms simulations can be integrated with automated exploration techniques based on model checking, thus offering a complete exploration of the behavioral space of the scenario. Our framework takes as input a Brahms model along with a Java implementation of its semantics. We then use Java PathFinder developed at NASA Ames to explore all possible behaviors of the model and, also, produce a generalized intermediate representation that encodes these behaviors. The intermediate representation is automatically transformed to the input language of mainstream model checkers, including PRISM, SPIN, and NuSMV allowing us to check different types of properties. We validate our approach on a model that contains key elements from the Air France Flight 447 accident and the Uberlingen accident.

Bio:
Dr. Neha Rungta is a Research Scientist at the NASA Ames Research Center located in California. Dr. Rungta’s research interests are in software model checking, verification of multi-agent systems for aviation safety, requirements analysis, and automated program analysis. In the past 10 years, Dr. Rungta’s work has been geared toward developing verification techniques for automated test case generation, detection of subtle concurrency errors, incremental program analysis, and verification of multi-agent systems. Dr. Rungta has published in several leading software engineering peer-reviewed conferences such as ICSE (International Conference on Software Engineering), ISSTA (International Symposium on Software Testing and Analysis), and ASE (International Conference on Automated Software Engineering), multi-agent system conferences such as AAMAS (International Conference on Autonomous Agents and Multi-agent Systems), as well as leading CS journals. She has chaired conferences such as the NASA Formal Methods (NFM) and the SPIN symposium on software model checking.