Peter C. Mehlitz
My major interests are
My ongoing work is mainly about using software design to facilitate verification of highly reliable flight software (D4V and RHS), and to maintain and extend the Java PathFinder software model checker.
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.
Yes, that's the same me. I'm still a developer at heart, and I'm still into open source software (see JPF). I just combined it with my passion for space exploration. If you want to find out more, here is my personal resume.
|"Java PathFinder" (JPF) is my main project: 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.|