PRISM 4.0: Verification of Probabilistic Real-Time Systems View Full Text


Ontology type: schema:Chapter      Open Access: True


Chapter Info

DATE

2011

AUTHORS

Marta Kwiatkowska , Gethin Norman , David Parker

ABSTRACT

This paper describes a major new release of the PRISM probabilistic model checker, adding, in particular, quantitative verification of (priced) probabilistic timed automata. These model systems exhibiting probabilistic, nondeterministic and real-time characteristics. In many application domains, all three aspects are essential; this includes, for example, embedded controllers in automotive or avionic systems, wireless communication protocols such as Bluetooth or Zigbee, and randomised security protocols. PRISM, which is open-source, also contains several new components that are of independent use. These include: an extensible toolkit for building, verifying and refining abstractions of probabilistic models; an explicit-state probabilistic model checking library; a discrete-event simulation engine for statistical model checking; support for generation of optimal adversaries/strategies; and a benchmark suite. More... »

PAGES

585-591

Identifiers

URI

http://scigraph.springernature.com/pub.10.1007/978-3-642-22110-1_47

DOI

http://dx.doi.org/10.1007/978-3-642-22110-1_47

DIMENSIONS

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


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, OX1 3QD, Oxford, UK", 
          "id": "http://www.grid.ac/institutes/grid.4991.5", 
          "name": [
            "Department of Computer Science, University of Oxford, 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": "School of Computing Science, University of Glasgow, G12 8RZ, Glasgow, UK", 
          "id": "http://www.grid.ac/institutes/grid.8756.c", 
          "name": [
            "School 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": "Department of Computer Science, University of Oxford, OX1 3QD, Oxford, UK", 
          "id": "http://www.grid.ac/institutes/grid.4991.5", 
          "name": [
            "Department of Computer Science, University of Oxford, 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": "2011", 
    "datePublishedReg": "2011-01-01", 
    "description": "This paper describes a major new release of the PRISM probabilistic model checker, adding, in particular, quantitative verification of (priced) probabilistic timed automata. These model systems exhibiting probabilistic, nondeterministic and real-time characteristics. In many application domains, all three aspects are essential; this includes, for example, embedded controllers in automotive or avionic systems, wireless communication protocols such as Bluetooth or Zigbee, and randomised security protocols. PRISM, which is open-source, also contains several new components that are of independent use. These include: an extensible toolkit for building, verifying and refining abstractions of probabilistic models; an explicit-state probabilistic model checking library; a discrete-event simulation engine for statistical model checking; support for generation of optimal adversaries/strategies; and a benchmark suite.", 
    "editor": [
      {
        "familyName": "Gopalakrishnan", 
        "givenName": "Ganesh", 
        "type": "Person"
      }, 
      {
        "familyName": "Qadeer", 
        "givenName": "Shaz", 
        "type": "Person"
      }
    ], 
    "genre": "chapter", 
    "id": "sg:pub.10.1007/978-3-642-22110-1_47", 
    "inLanguage": "en", 
    "isAccessibleForFree": true, 
    "isPartOf": {
      "isbn": [
        "978-3-642-22109-5", 
        "978-3-642-22110-1"
      ], 
      "name": "Computer Aided Verification", 
      "type": "Book"
    }, 
    "keywords": [
      "PRISM probabilistic model checker", 
      "probabilistic real-time systems", 
      "discrete event simulation engine", 
      "probabilistic model checker", 
      "real-time systems", 
      "wireless communication protocols", 
      "real-time characteristics", 
      "probabilistic model", 
      "statistical model checking", 
      "major new release", 
      "security protocols", 
      "application domains", 
      "model checker", 
      "model checking", 
      "simulation engine", 
      "Extensible Toolkit", 
      "communication protocols", 
      "avionics systems", 
      "benchmark suite", 
      "quantitative verification", 
      "new release", 
      "probabilistic", 
      "verification", 
      "new components", 
      "checker", 
      "ZigBee", 
      "checking", 
      "independent use", 
      "Bluetooth", 
      "abstraction", 
      "system", 
      "protocol", 
      "toolkit", 
      "automata", 
      "engine", 
      "controller", 
      "library", 
      "suite", 
      "model", 
      "domain", 
      "example", 
      "buildings", 
      "support", 
      "generation", 
      "aspects", 
      "strategies", 
      "use", 
      "components", 
      "characteristics", 
      "prism", 
      "model system", 
      "release", 
      "paper"
    ], 
    "name": "PRISM 4.0: Verification of Probabilistic Real-Time Systems", 
    "pagination": "585-591", 
    "productId": [
      {
        "name": "dimensions_id", 
        "type": "PropertyValue", 
        "value": [
          "pub.1027900693"
        ]
      }, 
      {
        "name": "doi", 
        "type": "PropertyValue", 
        "value": [
          "10.1007/978-3-642-22110-1_47"
        ]
      }
    ], 
    "publisher": {
      "name": "Springer Nature", 
      "type": "Organisation"
    }, 
    "sameAs": [
      "https://doi.org/10.1007/978-3-642-22110-1_47", 
      "https://app.dimensions.ai/details/publication/pub.1027900693"
    ], 
    "sdDataset": "chapters", 
    "sdDatePublished": "2022-05-10T10:54", 
    "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_450.jsonl", 
    "type": "Chapter", 
    "url": "https://doi.org/10.1007/978-3-642-22110-1_47"
  }
]
 

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-22110-1_47'

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-22110-1_47'

Turtle is a human-readable linked data format.

curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/978-3-642-22110-1_47'

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-22110-1_47'


 

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

143 TRIPLES      23 PREDICATES      81 URIs      72 LITERALS      7 BLANK NODES

Subject Predicate Object
1 sg:pub.10.1007/978-3-642-22110-1_47 schema:about anzsrc-for:08
2 anzsrc-for:0801
3 anzsrc-for:0802
4 anzsrc-for:0803
5 schema:author Nfec687657c564dd7979ee2c9b44783ae
6 schema:datePublished 2011
7 schema:datePublishedReg 2011-01-01
8 schema:description This paper describes a major new release of the PRISM probabilistic model checker, adding, in particular, quantitative verification of (priced) probabilistic timed automata. These model systems exhibiting probabilistic, nondeterministic and real-time characteristics. In many application domains, all three aspects are essential; this includes, for example, embedded controllers in automotive or avionic systems, wireless communication protocols such as Bluetooth or Zigbee, and randomised security protocols. PRISM, which is open-source, also contains several new components that are of independent use. These include: an extensible toolkit for building, verifying and refining abstractions of probabilistic models; an explicit-state probabilistic model checking library; a discrete-event simulation engine for statistical model checking; support for generation of optimal adversaries/strategies; and a benchmark suite.
9 schema:editor N43a8938fa7b34fc1a9ca859cfb6ffab8
10 schema:genre chapter
11 schema:inLanguage en
12 schema:isAccessibleForFree true
13 schema:isPartOf Nc56cdacc47944f1c8925250520d62c26
14 schema:keywords Bluetooth
15 Extensible Toolkit
16 PRISM probabilistic model checker
17 ZigBee
18 abstraction
19 application domains
20 aspects
21 automata
22 avionics systems
23 benchmark suite
24 buildings
25 characteristics
26 checker
27 checking
28 communication protocols
29 components
30 controller
31 discrete event simulation engine
32 domain
33 engine
34 example
35 generation
36 independent use
37 library
38 major new release
39 model
40 model checker
41 model checking
42 model system
43 new components
44 new release
45 paper
46 prism
47 probabilistic
48 probabilistic model
49 probabilistic model checker
50 probabilistic real-time systems
51 protocol
52 quantitative verification
53 real-time characteristics
54 real-time systems
55 release
56 security protocols
57 simulation engine
58 statistical model checking
59 strategies
60 suite
61 support
62 system
63 toolkit
64 use
65 verification
66 wireless communication protocols
67 schema:name PRISM 4.0: Verification of Probabilistic Real-Time Systems
68 schema:pagination 585-591
69 schema:productId Na69190b35f8d4548a05170e5868e8a7a
70 Nd0483d8425a24410825a3150ce675f6b
71 schema:publisher Nbf610df88b424d5caaee8b6f008f7f62
72 schema:sameAs https://app.dimensions.ai/details/publication/pub.1027900693
73 https://doi.org/10.1007/978-3-642-22110-1_47
74 schema:sdDatePublished 2022-05-10T10:54
75 schema:sdLicense https://scigraph.springernature.com/explorer/license/
76 schema:sdPublisher Nb83efe33e6924252a6b11bd9afb64a79
77 schema:url https://doi.org/10.1007/978-3-642-22110-1_47
78 sgo:license sg:explorer/license/
79 sgo:sdDataset chapters
80 rdf:type schema:Chapter
81 N43a8938fa7b34fc1a9ca859cfb6ffab8 rdf:first Nb26ec2f6f7fe4c3aa47dfc7e254c32eb
82 rdf:rest Nb29941899a0441718460aa1dea897a62
83 N5e3e4e97767142118021113f128682fb rdf:first sg:person.014007552600.37
84 rdf:rest rdf:nil
85 Na69190b35f8d4548a05170e5868e8a7a schema:name dimensions_id
86 schema:value pub.1027900693
87 rdf:type schema:PropertyValue
88 Nb26ec2f6f7fe4c3aa47dfc7e254c32eb schema:familyName Gopalakrishnan
89 schema:givenName Ganesh
90 rdf:type schema:Person
91 Nb29941899a0441718460aa1dea897a62 rdf:first Necf496450fee4458a03799eb1bd3db7b
92 rdf:rest rdf:nil
93 Nb83efe33e6924252a6b11bd9afb64a79 schema:name Springer Nature - SN SciGraph project
94 rdf:type schema:Organization
95 Nbf610df88b424d5caaee8b6f008f7f62 schema:name Springer Nature
96 rdf:type schema:Organisation
97 Nc56cdacc47944f1c8925250520d62c26 schema:isbn 978-3-642-22109-5
98 978-3-642-22110-1
99 schema:name Computer Aided Verification
100 rdf:type schema:Book
101 Nd0483d8425a24410825a3150ce675f6b schema:name doi
102 schema:value 10.1007/978-3-642-22110-1_47
103 rdf:type schema:PropertyValue
104 Ne1d912c742bb40eeba19bf708d9baccc rdf:first sg:person.016323171577.36
105 rdf:rest N5e3e4e97767142118021113f128682fb
106 Necf496450fee4458a03799eb1bd3db7b schema:familyName Qadeer
107 schema:givenName Shaz
108 rdf:type schema:Person
109 Nfec687657c564dd7979ee2c9b44783ae rdf:first sg:person.011375012273.39
110 rdf:rest Ne1d912c742bb40eeba19bf708d9baccc
111 anzsrc-for:08 schema:inDefinedTermSet anzsrc-for:
112 schema:name Information and Computing Sciences
113 rdf:type schema:DefinedTerm
114 anzsrc-for:0801 schema:inDefinedTermSet anzsrc-for:
115 schema:name Artificial Intelligence and Image Processing
116 rdf:type schema:DefinedTerm
117 anzsrc-for:0802 schema:inDefinedTermSet anzsrc-for:
118 schema:name Computation Theory and Mathematics
119 rdf:type schema:DefinedTerm
120 anzsrc-for:0803 schema:inDefinedTermSet anzsrc-for:
121 schema:name Computer Software
122 rdf:type schema:DefinedTerm
123 sg:person.011375012273.39 schema:affiliation grid-institutes:grid.4991.5
124 schema:familyName Kwiatkowska
125 schema:givenName Marta
126 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011375012273.39
127 rdf:type schema:Person
128 sg:person.014007552600.37 schema:affiliation grid-institutes:grid.4991.5
129 schema:familyName Parker
130 schema:givenName David
131 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.014007552600.37
132 rdf:type schema:Person
133 sg:person.016323171577.36 schema:affiliation grid-institutes:grid.8756.c
134 schema:familyName Norman
135 schema:givenName Gethin
136 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.016323171577.36
137 rdf:type schema:Person
138 grid-institutes:grid.4991.5 schema:alternateName Department of Computer Science, University of Oxford, OX1 3QD, Oxford, UK
139 schema:name Department of Computer Science, University of Oxford, OX1 3QD, Oxford, UK
140 rdf:type schema:Organization
141 grid-institutes:grid.8756.c schema:alternateName School of Computing Science, University of Glasgow, G12 8RZ, Glasgow, UK
142 schema:name School of Computing Science, University of Glasgow, G12 8RZ, Glasgow, UK
143 rdf:type schema:Organization
 




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


...