In the software engineering program I took in CMU, one of the core courses is Models of Software Systems. This course was considered as one of the hard ones, because it taught students techniques available out there to “proof” the software to be correct or safe.
I won’t say the problem of proving software correctness is already solved, but one important part of the course is about using finite state machines and tools to proof the correctness of them. C or C++ statement sequence is hard for exhaustive simulation, but finite state machines are much easier to handle. There have been a lot researches on state machines.
Even without the tools, state machines are far more easier to trace and understand then code or flow chart, for anything nontrivial. Simply asking this question in design review would save you a lot of headache at debugging:
If something bad happened, how do I reset the state machine?
Many of our API documentations focus on describing the parameters and return values. They are important, but the mind set, the state machine behind the API, is at least equally important. API is not just a function, but also a protocol between the client and server. More often than not, we design and compose a larger system based on this protocol, instead of the detailed arguments. Design review should also first check the correctness of the protocol.
Academically, we can ask for many questions to a state machine, but some of them are simple enough to be listed here:
Safety: something (bad) will NEVER happen. You can specify this (set of) API shall never touch other part of the system.
Liveness: something good will EVENTUALLY happen. You shall never get stuck.
Deadlock: is it possible for multiple state machines get locked
Subscribe to:
Post Comments (Atom)
No comments:
Post a Comment