3 ms·

On lightweight formal methods, a favorite of mine that's not widely known is trace verification using Linear Temporal Logic [0]. Basically you just need to log

On lightweight formal methods, a favorite of mine that's not widely known is trace verification using Linear Temporal Logic [0]. Basically you just need to log events - which you can even have for free in event-driven architectures etc - and run some predicates on execution traces, e.g. "Always(Locked, Implies(Eventually(Unlocked)))", etc. One can run it on historical traces, but also couple it to stress tests, fuzzing etc to explore the state space. Quite simple, powerful and widely applicable, and doesn't require a model, just predicates. [0] https://en.m.wikipedia.org/wiki/Linear_temporal_logic https://en.m.wikipedia.org/wiki/Linear_temporal_logic

johnbender 2y ago
A minor point. This is more akin to testing because you’re only checking your formulae against a subset of system traces. Formal methods connotes comprehensive evidence about system behavior. In the case of TLA and similar system that’s a state machine and not the real system but the output for the state machine is a proof that your LTL/CTL/TLA properties hold for all behaviors of the system (traces or trees of traces).
- charleshn 2y ago
  Definitely, I'm playing fast and loose with "lightweight formal method here", thanks for making it clear. I was mentioning it in the same context as e.g. the Amazon paper on lightweight formal methods [0] where they use property-based testing to test that the implementation conforms to the model specification. In a similar spirit, linearizability checkers like Porcupine [1] are a nice mix of formalism and usability. I really like those because they are incredibly powerful, don't require a model and verify the actual implementation - obviously as you mention they are not exhaustive. [0] https://assets.amazon.science/77/5e/4a7c238f4ce890efdc325df83263/using-lightweight-formal-methods-to-validate-a-key-value-storage-node-in-amazon-s3-2.pdf https://assets.amazon.science/77/5e/4a7c238f4ce890efdc325df8... [1] https://github.com/anishathalye/porcupine https://github.com/anishathalye/porcupine

johnbender 2y ago

A minor point. This is more akin to testing because you’re only checking your formulae against a subset of system traces. Formal methods connotes comprehensive evidence about system behavior. In the case of TLA and similar system that’s a state machine and not the real system but the output for the state machine is a proof that your LTL/CTL/TLA properties hold for all behaviors of the system (traces or trees of traces).

charleshn 2y ago
Definitely, I'm playing fast and loose with "lightweight formal method here", thanks for making it clear. I was mentioning it in the same context as e.g. the Amazon paper on lightweight formal methods [0] where they use property-based testing to test that the implementation conforms to the model specification. In a similar spirit, linearizability checkers like Porcupine [1] are a nice mix of formalism and usability. I really like those because they are incredibly powerful, don't require a model and verify the actual implementation - obviously as you mention they are not exhaustive. [0] https://assets.amazon.science/77/5e/4a7c238f4ce890efdc325df83263/using-lightweight-formal-methods-to-validate-a-key-value-storage-node-in-amazon-s3-2.pdf https://assets.amazon.science/77/5e/4a7c238f4ce890efdc325df8... [1] https://github.com/anishathalye/porcupine https://github.com/anishathalye/porcupine