Incremental Runtime Verification of Probabilistic Systems View Full Text


Ontology type: schema:Chapter      Open Access: True


Chapter Info

DATE

2013

AUTHORS

Vojtěch Forejt , Marta Kwiatkowska , David Parker , Hongyang Qu , Mateusz Ujma

ABSTRACT

Probabilistic verification techniques have been proposed for runtime analysis of adaptive software systems, with the verification results being used to steer the system so that it satisfies certain Quality-of-Service requirements. Since systems evolve over time, and verification results are required promptly, efficiency is an essential issue. To address this, we present incremental verification techniques, which exploit the results of previous analyses. We target systems modelled as Markov decision processes, developing incremental methods for constructing models from high-level system descriptions and for numerical solution using policy iteration based on strongly connected components. A prototype implementation, based on the PRISM model checker, demonstrates performance improvements on a range of case studies. More... »

PAGES

314-319

Identifiers

URI

http://scigraph.springernature.com/pub.10.1007/978-3-642-35632-2_30

DOI

http://dx.doi.org/10.1007/978-3-642-35632-2_30

DIMENSIONS

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


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": "Department of Computer Science, University of Oxford, Oxford, UK", 
          "id": "http://www.grid.ac/institutes/grid.4991.5", 
          "name": [
            "Department of Computer Science, University of Oxford, Oxford, UK"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Forejt", 
        "givenName": "Vojt\u011bch", 
        "id": "sg:person.012103627631.41", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.012103627631.41"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "Department of Computer Science, University of Oxford, Oxford, UK", 
          "id": "http://www.grid.ac/institutes/grid.4991.5", 
          "name": [
            "Department of Computer Science, University of Oxford, Oxford, UK"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Kwiatkowska", 
        "givenName": "Marta", 
        "id": "sg:person.011375012273.39", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011375012273.39"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "School of Computer Science, University of Birmingham, Birmingham, UK", 
          "id": "http://www.grid.ac/institutes/grid.6572.6", 
          "name": [
            "School of Computer Science, University of Birmingham, Birmingham, UK"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Parker", 
        "givenName": "David", 
        "id": "sg:person.014007552600.37", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.014007552600.37"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "Department of Computer Science, University of Oxford, Oxford, UK", 
          "id": "http://www.grid.ac/institutes/grid.4991.5", 
          "name": [
            "Department of Computer Science, University of Oxford, Oxford, UK"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Qu", 
        "givenName": "Hongyang", 
        "id": "sg:person.011574463543.04", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011574463543.04"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "Department of Computer Science, University of Oxford, Oxford, UK", 
          "id": "http://www.grid.ac/institutes/grid.4991.5", 
          "name": [
            "Department of Computer Science, University of Oxford, Oxford, UK"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Ujma", 
        "givenName": "Mateusz", 
        "id": "sg:person.011443107516.15", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011443107516.15"
        ], 
        "type": "Person"
      }
    ], 
    "datePublished": "2013", 
    "datePublishedReg": "2013-01-01", 
    "description": "Probabilistic verification techniques have been proposed for runtime analysis of adaptive software systems, with the verification results being used to steer the system so that it satisfies certain Quality-of-Service requirements. Since systems evolve over time, and verification results are required promptly, efficiency is an essential issue. To address this, we present incremental verification techniques, which exploit the results of previous analyses. We target systems modelled as Markov decision processes, developing incremental methods for constructing models from high-level system descriptions and for numerical solution using policy iteration based on strongly connected components. A prototype implementation, based on the PRISM model checker, demonstrates performance improvements on a range of case studies.", 
    "editor": [
      {
        "familyName": "Qadeer", 
        "givenName": "Shaz", 
        "type": "Person"
      }, 
      {
        "familyName": "Tasiran", 
        "givenName": "Serdar", 
        "type": "Person"
      }
    ], 
    "genre": "chapter", 
    "id": "sg:pub.10.1007/978-3-642-35632-2_30", 
    "inLanguage": "en", 
    "isAccessibleForFree": true, 
    "isPartOf": {
      "isbn": [
        "978-3-642-35631-5", 
        "978-3-642-35632-2"
      ], 
      "name": "Runtime Verification", 
      "type": "Book"
    }, 
    "keywords": [
      "verification techniques", 
      "high-level system descriptions", 
      "adaptive software systems", 
      "incremental verification technique", 
      "verification results", 
      "probabilistic verification techniques", 
      "PRISM model checker", 
      "software systems", 
      "runtime verification", 
      "Markov decision process", 
      "prototype implementation", 
      "model checker", 
      "service requirements", 
      "runtime analysis", 
      "probabilistic systems", 
      "system description", 
      "performance improvement", 
      "incremental method", 
      "policy iteration", 
      "certain quality", 
      "decision process", 
      "essential issue", 
      "checker", 
      "system", 
      "case study", 
      "verification", 
      "implementation", 
      "iteration", 
      "technique", 
      "requirements", 
      "issues", 
      "efficiency", 
      "quality", 
      "solution", 
      "results", 
      "method", 
      "description", 
      "model", 
      "improvement", 
      "process", 
      "time", 
      "components", 
      "analysis", 
      "numerical solution", 
      "previous analyses", 
      "range", 
      "study", 
      "Incremental Runtime Verification"
    ], 
    "name": "Incremental Runtime Verification of Probabilistic Systems", 
    "pagination": "314-319", 
    "productId": [
      {
        "name": "dimensions_id", 
        "type": "PropertyValue", 
        "value": [
          "pub.1038792421"
        ]
      }, 
      {
        "name": "doi", 
        "type": "PropertyValue", 
        "value": [
          "10.1007/978-3-642-35632-2_30"
        ]
      }
    ], 
    "publisher": {
      "name": "Springer Nature", 
      "type": "Organisation"
    }, 
    "sameAs": [
      "https://doi.org/10.1007/978-3-642-35632-2_30", 
      "https://app.dimensions.ai/details/publication/pub.1038792421"
    ], 
    "sdDataset": "chapters", 
    "sdDatePublished": "2021-12-01T20:07", 
    "sdLicense": "https://scigraph.springernature.com/explorer/license/", 
    "sdPublisher": {
      "name": "Springer Nature - SN SciGraph project", 
      "type": "Organization"
    }, 
    "sdSource": "s3://com-springernature-scigraph/baseset/20211201/entities/gbq_results/chapter/chapter_37.jsonl", 
    "type": "Chapter", 
    "url": "https://doi.org/10.1007/978-3-642-35632-2_30"
  }
]
 

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-35632-2_30'

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-35632-2_30'

Turtle is a human-readable linked data format.

curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/978-3-642-35632-2_30'

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-35632-2_30'


 

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

152 TRIPLES      23 PREDICATES      76 URIs      67 LITERALS      7 BLANK NODES

Subject Predicate Object
1 sg:pub.10.1007/978-3-642-35632-2_30 schema:about anzsrc-for:08
2 anzsrc-for:0801
3 anzsrc-for:0802
4 anzsrc-for:0803
5 schema:author N2ff04f9a77714ebdaa5b863eeef6fbef
6 schema:datePublished 2013
7 schema:datePublishedReg 2013-01-01
8 schema:description Probabilistic verification techniques have been proposed for runtime analysis of adaptive software systems, with the verification results being used to steer the system so that it satisfies certain Quality-of-Service requirements. Since systems evolve over time, and verification results are required promptly, efficiency is an essential issue. To address this, we present incremental verification techniques, which exploit the results of previous analyses. We target systems modelled as Markov decision processes, developing incremental methods for constructing models from high-level system descriptions and for numerical solution using policy iteration based on strongly connected components. A prototype implementation, based on the PRISM model checker, demonstrates performance improvements on a range of case studies.
9 schema:editor N45094dcb96d449f29dbb31243409e78e
10 schema:genre chapter
11 schema:inLanguage en
12 schema:isAccessibleForFree true
13 schema:isPartOf Na5cc65ec55df4af392e24e9a242e93ad
14 schema:keywords Incremental Runtime Verification
15 Markov decision process
16 PRISM model checker
17 adaptive software systems
18 analysis
19 case study
20 certain quality
21 checker
22 components
23 decision process
24 description
25 efficiency
26 essential issue
27 high-level system descriptions
28 implementation
29 improvement
30 incremental method
31 incremental verification technique
32 issues
33 iteration
34 method
35 model
36 model checker
37 numerical solution
38 performance improvement
39 policy iteration
40 previous analyses
41 probabilistic systems
42 probabilistic verification techniques
43 process
44 prototype implementation
45 quality
46 range
47 requirements
48 results
49 runtime analysis
50 runtime verification
51 service requirements
52 software systems
53 solution
54 study
55 system
56 system description
57 technique
58 time
59 verification
60 verification results
61 verification techniques
62 schema:name Incremental Runtime Verification of Probabilistic Systems
63 schema:pagination 314-319
64 schema:productId N8ba233bdf8b642da8356485de3dc9657
65 Nd74787c7fcc3426cb68aa48ed73efdb4
66 schema:publisher Ne066c478da8e455b81ee35cb9aa96647
67 schema:sameAs https://app.dimensions.ai/details/publication/pub.1038792421
68 https://doi.org/10.1007/978-3-642-35632-2_30
69 schema:sdDatePublished 2021-12-01T20:07
70 schema:sdLicense https://scigraph.springernature.com/explorer/license/
71 schema:sdPublisher N6ffdda960f7b46a7b66783aedce8fb52
72 schema:url https://doi.org/10.1007/978-3-642-35632-2_30
73 sgo:license sg:explorer/license/
74 sgo:sdDataset chapters
75 rdf:type schema:Chapter
76 N0ffc6a51deaa4e5ab6b9d5f4cb6859ec rdf:first sg:person.014007552600.37
77 rdf:rest Nf53de064a7e8410c9a2fa45badf4adbd
78 N2ff04f9a77714ebdaa5b863eeef6fbef rdf:first sg:person.012103627631.41
79 rdf:rest N3b094e0da231416ca4e5b0454e3e36b9
80 N3b094e0da231416ca4e5b0454e3e36b9 rdf:first sg:person.011375012273.39
81 rdf:rest N0ffc6a51deaa4e5ab6b9d5f4cb6859ec
82 N45094dcb96d449f29dbb31243409e78e rdf:first Nc9e0f6e1412b471fb2ac79ae62769185
83 rdf:rest Na12a02e9dbeb4dbfb5a647b17443f2a1
84 N6ffdda960f7b46a7b66783aedce8fb52 schema:name Springer Nature - SN SciGraph project
85 rdf:type schema:Organization
86 N8ba233bdf8b642da8356485de3dc9657 schema:name doi
87 schema:value 10.1007/978-3-642-35632-2_30
88 rdf:type schema:PropertyValue
89 Na12a02e9dbeb4dbfb5a647b17443f2a1 rdf:first Nef7d5f2d3ed64065987daf4ed839c38b
90 rdf:rest rdf:nil
91 Na5cc65ec55df4af392e24e9a242e93ad schema:isbn 978-3-642-35631-5
92 978-3-642-35632-2
93 schema:name Runtime Verification
94 rdf:type schema:Book
95 Nc9e0f6e1412b471fb2ac79ae62769185 schema:familyName Qadeer
96 schema:givenName Shaz
97 rdf:type schema:Person
98 Nd74787c7fcc3426cb68aa48ed73efdb4 schema:name dimensions_id
99 schema:value pub.1038792421
100 rdf:type schema:PropertyValue
101 Ne066c478da8e455b81ee35cb9aa96647 schema:name Springer Nature
102 rdf:type schema:Organisation
103 Nef7d5f2d3ed64065987daf4ed839c38b schema:familyName Tasiran
104 schema:givenName Serdar
105 rdf:type schema:Person
106 Nf53de064a7e8410c9a2fa45badf4adbd rdf:first sg:person.011574463543.04
107 rdf:rest Nfc3b190b558a4d34bcc41edcdeb54240
108 Nfc3b190b558a4d34bcc41edcdeb54240 rdf:first sg:person.011443107516.15
109 rdf:rest rdf:nil
110 anzsrc-for:08 schema:inDefinedTermSet anzsrc-for:
111 schema:name Information and Computing Sciences
112 rdf:type schema:DefinedTerm
113 anzsrc-for:0801 schema:inDefinedTermSet anzsrc-for:
114 schema:name Artificial Intelligence and Image Processing
115 rdf:type schema:DefinedTerm
116 anzsrc-for:0802 schema:inDefinedTermSet anzsrc-for:
117 schema:name Computation Theory and Mathematics
118 rdf:type schema:DefinedTerm
119 anzsrc-for:0803 schema:inDefinedTermSet anzsrc-for:
120 schema:name Computer Software
121 rdf:type schema:DefinedTerm
122 sg:person.011375012273.39 schema:affiliation grid-institutes:grid.4991.5
123 schema:familyName Kwiatkowska
124 schema:givenName Marta
125 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011375012273.39
126 rdf:type schema:Person
127 sg:person.011443107516.15 schema:affiliation grid-institutes:grid.4991.5
128 schema:familyName Ujma
129 schema:givenName Mateusz
130 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011443107516.15
131 rdf:type schema:Person
132 sg:person.011574463543.04 schema:affiliation grid-institutes:grid.4991.5
133 schema:familyName Qu
134 schema:givenName Hongyang
135 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011574463543.04
136 rdf:type schema:Person
137 sg:person.012103627631.41 schema:affiliation grid-institutes:grid.4991.5
138 schema:familyName Forejt
139 schema:givenName Vojtěch
140 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.012103627631.41
141 rdf:type schema:Person
142 sg:person.014007552600.37 schema:affiliation grid-institutes:grid.6572.6
143 schema:familyName Parker
144 schema:givenName David
145 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.014007552600.37
146 rdf:type schema:Person
147 grid-institutes:grid.4991.5 schema:alternateName Department of Computer Science, University of Oxford, Oxford, UK
148 schema:name Department of Computer Science, University of Oxford, Oxford, UK
149 rdf:type schema:Organization
150 grid-institutes:grid.6572.6 schema:alternateName School of Computer Science, University of Birmingham, Birmingham, UK
151 schema:name School of Computer Science, University of Birmingham, Birmingham, UK
152 rdf:type schema:Organization
 




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


...