mdh.sePublications
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Automated Verification of Completeness and Consistency of Abstract State Machine Specifications using a SAT Solver
Massachusetts Institute of Technology, United States .
Massachusetts Institute of Technology, United States .ORCID iD: 0000-0003-0904-3712
2007 (English)In: Electronical Notes in Theoretical Computer Science, ISSN 1571-0661, E-ISSN 1571-0661, Vol. 190, no 2, p. 85-97Article in journal (Refereed) Published
Abstract [en]

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 consistencyof 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.

Place, publisher, year, edition, pages
2007. Vol. 190, no 2, p. 85-97
National Category
Computer Systems
Identifiers
URN: urn:nbn:se:mdh:diva-7139DOI: 10.1016/j.entcs.2007.08.008Scopus ID: 2-s2.0-34548168337OAI: oai:DiVA.org:mdh-7139DiVA, id: diva2:237149
Conference
3rd International Workshop on Model-Based Testing (MBT '07), Satellite Workshop of ETAPS 2007, Electronic Notes in Theoretical Computer Science (ENTCS)
Available from: 2009-09-25 Created: 2009-09-25 Last updated: 2017-12-13Bibliographically approved

Open Access in DiVA

No full text in DiVA

Other links

Publisher's full textScopus

Authority records BETA

Lundqvist, Kristina

Search in DiVA

By author/editor
Lundqvist, Kristina
In the same journal
Electronical Notes in Theoretical Computer Science
Computer Systems

Search outside of DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetric score

doi
urn-nbn
Total: 26 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf