SPINHow does Spin work?High Level OrganizationCommand Line ToolsXspinSimulatorComments1Carnegie Mellon University SPINFlavio LerdaBug Catching 15-398SPINAn explicit state model checker2Carnegie Mellon University SPINFlavio LerdaBug Catching 15-398How does Spin work?•We already saw:–The Algorithm–The Promela Language•We need to see how we does the tool work.3Carnegie Mellon University SPINFlavio LerdaBug Catching 15-398High Level OrganizationLTL TranslatorBuchi TranslatorPan VerifierC CompilerC GeneratorAutomataGeneratorPromela ParserLTL formula Promela ModelBuchi AutomatonAbstract Syntax TreeAutomataC CodeVerification ResultThe Buchi automaton isturned into a Promelaprocess and composedwith the rest of the system. The generated verifier isspecific to the model andproperty we started with.4Carnegie Mellon University SPINFlavio LerdaBug Catching 15-398Command Line Tools•Spin–Generates the Promela code for the LTL formula~$ spin –f “[]<>p”•The proposition in the formula must correspond to #defines–Generates the C source code~$ spin –a source.pro•The property must be included in the source•Pan–Performs the verification•Has many compile time options to enable different features•Optimized for performance5Carnegie Mellon University SPINFlavio LerdaBug Catching 15-398Xspin•GUI for Spin6Carnegie Mellon University SPINFlavio LerdaBug Catching 15-398Simulator•Spin can also be used as a simulator–Simulated the Promela program•It is used as a simulator when a counterexample is generated–Steps through the trace–The trace itself is not “readable”•Can be used for random and manually guided simulation as well7Carnegie Mellon University SPINFlavio LerdaBug Catching 15-398Comments•DFS does not necessarily find the shortest counterexample•There might be a very short counterexample but the verification might go out of memory•If we don’t finish we might still have some sort of a result (coverage
View Full Document
Unlocking...