I’m new to formal methods, but I’m on fire for the notion, and benefits of “thinking above the code”. So far I have played with TLA+, only really used Alloy, and my impressions so far (still very new and ignorant) is that TLA+ is like the “expert mode” and that I could probably write a spec for just about anything with it, but it has a higher learning curve. Also, there seem to be many more learning resources available for TLA+ (probably just due to maturity I’m guessing). PlusCal looks like an amazingly helpful tool to help a noob like me ease into this.
Alloy’s approachable syntax and the model explorer seem absolutely awesome! Some parts of the Alloy docs I’ve been rereading because I’m so new to this higher level of abstraction. The temporal logic seems to make sense to me pretty quickly, it’s the relational logic that confused me a little bit at first. I really like Alloy a lot. (Please forgive me if I’m misusing some of this new vocabulary)
I’m curious, does anyone here have any experience with P? It seems interesting the whole idea of representing your system as communicating state machines.
In any case, I just took a new job working for a utility provider. I work with a bunch of Electrical Engineers and Power Systems Engineers so luckily, they are pretty supportive when it comes to improving quality, verifiability, and modeling. I’m extremely confident that Alloy 6 and/or TLA+ would be extremely helpful to our team. I’m very new to power systems as well, and we’re trying to make the power grid “smarter” by having the various devices involved in a microgrid send data about the system/circuit state through message broker and our Rust code subscribes to the topics, and then uses a genetic algorithm to “solve” the circuit for VVO/CVR (Variable Voltage Optimization/Conservation Voltage Reduction), and issues commands to the hardware to adjust the voltage to ensure we stay within the allotted range and don’t fry people’s stuff.
Given that this is a set of complex systems with a lot of concurrent behavior, extremely expensive equipment, and operators could get hurt or people could lose power, I’ve been shocked at the lack of documentation and tests of the code base my little team is inheriting.
This is an excellent example of verifiable correctness being kinda important, so I was pretty surprised when I asked around and the other software folk were not only unaware of formal methods, but were confused and almost hostile at the idea (perhaps I did not communicate effectively).
It has taken so long for my team to gain background context on the problem domain and to become familiar with the massive and complex code base we’ve inherited.
It never ceases to amaze me how ubiquitous it is in the industry to just cut corners (little/no or low quality tests, low/no diversity of testing strategies, poor/non-existent documentation, etc.). Many business just want to get to market first, and say they value quality, but any suggested practices/processes to improve quality/verifiability are met with impatience or annoyance.
Side Note: the previous team of contractors (and original authors of the code base) are being let go because they blew up a battery/capacitor bank that probably cost a couple years of my salary.
TLDR;
I’ve been hungry to learn some new tactics and tools to help the software teams I work on level up the quality of our deliverables and I think Alloy 6 and/or TLA+ is exactly what I’ve been looking for. I’ve got some minimal buy-in and I’m going to create a specification for our test grid, the devices on it, and ideally the voltage optimization algorithm and get the SMEs to help me ensure it’s correct and demonstrate to the software teams the power and benefits of this practice!