Software Foundations
softwarefoundations.cis.upenn.edu
softwarefoundations.cis.upenn.edu
Two of those with lots of benefit in realistic projects are Alloy Analyzer (esp for structure) and TLA+/PlusCal (esp for order):
https://learntla.com/introduction/
These are immediately useful. Especially in distributed systems for TLA+. Then, you get a book such as Chlipala's Certified Programming with Dependent Types or Pierce et al's Software Foundations. Chlipala is also doing a new one called "Formal Reasoning About Programs." You can try to use those to get some elementary stuff done with the heavyweight methods. It will probably take you 1-2 years to get proficient enough for real stuff. Two outcomes are common:
1. You don't make it. Don't get mad: most don't even when they're smart. Good news is you enjoyed lighter stuff that you'll probably continue to apply and expand on for rest of your career. If other users are lucky, you might have run into their limitations enough to start improving the tooling, documentation, or something else. Those will get better since you learned them but avoided heavyweight stuff.
2. You made it! Now, best result for us IT folks is you apply your skills to real-world software formally-verifying useful algorithms, protocols, compilers, OS's, and so on. For inspiration, be sure to look at CRYPTOL, miTLS, CompCert, CakeML, RockSalt, seL4 or VAMOS, Verdi, verified garbage collectors, foundational backing of static analyzers like Verasco, tools with automation such as SPARK Ada, ACL2 for hardware, and maybe rewriting-based stuff like C semantics in K Framework.
If you can understand heavyweight verification, then apply your knowledge to more stuff like that since you'll (a) possibly be having real-world impact and (b) be doing work challenging enough that you can be very proud of your successes.
One problem with Alloy, for someone who wants to learn logic, is that it uses a completely different notation from ordinary mathematical notation. OTOH, TLA+ is probably the formal tool that uses the notation most similar to ordinary mathematical notation (more so than Coq, Lean, or Isabelle), and formal proofs (if you want to write them -- you don't have to), that are by far the most readable.
So assuming I could specify this system with Alloy, what would I learn? I'm guessing I would at least detect gaps in the protocols and missing error recovery arcs in state machines. But that doesn't yield a correct implementation... it might help me fill in gaps in the validation test coverage space. Is this what I should expect?
Some formal system technologies let you "extract" algorithms into other languages. Model checkers like Alloy don't. What you take away is what you learn and what you can use of that learning to convince others.
A good concrete takeaway would be information you could use to design a test suite that breaks the system even where others believe it to be solid.
In a past life, I worked on automatic test pattern generation for sequential logic circuits. Which, if you want to tilt at windmills for little $return (1), is as good a pursuit as any. But it strikes me that this is a very similar problem. Given a description of a state space, create stimulus that covers it, sensitizing all the logic paths in a way that produces an observable result that differs from expectations.
(1) The central lesson of trying to sell test: Electronic Design Automation dollars are like western US water law, the first to divert wins. In the case of EDA, the up-front design tools get all the dollars, and there is hardly a trickle of money left by the time it reaches test phase.
I’d emphasize that using Alloy/TLA is often an iterative process where you refine your model over time. In this way, it’s possibly faster to dig through several iterations in Alloy before identifying a counter-example to a property of interest.
But if you are mostly interested in finding interesting test sets then you should be able to stop once you’ve modeled your actual implementation well enough.
https://repositorio-aberto.up.pt/bitstream/10216/59949/1/000...
http://www.dcc.fc.up.pt/~rvr/resources/MAP-i/2014s7c-mapi.pd...
One application to hardware with Alloy:
http://www.samkirk.com/atpg-in-alloy4/ATPG_in_Alloy.pdf
Honestly, I'd have thought TLA+ would be better of the two for hardware given it deals with concurrent things. Also, it can do stuff similar to SPIN model-checker that was used extensively for hardware verification in the past. For hardware, I'd have experimented with SPIN for lightweight method with ACL2 for heavyweight esp thanks to Jared Davis at Centaur contributing ACL2 components he used.
http://spinroot.com/spin/whatispin.html
https://www.cs.utexas.edu/~jared/publications/2011-memocode-...
Just for kicks, I did some quick Googling on test generation for sequential circuits to see if I could find anything interesting for you. Me, too, as I enjoy seeing what people do in your field. Most were paywalled but this one wasn't:
Alloy will tell you where things are over or under-specified. You can ask the system to generate you scenarios in the "world" so you can see a graphical representation of states. You can test/check your assumptions or operating criteria against the structures/rules of the of the "world" and it'll find and show you counter-examples where things fail. I especially like working in Alloy because it's incremental and interactive, like a REPL for you design work, providing some of the benefits of property-based testing in the design portions of creating your system. Simply put: It helps you think through and explore your design!
https://lamport.azurewebsites.net/tla/tla.html
Both are very useful resources and for those interested in learning I would recommend going through both together letting the book fill in the detail where the hyperbook leaves you wanting more information. The hyperbook concetrates on PlusCal, which is a higher level interface to the TLA language, while the TLA book is all in the TLA language itself. I find,in practice,that the TLA language is what I am more comfortable writing specifications in. I find it clearer and as essentially standard mathematical notation its one less thing to learn. I believe Leslie encourages engineers to use PlusCal as being more user friendly.
Once one has worked though the specification course in the hyperbook, one should be able to apply TLA to real problems in any event driven system. (Sequential problems can also be modeled though). The primary hurdle in getting to applications will probably be coming to the understanding that modeling work happens at a much higher level of abstraction than programming, and that ones insticts as programmers, to get into detail, are not correct.
The benefits are two fold. Modeling a system before it's built forces one to abstract, clarify and simplify ones approach. The second benefit is that the model checker will find all the corner cases and complexity that one missed in the design. If one does a good translation from the model to code from there, then to a first approximation the code is bug free. As a bonus, later, when one goes back to code that has a spec, the spec is a nice summary of what has been coded (becase you forgot) and one can modify, and verify the spec before one updates the code.
I decided to learn Alloy inspired by the excellent OCW course by its author Prof. Daniel Jackson, "Elements of Software Construction" 2008 [1], where it is introduced in the very interesting OO lecture.
My plan is to learn some logic first though, specially relational logic, from Stanforfd's "Introduction to Logic" [2], which I am enjoying.
There is also an Alloy book, with many examples like OO design and state machine based messaging protocols.
[1] https://ocw.mit.edu/courses/electrical-engineering-and-compu...
For those who are looking for a softer introduction to the field, I highly recommend "Reactive Systems: Modelling, Specification and Verification" by Aceto, Ingólfsdóttir, Larsen, and Srba (full disclosure, I am a student at Aceto's current affiliation).