Peter C. Mehlitz
Sr. Software Engineer
My main interests are
My current focus is on developing RACE, an open sourced, actor based framework that is written in Scala and can be used for a variety of simulation and verification purposes that require massively concurrent and distributed operation.
Prior to RACE, my work at NASA revolved around restructuring, maintaining and extending the JavaPathfinder software model checker, including a number of its extensions such as jpf-pathdroid (model checking Android byte code) and jpf-statechart (model checking state machine models).
Being a strong proponent of open source development, most people probably still know me from my work on PocketLinux, XGL/FGL, Kaffe (the first cleanroom Java implementation, of which only www.kaffe.org remains), and - even more distant - the BISS-AWT libraries and CThrough. I also gave a number of talks about design patterns, Java and Kaffe at the Software Summit, ALS, and a number of other conferences.
|The Runtime for Airspace Concept Evaluation (RACE) is a software architecture and framework to build configurable, highly concurrent and distributed message based systems. Among other things, RACE can be used to rapidly build simulations that span several machines (including synchronized displays), interface existing hardware simulators and other live data feeds, and incorporate sophisticated visualization components such as NASA’s WorldWind viewer. RACE is implemented as a distributed actor system built on top of the Akka framework, primarily uses Scala as programming language and runs within Java Virtual Machines. It is open sourced under Apache v2 license and available on https://github.com/NASARace/race|
|"Java PathFinder" (JPF) is an explicit state software model checker for Java bytecode. From an implementors point of view, JPF is mostly a state storing, backtrackable Java VirtualMachine (JVM), written in Java itself. I didn't start the project, nor am I the driving force behind its formal methods capabilities. Those accolades go to Willem Visser, Klaus Havelund , and numerous other people who worked on JPF in the past. My involvement is twofold: (1) I don't believe software model checking can scale in general, and therefore I focus on extension mechanisms that can be used to adapt JPF to the needs of particular applications and properties, and (2) I'm restructuring JPF so that it becomes more manageable and extensible (e.g. by means of Search- and VMListeners). Not to mention that a little bit of Java implementation knowledge from my past helps with JPF's VM and library abstractions. Since JPF is open sourced (hosted on Sourceforge), it's easy for everybody to get involved|
|"Radiation Hardened Software" (RHS) is currently dormant, but not dead. The idea is that we can - and have to - do a lot on the software side to protect against radiation induced probabilistic errors. Space is an electronically hostile environment, and the probability of defects due to radiation is as high as running into programming bugs. So far, this was mainly regarded as a hardware problem, mitigated with shielding (weight) and/or specialized, radiation hardened hardware (performance, power, size). That leaves much to be desired, especially the capability to react on demand on varying threat levels that depend on flight phase an solar activity. Part of this work will be creating a software simulation environment for injecting various single event effects into executable flight code, to see how it blows up.|
|"Design for Verification" (D4V) is in a way a basis for RHS. The main idea is that we cannot solely rely on tools to verify whatever software we throw at them. A defining quality of software is the potential number of different ways to implement the same functionality, and it is way too easy to break verification tools and methods by choosing an implementation that is unsuitable for a particular verification method - "design matters". D4V respects this by changing the traditional development process: the system is designed based on what later-on has to be verified. While there are a number of methods in D4V's repertoire, the usage of design patterns with property guarantees based on checkable usage rules stands out.|