This is another one of those posts devoted to misc. things which may be of interest to readers of this blog.
HVC
The Haifa Verification Conference 2015 is upon us (Nov 16-19). If you are in Israel at that time and have nothing better to do, here are some reasons you might want to come (in no particular order):
- You’ll be able to see me embarrass myself in front of a whole room of verification people, talking essentially about the stuff I discuss in this blog (the title is “Verification tribes, their habits and terminologies”). Also, if you do come and want to talk, just catch me there.
- My friend Kerstin Eder’s team will talk about “Coverage-Driven Verification – An approach to verify code for robots that directly interact with humans”. In other words, they actually report their experience of using CDV for verifying autonomous robots, and the results are interesting. Both our talks are Nov 17’th, BTW.
- HVC in general has a pretty good track record of being interdisciplinary, so I expect a whole bunch of other interesting verification presentations (though I don’t expect any of them to generate the same amount of excitement as the two mentioned above, especially now that Kerstin and myself have an agreement to laugh loudly at arbitrary points in each other’s presentations).
Game design languages
What is it: People who design video games have invented a bunch of languages for describing (“building”) the games. Some of those languages are pretty interesting (see below).
Why relevant for this blog: I have been thinking lately about good languages to describe scenarios, which have some leeway in them (i.e. “if X happens then you can do either Y or Z, except in winter, when you almost always do Z”). SVF certainly needs such a language, especially for describing behaviors at a high level (before you tie them down to coordinates, robot simulators and so on).
One potential place to look is the gaming industry: It is a huge industry, with a lot of idiosyncratic people and ideas (I say that as a form of praise).
Links:
One of the most interesting experiments in that world is Inform 7. It has a fairly-permissive, English-like language to describe scenes, scenarios, reactions and so on.
Quite a few interactive fiction games were written in it. Take a look at these (arbitrarily-chosen) two pages taken from the source code of a game called “Bronze”. Yes, this what the formatted source code actually looks like (double quotes mark literal strings, of course).
A newer, and pretty interesting, attempt is Ceptre. Here is the 37-minute video titled Ceptre – a language for modeling interactive worlds, and here is the paper (pdf).
Testing distributed systems with deterministic simulation
What is it: One of the problems in testing distributed systems is that they are generally not repeatable. The other big issue is that they are not controllable (i.e. you cannot easily force a network disconnect, or a disk crash, at exactly the point where your testing scenario calls for it). But some brave souls have created systems which solve both problems, via deterministic simulation of whole, multi-server setups.
Link: This 40-minute video (slides are here) describes how FoundationDB does just that. It is about a year old (FoundationDB has since been acquired by Apple), but it is well worth watching if you are into testing complex systems.
Why relevant for this blog: While testing multi-server systems is not directly one of the things SVF tries to do, the techniques and philosophy are pretty interesting and general.
In fact, I am surprised there are no startups already doing generic-deterministic-testing-infrastructure for multi-server systems (or perhaps there are, and I just don’t know about them). People have done partial things, e.g. with Simics and with Xen, but nothing like what this video is showing. With so many companies dealing with virtual machine infrastructure, multi-server configurations and so on, you would think this should happen.