« Lego RCX refercnes | Main | Guided model checking... by Edelkamp »
October 22, 2003
"Logic Verification of ANSI-C..." by Holzmann
[Logic Verification of ANSI C code with SPIN by Holzmann Mercer review]
An interesting approach to verifying C code using an abstraction in SPIN.
What is the problem being addressed?
reliable verification for software systems is a tough and elusive goal--especially for distributed software. Old-school things like code reviews, lab testing and peer reviews work better for sequential and deterministic things than they do for distributed systems. Logic verification of software in general is hard because most of the interesting verification problems are undecidable. Most automated efforts to do logic verification focus on carefully constructed and syntactically defined subsets. Programmers "shun" such efforts.
What approach is being taken to solve the problem?
Extract an abstract model of a piece of C code drop the abstract model into SPIN. The default abstraction should be "sufficient to make the verification problem tractable." For "reasonable constraints (e.g., given a memory arena of 64 MB and a runtime constraint of upto 10 minutes)" the probability of missing an error should be small.
more to come...
Posted by jones at October 22, 2003 08:53 AM
Comments
Post a comment
Thanks for signing in, . Now you can comment. (sign out)
(If you haven't left a comment here before, you may need to be approved by the site owner before your comment will appear. Until then, it won't appear on the entry. Thanks for waiting.)