From Model Checking to Runtime Verification and Back View Full Text


Ontology type: schema:Chapter      Open Access: True


Chapter Info

DATE

2017-09-06

AUTHORS

Katarína Kejstová , Petr Ročkai , Jiří Barnat

ABSTRACT

We describe a novel approach for adapting an existing software model checker to perform precise runtime verification. The software under test is allowed to communicate with the wider environment (including the file system and network). The modifications to the model checker are small and self-contained, making this a viable strategy for re-using existing model checking tools in a new context.Additionally, from the data that is gathered during a single execution in the runtime verification mode, we automatically re-construct a description of the execution environment which can then be used in the standard, full-blown model checker. This additional verification step can further improve coverage, especially in the case of parallel programs, without introducing substantial overhead into the process of runtime verification. More... »

PAGES

225-240

Identifiers

URI

http://scigraph.springernature.com/pub.10.1007/978-3-319-67531-2_14

DOI

http://dx.doi.org/10.1007/978-3-319-67531-2_14

DIMENSIONS

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


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/0801", 
        "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
        "name": "Artificial Intelligence and Image Processing", 
        "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"
      }, 
      {
        "id": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/0803", 
        "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
        "name": "Computer Software", 
        "type": "DefinedTerm"
      }
    ], 
    "author": [
      {
        "affiliation": {
          "alternateName": "Faculty of Informatics, Masaryk University, Brno, Czech Republic", 
          "id": "http://www.grid.ac/institutes/grid.10267.32", 
          "name": [
            "Faculty of Informatics, Masaryk University, Brno, Czech Republic"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Kejstov\u00e1", 
        "givenName": "Katar\u00edna", 
        "id": "sg:person.07560316405.30", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.07560316405.30"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "Faculty of Informatics, Masaryk University, Brno, Czech Republic", 
          "id": "http://www.grid.ac/institutes/grid.10267.32", 
          "name": [
            "Faculty of Informatics, Masaryk University, Brno, Czech Republic"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Ro\u010dkai", 
        "givenName": "Petr", 
        "id": "sg:person.07377571657.86", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.07377571657.86"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "Faculty of Informatics, Masaryk University, Brno, Czech Republic", 
          "id": "http://www.grid.ac/institutes/grid.10267.32", 
          "name": [
            "Faculty of Informatics, 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"
      }
    ], 
    "datePublished": "2017-09-06", 
    "datePublishedReg": "2017-09-06", 
    "description": "We describe a novel approach for adapting an existing software model checker to perform precise runtime verification. The software under test is allowed to communicate with the wider environment (including the file system and network). The modifications to the model checker are small and self-contained, making this a viable strategy for re-using existing model checking tools in a new context.Additionally, from the data that is gathered during a single execution in the runtime verification mode, we automatically re-construct a description of the execution environment which can then be used in the standard, full-blown model checker. This additional verification step can further improve coverage, especially in the case of parallel programs, without introducing substantial overhead into the process of runtime verification.", 
    "editor": [
      {
        "familyName": "Lahiri", 
        "givenName": "Shuvendu", 
        "type": "Person"
      }, 
      {
        "familyName": "Reger", 
        "givenName": "Giles", 
        "type": "Person"
      }
    ], 
    "genre": "chapter", 
    "id": "sg:pub.10.1007/978-3-319-67531-2_14", 
    "isAccessibleForFree": true, 
    "isPartOf": {
      "isbn": [
        "978-3-319-67530-5", 
        "978-3-319-67531-2"
      ], 
      "name": "Runtime Verification", 
      "type": "Book"
    }, 
    "keywords": [
      "runtime verification", 
      "model checker", 
      "software model checkers", 
      "additional verification step", 
      "execution environment", 
      "parallel programs", 
      "substantial overhead", 
      "verification mode", 
      "single execution", 
      "verification step", 
      "checker", 
      "novel approach", 
      "verification", 
      "overhead", 
      "execution", 
      "new context", 
      "environment", 
      "software", 
      "model", 
      "tool", 
      "wider environment", 
      "context", 
      "step", 
      "data", 
      "description", 
      "coverage", 
      "process", 
      "strategies", 
      "program", 
      "mode", 
      "cases", 
      "modification", 
      "viable strategy", 
      "test", 
      "approach"
    ], 
    "name": "From Model Checking to Runtime Verification and Back", 
    "pagination": "225-240", 
    "productId": [
      {
        "name": "dimensions_id", 
        "type": "PropertyValue", 
        "value": [
          "pub.1091543387"
        ]
      }, 
      {
        "name": "doi", 
        "type": "PropertyValue", 
        "value": [
          "10.1007/978-3-319-67531-2_14"
        ]
      }
    ], 
    "publisher": {
      "name": "Springer Nature", 
      "type": "Organisation"
    }, 
    "sameAs": [
      "https://doi.org/10.1007/978-3-319-67531-2_14", 
      "https://app.dimensions.ai/details/publication/pub.1091543387"
    ], 
    "sdDataset": "chapters", 
    "sdDatePublished": "2022-08-04T17:14", 
    "sdLicense": "https://scigraph.springernature.com/explorer/license/", 
    "sdPublisher": {
      "name": "Springer Nature - SN SciGraph project", 
      "type": "Organization"
    }, 
    "sdSource": "s3://com-springernature-scigraph/baseset/20220804/entities/gbq_results/chapter/chapter_132.jsonl", 
    "type": "Chapter", 
    "url": "https://doi.org/10.1007/978-3-319-67531-2_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-319-67531-2_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-319-67531-2_14'

Turtle is a human-readable linked data format.

curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/978-3-319-67531-2_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-319-67531-2_14'


 

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

121 TRIPLES      22 PREDICATES      61 URIs      52 LITERALS      7 BLANK NODES

Subject Predicate Object
1 sg:pub.10.1007/978-3-319-67531-2_14 schema:about anzsrc-for:08
2 anzsrc-for:0801
3 anzsrc-for:0802
4 anzsrc-for:0803
5 schema:author N3819dcc927c04e928c9908516c164ec3
6 schema:datePublished 2017-09-06
7 schema:datePublishedReg 2017-09-06
8 schema:description We describe a novel approach for adapting an existing software model checker to perform precise runtime verification. The software under test is allowed to communicate with the wider environment (including the file system and network). The modifications to the model checker are small and self-contained, making this a viable strategy for re-using existing model checking tools in a new context.Additionally, from the data that is gathered during a single execution in the runtime verification mode, we automatically re-construct a description of the execution environment which can then be used in the standard, full-blown model checker. This additional verification step can further improve coverage, especially in the case of parallel programs, without introducing substantial overhead into the process of runtime verification.
9 schema:editor N067f1848c04f4316a9baa4338d44284b
10 schema:genre chapter
11 schema:isAccessibleForFree true
12 schema:isPartOf Ncfb39dcdfdcf4aa1a68c3cba9af36a00
13 schema:keywords additional verification step
14 approach
15 cases
16 checker
17 context
18 coverage
19 data
20 description
21 environment
22 execution
23 execution environment
24 mode
25 model
26 model checker
27 modification
28 new context
29 novel approach
30 overhead
31 parallel programs
32 process
33 program
34 runtime verification
35 single execution
36 software
37 software model checkers
38 step
39 strategies
40 substantial overhead
41 test
42 tool
43 verification
44 verification mode
45 verification step
46 viable strategy
47 wider environment
48 schema:name From Model Checking to Runtime Verification and Back
49 schema:pagination 225-240
50 schema:productId N0eafa276170941f798b2f7676ea5930f
51 N9550ceb6149541e7878b1ee4247f2929
52 schema:publisher Na2f65916b5c447459e852b65d6a686e1
53 schema:sameAs https://app.dimensions.ai/details/publication/pub.1091543387
54 https://doi.org/10.1007/978-3-319-67531-2_14
55 schema:sdDatePublished 2022-08-04T17:14
56 schema:sdLicense https://scigraph.springernature.com/explorer/license/
57 schema:sdPublisher Nfe6d4e2141604000bd2de05d56a94a41
58 schema:url https://doi.org/10.1007/978-3-319-67531-2_14
59 sgo:license sg:explorer/license/
60 sgo:sdDataset chapters
61 rdf:type schema:Chapter
62 N067f1848c04f4316a9baa4338d44284b rdf:first Ne03b70aa34a2468288bac542b11d727a
63 rdf:rest N49ed02b0e49a4f22b4b47a42a1f05eea
64 N0eafa276170941f798b2f7676ea5930f schema:name dimensions_id
65 schema:value pub.1091543387
66 rdf:type schema:PropertyValue
67 N2a38e746eefd41638401a92a3f0c5ff7 rdf:first sg:person.011367557177.46
68 rdf:rest rdf:nil
69 N3819dcc927c04e928c9908516c164ec3 rdf:first sg:person.07560316405.30
70 rdf:rest Nd9ecd328ddde4ee89dac1140d5218904
71 N49ed02b0e49a4f22b4b47a42a1f05eea rdf:first Nf0ad6d447d6a4e33934527e893070ae9
72 rdf:rest rdf:nil
73 N9550ceb6149541e7878b1ee4247f2929 schema:name doi
74 schema:value 10.1007/978-3-319-67531-2_14
75 rdf:type schema:PropertyValue
76 Na2f65916b5c447459e852b65d6a686e1 schema:name Springer Nature
77 rdf:type schema:Organisation
78 Ncfb39dcdfdcf4aa1a68c3cba9af36a00 schema:isbn 978-3-319-67530-5
79 978-3-319-67531-2
80 schema:name Runtime Verification
81 rdf:type schema:Book
82 Nd9ecd328ddde4ee89dac1140d5218904 rdf:first sg:person.07377571657.86
83 rdf:rest N2a38e746eefd41638401a92a3f0c5ff7
84 Ne03b70aa34a2468288bac542b11d727a schema:familyName Lahiri
85 schema:givenName Shuvendu
86 rdf:type schema:Person
87 Nf0ad6d447d6a4e33934527e893070ae9 schema:familyName Reger
88 schema:givenName Giles
89 rdf:type schema:Person
90 Nfe6d4e2141604000bd2de05d56a94a41 schema:name Springer Nature - SN SciGraph project
91 rdf:type schema:Organization
92 anzsrc-for:08 schema:inDefinedTermSet anzsrc-for:
93 schema:name Information and Computing Sciences
94 rdf:type schema:DefinedTerm
95 anzsrc-for:0801 schema:inDefinedTermSet anzsrc-for:
96 schema:name Artificial Intelligence and Image Processing
97 rdf:type schema:DefinedTerm
98 anzsrc-for:0802 schema:inDefinedTermSet anzsrc-for:
99 schema:name Computation Theory and Mathematics
100 rdf:type schema:DefinedTerm
101 anzsrc-for:0803 schema:inDefinedTermSet anzsrc-for:
102 schema:name Computer Software
103 rdf:type schema:DefinedTerm
104 sg:person.011367557177.46 schema:affiliation grid-institutes:grid.10267.32
105 schema:familyName Barnat
106 schema:givenName Jiří
107 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011367557177.46
108 rdf:type schema:Person
109 sg:person.07377571657.86 schema:affiliation grid-institutes:grid.10267.32
110 schema:familyName Ročkai
111 schema:givenName Petr
112 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.07377571657.86
113 rdf:type schema:Person
114 sg:person.07560316405.30 schema:affiliation grid-institutes:grid.10267.32
115 schema:familyName Kejstová
116 schema:givenName Katarína
117 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.07560316405.30
118 rdf:type schema:Person
119 grid-institutes:grid.10267.32 schema:alternateName Faculty of Informatics, Masaryk University, Brno, Czech Republic
120 schema:name Faculty of Informatics, Masaryk University, Brno, Czech Republic
121 rdf:type schema:Organization
 




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


...