Yes SPIN is in general a very good idea, but as Andrew did I don't want to write the modle directly in Promela, because that would mean change it every time I change the code..
If I find a good representation for the network protocol that can also "export" for SPIN that great, I could use it, otherwise some really good unit/integration tests might be enough... Anyway to explain the situation a bit better: - at the moment the program will run on one machine only, and think I can not care about malicious actors, if it will ever be reachable by other machines in the network I'll see what to do.. - the speed and the data transferred will be really not that much, because the results are still written on the file systems and on a MySQL database. Maybe in the future we can avoid some of these writes if we are able to make all the programs that need the database communicate correctly, but at the moment the messages contain mainly control actions. So for now even a simple text protocol (maybe using JSON) is perfectly fine. 2012/8/18 Cem Karan <[email protected]>: > I agree with Brian that using a serialization library is a good idea, but > they'll only verify that the archived byte string can be deserialized > correctly. To verify that your system won't get into a wedged state, you'll > need to use something stronger, such as spin (thank you for mentioning it > Andrew!). > > Also, how concerned are you with malicious actors? Guarding against random > corruption is pretty easy, but if you know that there will be malicious > actors on your network, then you really DO need something that can verify > your model, AND you need to spend some time designing a real threat model. > That is, what capabilities will the malicious actors have? Can they only > corrupt packets, or can they see the state of the entire network, and > inject/destroy packets at will? Is there more than one attacker? Do they > have an unlimited amount of power/energy, or do they have to make choices > about when/where they attack? > > Finally, I'm going to mention MessagePack (http://msgpack.org/) and Google > Protocol Buffers (https://developers.google.com/protocol-buffers/) as > alternatives to JSON. They are only serialization libraries, but I've > noticed that MessagePack + blosc (http://blosc.pytables.org/trac) make for a > fairly powerful way of serializing & compressing data. I won't post any > numbers on transmission rates because the rest of my code is sufficiently > horrible that it will skew the results, but even with HIGHLY non-optimal > code, I'm pleased with the speeds/compression ratios I'm getting. > > Thanks, > Cem Karan > _______________________________________________ zeromq-dev mailing list [email protected] http://lists.zeromq.org/mailman/listinfo/zeromq-dev
