purplecat

Thank you very much for submitting a paper to CLIMA XIV. We are delighted to let
you know that your paper "Using Agent JPF to Build Models for Other Model Checkers" is accepted for presentation and inclusion in the Springer LNAI Proceedings.

Yay! That is my fifth paper acceptance this year which considering the publication deserts that were 2012 and 2011 is a welcome relief.

Agent JPF is a model checking tool for so called rational agent programming languages that I built on top of NASA's Java Pathfinder as part of the project before last. I've been tweaking it ever since and grappling slightly with the fact that, out of the box, JPF only checks there are no deadlocks or exceptions in a Java program where most model checkers have fairly sophisticated languages for describing properties based on temporal logics.

Hunter et al. recently published an interesting paper in which they used JPF to create a model of an agent program written in the Brahms language (which is a human-agent interaction modelling language used by NASA) but then shipped the model off to the Spin model checker for actual verification. I knew about this work in advance since they worked with my (very nearly almost graduated) PhD student and he brought one of the authors, Franco Raimondi up to Liverpool to give a talk, and then I picked his brains about how it all worked. At some point during the conversation I had one of those why didn't I think of this? moments because it is a very elegant and simple idea and I was within a hair's breadth of implementing it myself - I just hadn't realised the fact.

So I quickly adapted AJPF to do the same. Outputting models to Spin proved to be a doddle, but I was really interested in outputting stuff to a model checker called PRISM which can verify probabilistic properties - e.g., "if the aircraft's sensors are correct 90% of a time and the risk of an aircraft appearing on a collision course is 10% then the chance that the aircraft collides with another is less than 1%" because I really didn't want to implement algorithms for reasoning about probabilities over Java programs.

It was all implemented and written up in something of a rush, so I'm pleased it got accepted, though slightly alarmed by the fact that all the reviewers have commented on how well written the paper is. Maybe I should write more papers in a frantic hurry!