Model Checking with Abstract Types

Winter, Kirsten (2001). Model Checking with Abstract Types. In: M. W. Mislove, Scott D. Stoller and Willem Visser, Electronic Notes in Theoretical Computer Science: Workshop on Software Model Checking (in connection with CAV '01). 13th Conference on Computer Aided Verification, Paris, France, (382-393). July 18-23, 2001. doi:10.1016/S1571-0661(04)00264-6


Author Winter, Kirsten
Title of paper Model Checking with Abstract Types
Conference name 13th Conference on Computer Aided Verification
Conference location Paris, France
Conference dates July 18-23, 2001
Proceedings title Electronic Notes in Theoretical Computer Science: Workshop on Software Model Checking (in connection with CAV '01)   Check publisher's open access policy
Place of Publication Amsterdam ; New York
Publisher Elsevier Science
Publication Year 2001
Sub-type Fully published paper
DOI 10.1016/S1571-0661(04)00264-6
Open Access Status
ISSN 1571-0661
Editor M. W. Mislove
Scott D. Stoller
Willem Visser
Volume 55
Issue 3
Start page 382
End page 393
Total pages 12
Language eng
Abstract/Summary Model checking the design of a software system can be supported by providing an interface from a high-level modelling language, which is suitable for describing software design, to a given model checking tool. In order to cope with the higher complexity of software systems, we additionally need a means for reducing the system's state space. This can be done be applying abstraction to large or infinite data parts of the model. In our work, we introduce an interface from the high-level modelling language ASM to Multiway Decision Graphs (MDGs). Similar to OBDDs, MDGs are a data structure suitable for symbolic representation of transition systems, and their model checking. Since MDGs support the representation of abstract sorts and functions they can treat abstract models. We present a transformation algorithm from ASM to MDGs that automatically generates abstract models once the user has marked the data to be abstracted. We adapt the MDG model checking algorithms for the treatment of ASM models.
Subjects E1
080309 Software Engineering
080399 Computer Software not elsewhere classified
Q-Index Code E1

 
Versions
Version Filter Type
Citation counts: Scopus Citation Count Cited 3 times in Scopus Article | Citations
Google Scholar Search Google Scholar
Created: Wed, 22 Apr 2009, 01:28:50 EST by Maria Campbell on behalf of Library Corporate Services