A Framework for Verification of Software with Time and Probabilities View Full Text


Ontology type: schema:Chapter      Open Access: True


Chapter Info

DATE

2010

AUTHORS

Marta Kwiatkowska , Gethin Norman , David Parker

ABSTRACT

Quantitative verification techniques are able to establish system properties such as “the probability of an airbag failing to deploy on demand” or “the expected time for a network protocol to successfully send a message packet”. In this paper, we describe a framework for quantitative verification of software that exhibits both real-time and probabilistic behaviour. The complexity of real software, combined with the need to capture precise timing information, necessitates the use of abstraction techniques. We outline a quantitative abstraction refinement approach, which can be used to automatically construct and analyse abstractions of probabilistic, real-time programs. As a concrete example of the potential applicability of our framework, we discuss the challenges involved in applying it to the quantitative verification of SystemC, an increasingly popular system-level modelling language. More... »

PAGES

25-45

Identifiers

URI

http://scigraph.springernature.com/pub.10.1007/978-3-642-15297-9_4

DOI

http://dx.doi.org/10.1007/978-3-642-15297-9_4

DIMENSIONS

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


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": "Oxford University Computing Laboratory, Parks Road, OX1 3QD, Oxford, UK", 
          "id": "http://www.grid.ac/institutes/grid.4991.5", 
          "name": [
            "Oxford University Computing Laboratory, Parks Road, OX1 3QD, 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": "Department of Computing Science, University of Glasgow, G12 8RZ, Glasgow, UK", 
          "id": "http://www.grid.ac/institutes/grid.8756.c", 
          "name": [
            "Department of Computing Science, University of Glasgow, G12 8RZ, Glasgow, UK"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Norman", 
        "givenName": "Gethin", 
        "id": "sg:person.016323171577.36", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.016323171577.36"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "Oxford University Computing Laboratory, Parks Road, OX1 3QD, Oxford, UK", 
          "id": "http://www.grid.ac/institutes/grid.4991.5", 
          "name": [
            "Oxford University Computing Laboratory, Parks Road, OX1 3QD, Oxford, 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"
      }
    ], 
    "datePublished": "2010", 
    "datePublishedReg": "2010-01-01", 
    "description": "Quantitative verification techniques are able to establish system properties such as \u201cthe probability of an airbag failing to deploy on demand\u201d or \u201cthe expected time for a network protocol to successfully send a message packet\u201d. In this paper, we describe a framework for quantitative verification of software that exhibits both real-time and probabilistic behaviour. The complexity of real software, combined with the need to capture precise timing information, necessitates the use of abstraction techniques. We outline a quantitative abstraction refinement approach, which can be used to automatically construct and analyse abstractions of probabilistic, real-time programs. As a concrete example of the potential applicability of our framework, we discuss the challenges involved in applying it to the quantitative verification of SystemC, an increasingly popular system-level modelling language.", 
    "editor": [
      {
        "familyName": "Chatterjee", 
        "givenName": "Krishnendu", 
        "type": "Person"
      }, 
      {
        "familyName": "Henzinger", 
        "givenName": "Thomas A.", 
        "type": "Person"
      }
    ], 
    "genre": "chapter", 
    "id": "sg:pub.10.1007/978-3-642-15297-9_4", 
    "inLanguage": "en", 
    "isAccessibleForFree": true, 
    "isPartOf": {
      "isbn": [
        "978-3-642-15296-2", 
        "978-3-642-15297-9"
      ], 
      "name": "Formal Modeling and Analysis of Timed Systems", 
      "type": "Book"
    }, 
    "keywords": [
      "system-level modelling language", 
      "verification of software", 
      "quantitative verification techniques", 
      "real-time programs", 
      "abstraction refinement approach", 
      "quantitative verification", 
      "real software", 
      "modelling language", 
      "network protocols", 
      "verification techniques", 
      "abstraction techniques", 
      "message packets", 
      "precise timing information", 
      "refinement approach", 
      "software", 
      "timing information", 
      "probabilistic behavior", 
      "verification", 
      "system properties", 
      "framework", 
      "concrete examples", 
      "SystemC", 
      "packets", 
      "abstraction", 
      "complexity", 
      "language", 
      "technique", 
      "information", 
      "protocol", 
      "challenges", 
      "probability", 
      "potential applicability", 
      "applicability", 
      "demand", 
      "time", 
      "example", 
      "need", 
      "airbag", 
      "program", 
      "use", 
      "behavior", 
      "properties", 
      "paper", 
      "approach"
    ], 
    "name": "A Framework for Verification of Software with Time and Probabilities", 
    "pagination": "25-45", 
    "productId": [
      {
        "name": "dimensions_id", 
        "type": "PropertyValue", 
        "value": [
          "pub.1011541532"
        ]
      }, 
      {
        "name": "doi", 
        "type": "PropertyValue", 
        "value": [
          "10.1007/978-3-642-15297-9_4"
        ]
      }
    ], 
    "publisher": {
      "name": "Springer Nature", 
      "type": "Organisation"
    }, 
    "sameAs": [
      "https://doi.org/10.1007/978-3-642-15297-9_4", 
      "https://app.dimensions.ai/details/publication/pub.1011541532"
    ], 
    "sdDataset": "chapters", 
    "sdDatePublished": "2022-05-10T10:45", 
    "sdLicense": "https://scigraph.springernature.com/explorer/license/", 
    "sdPublisher": {
      "name": "Springer Nature - SN SciGraph project", 
      "type": "Organization"
    }, 
    "sdSource": "s3://com-springernature-scigraph/baseset/20220509/entities/gbq_results/chapter/chapter_28.jsonl", 
    "type": "Chapter", 
    "url": "https://doi.org/10.1007/978-3-642-15297-9_4"
  }
]
 

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-15297-9_4'

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-15297-9_4'

Turtle is a human-readable linked data format.

curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/978-3-642-15297-9_4'

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-15297-9_4'


 

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

134 TRIPLES      23 PREDICATES      72 URIs      63 LITERALS      7 BLANK NODES

Subject Predicate Object
1 sg:pub.10.1007/978-3-642-15297-9_4 schema:about anzsrc-for:08
2 anzsrc-for:0801
3 anzsrc-for:0802
4 anzsrc-for:0803
5 schema:author Ne324eec1aa7a4dc59bda14cf30b32363
6 schema:datePublished 2010
7 schema:datePublishedReg 2010-01-01
8 schema:description Quantitative verification techniques are able to establish system properties such as “the probability of an airbag failing to deploy on demand” or “the expected time for a network protocol to successfully send a message packet”. In this paper, we describe a framework for quantitative verification of software that exhibits both real-time and probabilistic behaviour. The complexity of real software, combined with the need to capture precise timing information, necessitates the use of abstraction techniques. We outline a quantitative abstraction refinement approach, which can be used to automatically construct and analyse abstractions of probabilistic, real-time programs. As a concrete example of the potential applicability of our framework, we discuss the challenges involved in applying it to the quantitative verification of SystemC, an increasingly popular system-level modelling language.
9 schema:editor N5eb2e7abd4da4795b6c5b0da5a35c03a
10 schema:genre chapter
11 schema:inLanguage en
12 schema:isAccessibleForFree true
13 schema:isPartOf N4b0c72a0d8aa4e35bc7cd97f7c1a0f19
14 schema:keywords SystemC
15 abstraction
16 abstraction refinement approach
17 abstraction techniques
18 airbag
19 applicability
20 approach
21 behavior
22 challenges
23 complexity
24 concrete examples
25 demand
26 example
27 framework
28 information
29 language
30 message packets
31 modelling language
32 need
33 network protocols
34 packets
35 paper
36 potential applicability
37 precise timing information
38 probabilistic behavior
39 probability
40 program
41 properties
42 protocol
43 quantitative verification
44 quantitative verification techniques
45 real software
46 real-time programs
47 refinement approach
48 software
49 system properties
50 system-level modelling language
51 technique
52 time
53 timing information
54 use
55 verification
56 verification of software
57 verification techniques
58 schema:name A Framework for Verification of Software with Time and Probabilities
59 schema:pagination 25-45
60 schema:productId N409cdb11a73d4a18b33b26df12ce2404
61 N4a040da5b246420bbfa58b338539ee4e
62 schema:publisher Nd02a89eb86fc42248f794ab3e527372f
63 schema:sameAs https://app.dimensions.ai/details/publication/pub.1011541532
64 https://doi.org/10.1007/978-3-642-15297-9_4
65 schema:sdDatePublished 2022-05-10T10:45
66 schema:sdLicense https://scigraph.springernature.com/explorer/license/
67 schema:sdPublisher Nfcbe9fd8f8ae4e548c548420c8d967fb
68 schema:url https://doi.org/10.1007/978-3-642-15297-9_4
69 sgo:license sg:explorer/license/
70 sgo:sdDataset chapters
71 rdf:type schema:Chapter
72 N409cdb11a73d4a18b33b26df12ce2404 schema:name dimensions_id
73 schema:value pub.1011541532
74 rdf:type schema:PropertyValue
75 N4a040da5b246420bbfa58b338539ee4e schema:name doi
76 schema:value 10.1007/978-3-642-15297-9_4
77 rdf:type schema:PropertyValue
78 N4b0c72a0d8aa4e35bc7cd97f7c1a0f19 schema:isbn 978-3-642-15296-2
79 978-3-642-15297-9
80 schema:name Formal Modeling and Analysis of Timed Systems
81 rdf:type schema:Book
82 N5eb2e7abd4da4795b6c5b0da5a35c03a rdf:first N923e2f5e140246f5858dc217e4b3bc07
83 rdf:rest Needd49d4c65d466a9b31dbe687a1ca19
84 N6444cf615c4541dc91d16f2f8f7fd1ad schema:familyName Henzinger
85 schema:givenName Thomas A.
86 rdf:type schema:Person
87 N8e205fecfb41434fbb0f1a7cdc9b26ad rdf:first sg:person.016323171577.36
88 rdf:rest Ne31fb953da814b06a162a1c17e112f6d
89 N923e2f5e140246f5858dc217e4b3bc07 schema:familyName Chatterjee
90 schema:givenName Krishnendu
91 rdf:type schema:Person
92 Nd02a89eb86fc42248f794ab3e527372f schema:name Springer Nature
93 rdf:type schema:Organisation
94 Ne31fb953da814b06a162a1c17e112f6d rdf:first sg:person.014007552600.37
95 rdf:rest rdf:nil
96 Ne324eec1aa7a4dc59bda14cf30b32363 rdf:first sg:person.011375012273.39
97 rdf:rest N8e205fecfb41434fbb0f1a7cdc9b26ad
98 Needd49d4c65d466a9b31dbe687a1ca19 rdf:first N6444cf615c4541dc91d16f2f8f7fd1ad
99 rdf:rest rdf:nil
100 Nfcbe9fd8f8ae4e548c548420c8d967fb schema:name Springer Nature - SN SciGraph project
101 rdf:type schema:Organization
102 anzsrc-for:08 schema:inDefinedTermSet anzsrc-for:
103 schema:name Information and Computing Sciences
104 rdf:type schema:DefinedTerm
105 anzsrc-for:0801 schema:inDefinedTermSet anzsrc-for:
106 schema:name Artificial Intelligence and Image Processing
107 rdf:type schema:DefinedTerm
108 anzsrc-for:0802 schema:inDefinedTermSet anzsrc-for:
109 schema:name Computation Theory and Mathematics
110 rdf:type schema:DefinedTerm
111 anzsrc-for:0803 schema:inDefinedTermSet anzsrc-for:
112 schema:name Computer Software
113 rdf:type schema:DefinedTerm
114 sg:person.011375012273.39 schema:affiliation grid-institutes:grid.4991.5
115 schema:familyName Kwiatkowska
116 schema:givenName Marta
117 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011375012273.39
118 rdf:type schema:Person
119 sg:person.014007552600.37 schema:affiliation grid-institutes:grid.4991.5
120 schema:familyName Parker
121 schema:givenName David
122 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.014007552600.37
123 rdf:type schema:Person
124 sg:person.016323171577.36 schema:affiliation grid-institutes:grid.8756.c
125 schema:familyName Norman
126 schema:givenName Gethin
127 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.016323171577.36
128 rdf:type schema:Person
129 grid-institutes:grid.4991.5 schema:alternateName Oxford University Computing Laboratory, Parks Road, OX1 3QD, Oxford, UK
130 schema:name Oxford University Computing Laboratory, Parks Road, OX1 3QD, Oxford, UK
131 rdf:type schema:Organization
132 grid-institutes:grid.8756.c schema:alternateName Department of Computing Science, University of Glasgow, G12 8RZ, Glasgow, UK
133 schema:name Department of Computing Science, University of Glasgow, G12 8RZ, Glasgow, UK
134 rdf:type schema:Organization
 




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


...