Model checking Export

@inproceedings{conf/fsttsc97, abstract = {Model checking is an automatic technique for verifying finite-state reactive systems, such as sequential circuit designs and communication protocols. Specifications are expressed in temporal logic, and the reactive system is modeled as a statetransition graph. An efficient search procedure is used to determine whether or not the state-transition graph satisfies the specifications. We describe the basic model checking algorithm and show how it can be used with binary decision diagrams to verify properties of large state-transition graphs. We illustrate the power of model checking to find subtle errors by verifying part of the Contingency Guidance Requirements for the Space Shuttle.}, address = {Kharagpur, India}, author = {Clarke, Edmund}, booktitle = {Proceedings of the 17th Conference on Foundations of Software Technology and Theoretical Computer Science}, citeulike-article-id = {2924231}, citeulike-linkout-0 = {http://dx.doi.org/10.1007/BFb0058022}, citeulike-linkout-1 = {http://dx.doi.org/http://dx.doi.org/10.1007/BFb0058022}, citeulike-linkout-2 = {http://dx.doi.org/10.1007/BFb0058022}, doi = {10.1007/BFb0058022}, editor = {Ramesh, S. and Sivakumar, G.}, journal = {Foundations of Software Technology and Theoretical Computer Science}, keywords = {state-transition-graph, temporal-logic, verification}, pages = {54--56}, posted-at = {2008-09-25 09:31:47}, priority = {3}, title = {Model checking}, url = {http://dx.doi.org/10.1007/BFb0058022}, year = {1997} }

TY - CONF ID - conf/fsttsc97 L3 - citeulike-article-id:2924231 N2 - Model checking is an automatic technique for verifying finite-state reactive systems, such as sequential circuit designs and communication protocols. Specifications are expressed in temporal logic, and the reactive system is modeled as a statetransition graph. An efficient search procedure is used to determine whether or not the state-transition graph satisfies the specifications. We describe the basic model checking algorithm and show how it can be used with binary decision diagrams to verify properties of large state-transition graphs. We illustrate the power of model checking to find subtle errors by verifying part of the Contingency Guidance Requirements for the Space Shuttle. JF - Foundations of Software Technology and Theoretical Computer Science AD - Kharagpur, India EP - 56 TI - Model checking T2 - Proceedings of the 17th Conference on Foundations of Software Technology and Theoretical Computer Science SP - 54 KW - state-transition-graph KW - temporal-logic KW - verification AU - Clarke, Edmund A2 - Ramesh, S A2 - Sivakumar, G PY - 1997/// UR - http://dx.doi.org/10.1007/BFb0058022 ER -