A practical advice: when specifying a large system, use modules and TLA+ support for module instantiation. Split the system into logical components, map each component to a TLA+ module. Create a test module for each component module. Instantiate a component module within a test module. Create a model and run it to test the instantiated component module.
This helps a lot with finding specification bugs early in the process.
At the very minimum test type invariants. Test modules do not need to be complicated, just something simple like shown below.
This helps a lot with finding specification bugs early in the process.
At the very minimum test type invariants. Test modules do not need to be complicated, just something simple like shown below.
No comments:
Post a Comment