purplecat: Hand Drawn picture of a Toy Cat (Default)
purplecat ([personal profile] purplecat) wrote2013-06-25 03:57 pm

Paper Accepted: Using Agent JPF to Build Models for Other Model Checkers

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!
zorkian: Icon full of binary ones and zeros in no pattern. (Default)

[personal profile] zorkian 2013-06-28 12:12 am (UTC)(link)
I don't know half of what you were talking about, but I'm fascinated and excited that you wrote about it here! And congratulations on the paper acceptance!

When you say model checker for a Java program... is this in the vein of verifying correctness of a program, i.e., provably saying that it actually does X? Or is this more like, "this program models an airplane" and then "this checker verifies that the program models an airplane"? I've some experience with the idea of the former, and of course, the latter sounds somewhat close to the idea of unit testing (except at a more meta level?).
zorkian: Icon full of binary ones and zeros in no pattern. (Default)

[personal profile] zorkian 2013-07-08 09:18 pm (UTC)(link)

Thank you for the explanation!

That is pretty interesting, and a whole lot different from building consumer software. I spend a lot of my time thinking about reliability of systems, but usually at a higher level -- I assume that systems will fail, so I (try to) design architectures around those failures. What if I lose X or Y, what happens?

It sounds like you have to go a lot lower level and verify everything. (An endless task?) I suppose some of it gets rolled up -- i.e., you don't have to worry about, say, motor burnout specifically, but more just "there is a 0.01% cumulative chance of failure for every 1 hour of usage" and that includes physical wear and tear, unexpected failures, etc?

ladiesbingomod: Two women looking at each other (Default)

[personal profile] ladiesbingomod 2013-07-11 10:04 am (UTC)(link)
A lot of this, especially when it comes to the certification of unmanned aircraft, is about trying to assess the probability of a catastrophic failure assuming all mitigation mechanisms as failed - so they want to know that the chances of an unmanned aircraft dive-bombing a hospital are lower than some very small number.

And then yes, its a matter of working out how all the cumulative potential points of failure (with numbers obtained in various ways) combine together with the onboard software to give some overall (hopefully small) number.

[identity profile] wellinghall.livejournal.com 2013-06-25 03:44 pm (UTC)(link)
Well done! :-)

[identity profile] louisedennis.livejournal.com 2013-06-25 04:53 pm (UTC)(link)
Thanks!

[identity profile] the-marquis.livejournal.com 2013-06-25 08:38 pm (UTC)(link)
Well done on geting a paper into Climax IV

[identity profile] louisedennis.livejournal.com 2013-06-25 08:40 pm (UTC)(link)
It was funnier when I got a paper into CLIMA-X in 2009 *g* (Model Checking Normative Agent Organisations, in case you are interested)

[identity profile] the-marquis.livejournal.com 2013-06-25 08:57 pm (UTC)(link)
I can see that ;-) you must have quite a bibliography of your own by now.