In my day job, we have a medium-complicated system with many moving parts, and in particular many behaviors that are dependent on time elements (unreliable events, data coming in out of order, etc). It’s pretty hard to reason about.
What I would like to do is write a model of system behavior in Prolog, where I can define system boundaries and claim certain behaviors within those subsystems (which I then write tests for in our production system), then set out a handful of variables like “number of users between 0 and 200”, and “latency between 0 and 10 seconds” and “data receipt wait times between 5 minutes and 1 week”. Then define some failure modes, and ask Prolog to show me the exact combinations of variables that may lead to those failures.
I’m not sure where I got the idea that Prolog is appropriate for this sort of work, but I have faith that it is! I’m hoping there are libraries for this kind of thing, or maybe just papers on techniques to use. My problem is that I don’t really know what this sort of program verification is called, and my searching has only turned up using Prolog to verify source code, or compiler correctness, that sort of thing.
Maybe this is just a broad enough topic that there isn’t any particular technique, it’s just “go and write the program”. But if anyone knows what I’m talking about and can point the way to any further learning resources, I would be very grateful.
Perhaps I’m biased but this sounds like a constraint satisfaction problem to me. Define domains for your variables and then look for solutions corresponding to the “failure modes”. (As @brebs noted, this isn’t the same as a Prolog query failure.)
If your variables are integers look at library(clpfd); if reals, perhaps add-on pack clpBNR (disclaimer: I’m currently responsible for clpBNR so I’d be interested if it is a fit for your application).
Made available some time ago, pack Julian had would helped to build the linguistic model (here are the docs, just in case you want to keep reading…), but installing the pack triggers an error on post installation scripts - maybe not a fatal one.
In the end, since you got the attention of @ridgeworks, I suggest to keep on him.
Thanks to all of you for the responses! Having these search terms and links is invaluable, this is pointing me towards the right rabbit holes.
And yes, the definitions of “success” and “failure” will be reversed between the system and the model of the system! I will be trying very hard to make it fail.
So far, event calculus appears to be the most likely path. One of the more important failure modes will be “Under which circumstances could user X have access to resource Y at time T?” In which that’s not supposed to happen. So there’s a heavy time element to it, and my brief skimming of event calculus makes it look like it is specifically designed for that sort of thing.
Representing states using integers or reals isn’t out of the question, but would require some careful thinking about how best to represent states and conditions. This whole enterprise is going to be messy, in the same way that introducing unit testing to a codebase that wasn’t written with testing in mind is messy. I expect I’ll have to do quite a bit of adjusting of the system itself, in order to create clearer logical boundaries that map cleanly onto an abstracted model.
We’ll see how it goes! Thanks very much for these ideas and links.
What will also help those helping you and others is to click the heart at the bottom of each reply that is of value, this way it will get sorted up higher in searches, so others reading long post with lots of replies that this reply is worth reading and if it has enough likes will make it into the email for members that don’t visit the site but get only email summaries.
