%0 Journal Article %1 ouimet_07_automated %A Ouimet, Martin %A Lundqvist, Kristina %B Proceedings of the Third Workshop on Model Based Testing (MBT 2007) %D 2007 %J Electronic Notes in Theoretical Computer Science %K completeness 2007 sat consistency \_pdf asm %N 2 %P 85--97 %R http://dx.doi.org/10.1016/j.entcs.2007.08.008 %T Automated Verification of Completeness and Consistency of Abstract State Machine Specifications using a SAT Solver %U http://dx.doi.org/10.1016/j.entcs.2007.08.008 %V 190 %X In the requirements engineering community, consistency and completeness have been identified as important properties of system specifications. Custom algorithms to verify these properties automatically have been devised for a number of specification languages, including SCR, RSML, and Statecharts. In this paper, we provide means to automatically verify completeness and consistency of Abstract State Machine (ASM) specifications. The verification is performed using a widely available tool, a SAT solver. The use of a SAT solver removes the need for designing and fine tuning language specific verification algorithms. Furthermore, the use of a SAT solver automates the verification procedure and produces a counterexample automatically when a specification is incomplete or inconsistent. We provide an algorithm to translate ASM specifications to a SAT problem instance. The translation is illustrated using the TASM toolset in conjunction with the "production cell system" case study.

@article{ouimet_07_automated, abstract = {In the requirements engineering community, consistency and completeness have been identified as important properties of system specifications. Custom algorithms to verify these properties automatically have been devised for a number of specification languages, including SCR, RSML, and Statecharts. In this paper, we provide means to automatically verify completeness and consistency of Abstract State Machine (ASM) specifications. The verification is performed using a widely available tool, a SAT solver. The use of a SAT solver removes the need for designing and fine tuning language specific verification algorithms. Furthermore, the use of a SAT solver automates the verification procedure and produces a counterexample automatically when a specification is incomplete or inconsistent. We provide an algorithm to translate ASM specifications to a SAT problem instance. The translation is illustrated using the TASM toolset in conjunction with the "production cell system" case study.}, added-at = {2009-03-10T04:37:38.000+0100}, author = {Ouimet, Martin and Lundqvist, Kristina}, biburl = {https://www.bibsonomy.org/bibtex/2a0d13a2311f32302a71c5a75797b2a45/leonardo}, booktitle = {Proceedings of the Third Workshop on Model Based Testing (MBT 2007)}, citeulike-article-id = {1803529}, doi = {http://dx.doi.org/10.1016/j.entcs.2007.08.008}, interhash = {9e8dc6a946c59f10b73c71897a973ccb}, intrahash = {a0d13a2311f32302a71c5a75797b2a45}, journal = {Electronic Notes in Theoretical Computer Science}, keywords = {completeness 2007 sat consistency \_pdf asm}, month = {August}, number = 2, pages = {85--97}, posted-at = {2007-10-22 02:43:20}, priority = {4}, timestamp = {2009-03-10T04:37:38.000+0100}, title = {Automated Verification of Completeness and Consistency of Abstract State Machine Specifications using a SAT Solver}, url = {http://dx.doi.org/10.1016/j.entcs.2007.08.008}, volume = 190, year = 2007 }