Can Flash Memory Help in Model Checking? View Full Text


Ontology type: schema:Chapter     


Chapter Info

DATE

2009

AUTHORS

Jiří Barnat , Luboš Brim , Stefan Edelkamp , Damian Sulewski , Pavel Šimeček

ABSTRACT

As flash media become common and their capacities and speed grow, they are becoming a practical alternative for standard mechanical drives. So far, external memory model checking algorithms have been optimized for mechanical hard disks corresponding to the model of Aggarwal and Vitter [1]. Since flash memories are essentially different, the model of Aggarwal and Vitter no longer describes their typical behavior. On such a different device, algorithms can have different complexity, which may lead to the design of completely new flash-memory-efficient algorithms. We provide a model for computation of I/O complexity on the model of Aggarwal and Vitter modified for flash memories. We discuss verification algorithms optimized for this model and compare the performance of these algorithms with approaches known from I/O efficient model checking on mechanical hard disks. We also give an answer, when the usage of flash devices pays off and whether their further evolution in speed and capacity could broaden a range, where new algorithms outperform the old ones. More... »

PAGES

150-165

Book

TITLE

Formal Methods for Industrial Critical Systems

ISBN

978-3-642-03239-4
978-3-642-03240-0

Identifiers

URI

http://scigraph.springernature.com/pub.10.1007/978-3-642-03240-0_14

DOI

http://dx.doi.org/10.1007/978-3-642-03240-0_14

DIMENSIONS

https://app.dimensions.ai/details/publication/pub.1046717426


Indexing Status Check whether this publication has been indexed by Scopus and Web Of Science using the SN Indexing Status Tool
Incoming Citations Browse incoming citations for this publication using opencitations.net

JSON-LD is the canonical representation for SciGraph data.

TIP: You can open this SciGraph record using an external JSON-LD service: JSON-LD Playground Google SDTT

[
  {
    "@context": "https://springernature.github.io/scigraph/jsonld/sgcontext.json", 
    "about": [
      {
        "id": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/08", 
        "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
        "name": "Information and Computing Sciences", 
        "type": "DefinedTerm"
      }, 
      {
        "id": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/0802", 
        "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
        "name": "Computation Theory and Mathematics", 
        "type": "DefinedTerm"
      }
    ], 
    "author": [
      {
        "affiliation": {
          "alternateName": "Masaryk University Brno, Czech Republic", 
          "id": "http://www.grid.ac/institutes/grid.10267.32", 
          "name": [
            "Masaryk University Brno, Czech Republic"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Barnat", 
        "givenName": "Ji\u0159\u00ed", 
        "id": "sg:person.011367557177.46", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011367557177.46"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "Masaryk University Brno, Czech Republic", 
          "id": "http://www.grid.ac/institutes/grid.10267.32", 
          "name": [
            "Masaryk University Brno, Czech Republic"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Brim", 
        "givenName": "Lubo\u0161", 
        "id": "sg:person.0645117057.83", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.0645117057.83"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "Technische Universit\u00e4t Dortmund, Germany", 
          "id": "http://www.grid.ac/institutes/grid.5675.1", 
          "name": [
            "Technische Universit\u00e4t Dortmund, Germany"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Edelkamp", 
        "givenName": "Stefan", 
        "id": "sg:person.011300365431.45", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011300365431.45"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "Technische Universit\u00e4t Dortmund, Germany", 
          "id": "http://www.grid.ac/institutes/grid.5675.1", 
          "name": [
            "Technische Universit\u00e4t Dortmund, Germany"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Sulewski", 
        "givenName": "Damian", 
        "id": "sg:person.07751627652.24", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.07751627652.24"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "Masaryk University Brno, Czech Republic", 
          "id": "http://www.grid.ac/institutes/grid.10267.32", 
          "name": [
            "Masaryk University Brno, Czech Republic"
          ], 
          "type": "Organization"
        }, 
        "familyName": "\u0160ime\u010dek", 
        "givenName": "Pavel", 
        "id": "sg:person.016270033701.83", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.016270033701.83"
        ], 
        "type": "Person"
      }
    ], 
    "datePublished": "2009", 
    "datePublishedReg": "2009-01-01", 
    "description": "As flash media become common and their capacities and speed grow, they are becoming a practical alternative for standard mechanical drives. So far, external memory model checking algorithms have been optimized for mechanical hard disks corresponding to the model of Aggarwal and Vitter\u00a0[1]. Since flash memories are essentially different, the model of Aggarwal and Vitter no longer describes their typical behavior. On such a different device, algorithms can have different complexity, which may lead to the design of completely new flash-memory-efficient algorithms. We provide a model for computation of I/O complexity on the model of Aggarwal and Vitter modified for flash memories. We discuss verification algorithms optimized for this model and compare the performance of these algorithms with approaches known from I/O efficient model checking on mechanical hard disks. We also give an answer, when the usage of flash devices pays off and whether their further evolution in speed and capacity could broaden a range, where new algorithms outperform the old ones.", 
    "editor": [
      {
        "familyName": "Cofer", 
        "givenName": "Darren", 
        "type": "Person"
      }, 
      {
        "familyName": "Fantechi", 
        "givenName": "Alessandro", 
        "type": "Person"
      }
    ], 
    "genre": "chapter", 
    "id": "sg:pub.10.1007/978-3-642-03240-0_14", 
    "inLanguage": "en", 
    "isAccessibleForFree": false, 
    "isPartOf": {
      "isbn": [
        "978-3-642-03239-4", 
        "978-3-642-03240-0"
      ], 
      "name": "Formal Methods for Industrial Critical Systems", 
      "type": "Book"
    }, 
    "keywords": [
      "model of Aggarwal", 
      "mechanical hard disks", 
      "hard disk", 
      "external memory model", 
      "flash memory", 
      "verification algorithm", 
      "efficient algorithm", 
      "Vitter", 
      "memory model", 
      "new algorithm", 
      "algorithm", 
      "flash media", 
      "different devices", 
      "efficient model", 
      "flash devices", 
      "different complexity", 
      "Aggarwal", 
      "complexity", 
      "computation", 
      "memory", 
      "devices", 
      "speed", 
      "model", 
      "usage", 
      "practical alternative", 
      "further evolution", 
      "performance", 
      "typical behavior", 
      "design", 
      "help", 
      "mechanical drive", 
      "answers", 
      "older ones", 
      "drive", 
      "one", 
      "alternative", 
      "disk", 
      "capacity", 
      "behavior", 
      "evolution", 
      "medium", 
      "range", 
      "approach"
    ], 
    "name": "Can Flash Memory Help in Model Checking?", 
    "pagination": "150-165", 
    "productId": [
      {
        "name": "dimensions_id", 
        "type": "PropertyValue", 
        "value": [
          "pub.1046717426"
        ]
      }, 
      {
        "name": "doi", 
        "type": "PropertyValue", 
        "value": [
          "10.1007/978-3-642-03240-0_14"
        ]
      }
    ], 
    "publisher": {
      "name": "Springer Nature", 
      "type": "Organisation"
    }, 
    "sameAs": [
      "https://doi.org/10.1007/978-3-642-03240-0_14", 
      "https://app.dimensions.ai/details/publication/pub.1046717426"
    ], 
    "sdDataset": "chapters", 
    "sdDatePublished": "2022-05-20T07:49", 
    "sdLicense": "https://scigraph.springernature.com/explorer/license/", 
    "sdPublisher": {
      "name": "Springer Nature - SN SciGraph project", 
      "type": "Organization"
    }, 
    "sdSource": "s3://com-springernature-scigraph/baseset/20220519/entities/gbq_results/chapter/chapter_82.jsonl", 
    "type": "Chapter", 
    "url": "https://doi.org/10.1007/978-3-642-03240-0_14"
  }
]
 

Download the RDF metadata as:  json-ld nt turtle xml License info

HOW TO GET THIS DATA PROGRAMMATICALLY:

JSON-LD is a popular format for linked data which is fully compatible with JSON.

curl -H 'Accept: application/ld+json' 'https://scigraph.springernature.com/pub.10.1007/978-3-642-03240-0_14'

N-Triples is a line-based linked data format ideal for batch operations.

curl -H 'Accept: application/n-triples' 'https://scigraph.springernature.com/pub.10.1007/978-3-642-03240-0_14'

Turtle is a human-readable linked data format.

curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/978-3-642-03240-0_14'

RDF/XML is a standard XML format for linked data.

curl -H 'Accept: application/rdf+xml' 'https://scigraph.springernature.com/pub.10.1007/978-3-642-03240-0_14'


 

This table displays all metadata directly associated to this object as RDF triples.

139 TRIPLES      23 PREDICATES      69 URIs      62 LITERALS      7 BLANK NODES

Subject Predicate Object
1 sg:pub.10.1007/978-3-642-03240-0_14 schema:about anzsrc-for:08
2 anzsrc-for:0802
3 schema:author Na8fde09528d846fcb1b7f6fecf84c421
4 schema:datePublished 2009
5 schema:datePublishedReg 2009-01-01
6 schema:description As flash media become common and their capacities and speed grow, they are becoming a practical alternative for standard mechanical drives. So far, external memory model checking algorithms have been optimized for mechanical hard disks corresponding to the model of Aggarwal and Vitter [1]. Since flash memories are essentially different, the model of Aggarwal and Vitter no longer describes their typical behavior. On such a different device, algorithms can have different complexity, which may lead to the design of completely new flash-memory-efficient algorithms. We provide a model for computation of I/O complexity on the model of Aggarwal and Vitter modified for flash memories. We discuss verification algorithms optimized for this model and compare the performance of these algorithms with approaches known from I/O efficient model checking on mechanical hard disks. We also give an answer, when the usage of flash devices pays off and whether their further evolution in speed and capacity could broaden a range, where new algorithms outperform the old ones.
7 schema:editor Nbf8f33bb2c324e4da21624516ce8c100
8 schema:genre chapter
9 schema:inLanguage en
10 schema:isAccessibleForFree false
11 schema:isPartOf N94dfadba3adf41e28957a2f6ce7ff992
12 schema:keywords Aggarwal
13 Vitter
14 algorithm
15 alternative
16 answers
17 approach
18 behavior
19 capacity
20 complexity
21 computation
22 design
23 devices
24 different complexity
25 different devices
26 disk
27 drive
28 efficient algorithm
29 efficient model
30 evolution
31 external memory model
32 flash devices
33 flash media
34 flash memory
35 further evolution
36 hard disk
37 help
38 mechanical drive
39 mechanical hard disks
40 medium
41 memory
42 memory model
43 model
44 model of Aggarwal
45 new algorithm
46 older ones
47 one
48 performance
49 practical alternative
50 range
51 speed
52 typical behavior
53 usage
54 verification algorithm
55 schema:name Can Flash Memory Help in Model Checking?
56 schema:pagination 150-165
57 schema:productId N641c9704bf154db09933e00041f51214
58 N76a42a294f6b44a6a3295669a3241ff3
59 schema:publisher Ne945d58fb530431388a84c6e715c4add
60 schema:sameAs https://app.dimensions.ai/details/publication/pub.1046717426
61 https://doi.org/10.1007/978-3-642-03240-0_14
62 schema:sdDatePublished 2022-05-20T07:49
63 schema:sdLicense https://scigraph.springernature.com/explorer/license/
64 schema:sdPublisher N702d391b6db74acaabf1a5b7f0ac569f
65 schema:url https://doi.org/10.1007/978-3-642-03240-0_14
66 sgo:license sg:explorer/license/
67 sgo:sdDataset chapters
68 rdf:type schema:Chapter
69 N0a9e29abde2c40f6810158a9690bbe97 rdf:first sg:person.011300365431.45
70 rdf:rest N6bf6a1b6f4fc49cb90178bb9afb45948
71 N0d87497f1bd14b00b8d370acf4ecc72c schema:familyName Fantechi
72 schema:givenName Alessandro
73 rdf:type schema:Person
74 N24fa5f14b3fb415d9413a05ed8348d19 rdf:first sg:person.016270033701.83
75 rdf:rest rdf:nil
76 N2ef26f65e33c4065b0e727c6de58debe rdf:first N0d87497f1bd14b00b8d370acf4ecc72c
77 rdf:rest rdf:nil
78 N641c9704bf154db09933e00041f51214 schema:name doi
79 schema:value 10.1007/978-3-642-03240-0_14
80 rdf:type schema:PropertyValue
81 N6b6925be07f847d2992f3f0f24bf46ab rdf:first sg:person.0645117057.83
82 rdf:rest N0a9e29abde2c40f6810158a9690bbe97
83 N6bf6a1b6f4fc49cb90178bb9afb45948 rdf:first sg:person.07751627652.24
84 rdf:rest N24fa5f14b3fb415d9413a05ed8348d19
85 N702d391b6db74acaabf1a5b7f0ac569f schema:name Springer Nature - SN SciGraph project
86 rdf:type schema:Organization
87 N76a42a294f6b44a6a3295669a3241ff3 schema:name dimensions_id
88 schema:value pub.1046717426
89 rdf:type schema:PropertyValue
90 N94dfadba3adf41e28957a2f6ce7ff992 schema:isbn 978-3-642-03239-4
91 978-3-642-03240-0
92 schema:name Formal Methods for Industrial Critical Systems
93 rdf:type schema:Book
94 Na8fde09528d846fcb1b7f6fecf84c421 rdf:first sg:person.011367557177.46
95 rdf:rest N6b6925be07f847d2992f3f0f24bf46ab
96 Nbf8f33bb2c324e4da21624516ce8c100 rdf:first Nfe669094bba645e0b82cf4313a445e93
97 rdf:rest N2ef26f65e33c4065b0e727c6de58debe
98 Ne945d58fb530431388a84c6e715c4add schema:name Springer Nature
99 rdf:type schema:Organisation
100 Nfe669094bba645e0b82cf4313a445e93 schema:familyName Cofer
101 schema:givenName Darren
102 rdf:type schema:Person
103 anzsrc-for:08 schema:inDefinedTermSet anzsrc-for:
104 schema:name Information and Computing Sciences
105 rdf:type schema:DefinedTerm
106 anzsrc-for:0802 schema:inDefinedTermSet anzsrc-for:
107 schema:name Computation Theory and Mathematics
108 rdf:type schema:DefinedTerm
109 sg:person.011300365431.45 schema:affiliation grid-institutes:grid.5675.1
110 schema:familyName Edelkamp
111 schema:givenName Stefan
112 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011300365431.45
113 rdf:type schema:Person
114 sg:person.011367557177.46 schema:affiliation grid-institutes:grid.10267.32
115 schema:familyName Barnat
116 schema:givenName Jiří
117 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011367557177.46
118 rdf:type schema:Person
119 sg:person.016270033701.83 schema:affiliation grid-institutes:grid.10267.32
120 schema:familyName Šimeček
121 schema:givenName Pavel
122 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.016270033701.83
123 rdf:type schema:Person
124 sg:person.0645117057.83 schema:affiliation grid-institutes:grid.10267.32
125 schema:familyName Brim
126 schema:givenName Luboš
127 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.0645117057.83
128 rdf:type schema:Person
129 sg:person.07751627652.24 schema:affiliation grid-institutes:grid.5675.1
130 schema:familyName Sulewski
131 schema:givenName Damian
132 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.07751627652.24
133 rdf:type schema:Person
134 grid-institutes:grid.10267.32 schema:alternateName Masaryk University Brno, Czech Republic
135 schema:name Masaryk University Brno, Czech Republic
136 rdf:type schema:Organization
137 grid-institutes:grid.5675.1 schema:alternateName Technische Universität Dortmund, Germany
138 schema:name Technische Universität Dortmund, Germany
139 rdf:type schema:Organization
 




Preview window. Press ESC to close (or click here)


...