4 ms·

Does anyone know of any good resources for high-level guidelines on how to incorporate model checking into a typical software development flow? I've only used T

Does anyone know of any good resources for high-level guidelines on how to incorporate model checking into a typical software development flow? I've only used TLA+ in my own time for some fairly basic modeling of simplified service interactions at work. The team I'm on is soon inheriting a fairly complex codebase that is one of the core backend services at my company. At a high level, it is responsible for kicking off a "state machine" (which spans a few backend services) that ultimately updates a single "item", which is the smallest unit of data we care about. I'd be interested in spending a weekend or two with getting a rudimentary model of it up and running to aid in tech spec writing of new features and perhaps documenting possible bugs in the entire state machine flow. As it stands today, the state machine spans multiple services and is ill defined so I'll be diving into that for documentation purposes regardless, and it seems like creating a codified model simultaneously won't be too much overhead (at the very least, it could be fun).

nickpsecurity 9y ago
You can combine the model with property-based testing of that code to essentially try your model on the code and vice versa. You might also encode some of your expectations in there as preconditions, invariants, or postconditions that are checked at runtime during the tests. Throw a fuzzer like AFL at them. Hwayne has write-ups on both of those concepts: learntla.com https://hillelwayne.com/post/pbt-contracts/ https://hillelwayne.com/post/pbt-contracts/ Here's one on contracts that even your management might like: https://www.win.tue.nl/~wstomv/edu/2ip30/references/design-by-contract/index.html https://www.win.tue.nl/~wstomv/edu/2ip30/references/design-b...
- seattleeng 9y ago
  Property-based testing seems to be an interesting idea and fairly easy to trial and then recommend to my teammates. The js library I stumbled upon even has TypeScript support and plays nicely with mocha, both of which are directly relevant to my work (https://github.com/jsverify/jsverify https://github.com/jsverify/jsverify)!
ahelwer 9y ago
I wrote a finite model checker in C#, which I used to exhaustively check reads/writes against some complicated serialization code (serializing a bunch of different types into the blob, updating existing objects, ensuring values of all objects were as expected). Used during some tricky memory footprint reduction stuff inside Microsoft, I'll see whether I can open source it. Other than that, integrating TLA+ with your dev workflow is very straightforward if you're dealing with concurrency or distributed systems. In other domains its value is less obvious. You might also take a look at the P language, which will model-check your code if you add the right hooks.
- seattleeng 9y ago
  Yes, I suppose I'll try my naive TLA+ approach of modeling what I can as I document various parts of the system and see where it gets me. P looks like an interesting experiment to dabble in.

nickpsecurity 9y ago

You can combine the model with property-based testing of that code to essentially try your model on the code and vice versa. You might also encode some of your expectations in there as preconditions, invariants, or postconditions that are checked at runtime during the tests. Throw a fuzzer like AFL at them. Hwayne has write-ups on both of those concepts: learntla.com https://hillelwayne.com/post/pbt-contracts/ https://hillelwayne.com/post/pbt-contracts/ Here's one on contracts that even your management might like: https://www.win.tue.nl/~wstomv/edu/2ip30/references/design-by-contract/index.html https://www.win.tue.nl/~wstomv/edu/2ip30/references/design-b...

seattleeng 9y ago
Property-based testing seems to be an interesting idea and fairly easy to trial and then recommend to my teammates. The js library I stumbled upon even has TypeScript support and plays nicely with mocha, both of which are directly relevant to my work (https://github.com/jsverify/jsverify https://github.com/jsverify/jsverify)!

ahelwer 9y ago

I wrote a finite model checker in C#, which I used to exhaustively check reads/writes against some complicated serialization code (serializing a bunch of different types into the blob, updating existing objects, ensuring values of all objects were as expected). Used during some tricky memory footprint reduction stuff inside Microsoft, I'll see whether I can open source it. Other than that, integrating TLA+ with your dev workflow is very straightforward if you're dealing with concurrency or distributed systems. In other domains its value is less obvious. You might also take a look at the P language, which will model-check your code if you add the right hooks.

seattleeng 9y ago
Yes, I suppose I'll try my naive TLA+ approach of modeling what I can as I document various parts of the system and see where it gets me. P looks like an interesting experiment to dabble in.