NASA Logo, National Aeronautics and Space Administration

Nastaran Shafiei, Ph.D.


I am a computer scientist in the Robust Software Engineering group at the NASA Ames Research Center, employed by String Ghaffarian Technologies. I am interested in verification of distributed systems applying model checking and runtime verification. My current focus includes developing a monitoring tool, called MESA, for analysis of message based systems against linear temporal logic specifications.

Projects

  • RACE - the Runtime for Airspace Concept Evaluation (RACE) is a framework to build highly distributed message based systems. RACE can be also used to create simulations running on several machines, connect to live data feeds, provide visualization via NASA’s WorldWind viewer, etc. RACE is an actor-based system which relies on the Akka framework.
  • JPF - Java Pathfinder (JPF) is an explicit-state model checker for Java bytecode. The core of JPF is a virtual machine (VM) that executes the system under test in all possible ways. As it drives the execution, it checks for properties, such as unhandled exceptions (including user-defined assertions) and deadlocks. The VM in JPF can be used to execute single-process multithreaded applications. I proposed and implemented an instance of the so-called centralization approach which allows the VM of JPF to execute multiple processes. This functionality is used to model check distributed multithreaded systems.
  • NAS - I have developed a tool for model checking Networked Asynchronous Systems (NAS), which allows for verifying distributed multithreaded Java applications. NAS is an extension of JPF, relies on the multiprocess support included in JPF, and models interprocess communication mechanisms. At this stage, it supports blocking operations on unbounded buffers. It uses a form of partial order reduction to reduce the state space of distributed applications, and provides a functionality to check the given distributed application under test against possible network failures which can occur at the operating system or the hardware layer.

Address: NASA Ames Research Center Mail Stop 269-1 Moffett Field, CA 94035 USA

Office: Bldg. 269, Rm. 235 Phone: (650) 604-

Email: nastaran.shafiei "at" nasa.gov

First Gov logo
NASA Logo - nasa.gov