Tutorial: Parallel Model Checking View Full Text


Ontology type: schema:Chapter     


Chapter Info

DATE

2007

AUTHORS

Luboš Brim , Jiří Barnat

ABSTRACT

With the increase in the complexity of computer systems, it becomes even more important to develop formal methods for ensuring their quality. Various techniques for automated and semi-automated analysis and verification have been proposed. In particular, model-checking has become a very practical technique due to its push-button character. The basic principle behind model-checking is to build a model of the system under consideration together with a formal description of the verified property in a suitable temporal logic. The model-checking algorithm is a decision procedure which in addition to the yes/no answer returns a trace of a faulty behaviour in case the checked property is not satisfied by the model. One of the additional advantages of this approach is that verification can be performed against partial specifications, by considering only a subset of all specification requirements. This allows for increased efficiency by checking correctness with respect to only the most relevant requirements that should be fulfilled. More... »

PAGES

2-3

Identifiers

URI

http://scigraph.springernature.com/pub.10.1007/978-3-540-73370-6_2

DOI

http://dx.doi.org/10.1007/978-3-540-73370-6_2

DIMENSIONS

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


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": "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": "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": "2007", 
    "datePublishedReg": "2007-01-01", 
    "description": "With the increase in the complexity of computer systems, it becomes even more important to develop formal methods for ensuring their quality. Various techniques for automated and semi-automated analysis and verification have been proposed. In particular, model-checking has become a very practical technique due to its push-button character. The basic principle behind model-checking is to build a model of the system under consideration together with a formal description of the verified property in a suitable temporal logic. The model-checking algorithm is a decision procedure which in addition to the yes/no answer returns a trace of a faulty behaviour in case the checked property is not satisfied by the model. One of the additional advantages of this approach is that verification can be performed against partial specifications, by considering only a subset of all specification requirements. This allows for increased efficiency by checking correctness with respect to only the most relevant requirements that should be fulfilled.", 
    "editor": [
      {
        "familyName": "Bo\u0161na\u010dki", 
        "givenName": "Dragan", 
        "type": "Person"
      }, 
      {
        "familyName": "Edelkamp", 
        "givenName": "Stefan", 
        "type": "Person"
      }
    ], 
    "genre": "chapter", 
    "id": "sg:pub.10.1007/978-3-540-73370-6_2", 
    "inLanguage": "en", 
    "isAccessibleForFree": false, 
    "isPartOf": {
      "isbn": [
        "978-3-540-73369-0", 
        "978-3-540-73370-6"
      ], 
      "name": "Model Checking Software", 
      "type": "Book"
    }, 
    "keywords": [
      "suitable temporal logic", 
      "parallel model checking", 
      "model-checking algorithm", 
      "formal methods", 
      "model checking", 
      "computer systems", 
      "temporal logic", 
      "verified properties", 
      "partial specifications", 
      "formal description", 
      "faulty behavior", 
      "relevant requirements", 
      "decision procedure", 
      "verification", 
      "specification requirements", 
      "practical technique", 
      "requirements", 
      "checking", 
      "algorithm", 
      "correctness", 
      "specification", 
      "system", 
      "logic", 
      "complexity", 
      "technique", 
      "basic principles", 
      "additional advantage", 
      "model", 
      "traces", 
      "advantages", 
      "efficiency", 
      "answers", 
      "quality", 
      "description", 
      "method", 
      "subset", 
      "principles", 
      "consideration", 
      "respect", 
      "behavior", 
      "analysis", 
      "procedure", 
      "cases", 
      "addition", 
      "character", 
      "properties", 
      "increase", 
      "approach"
    ], 
    "name": "Tutorial: Parallel Model Checking", 
    "pagination": "2-3", 
    "productId": [
      {
        "name": "dimensions_id", 
        "type": "PropertyValue", 
        "value": [
          "pub.1003860349"
        ]
      }, 
      {
        "name": "doi", 
        "type": "PropertyValue", 
        "value": [
          "10.1007/978-3-540-73370-6_2"
        ]
      }
    ], 
    "publisher": {
      "name": "Springer Nature", 
      "type": "Organisation"
    }, 
    "sameAs": [
      "https://doi.org/10.1007/978-3-540-73370-6_2", 
      "https://app.dimensions.ai/details/publication/pub.1003860349"
    ], 
    "sdDataset": "chapters", 
    "sdDatePublished": "2022-05-20T07:46", 
    "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_325.jsonl", 
    "type": "Chapter", 
    "url": "https://doi.org/10.1007/978-3-540-73370-6_2"
  }
]
 

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-540-73370-6_2'

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-540-73370-6_2'

Turtle is a human-readable linked data format.

curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/978-3-540-73370-6_2'

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-540-73370-6_2'


 

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

128 TRIPLES      23 PREDICATES      76 URIs      67 LITERALS      7 BLANK NODES

Subject Predicate Object
1 sg:pub.10.1007/978-3-540-73370-6_2 schema:about anzsrc-for:08
2 anzsrc-for:0801
3 anzsrc-for:0802
4 anzsrc-for:0803
5 schema:author N3ae54e206e934bfaa4c139e903b80280
6 schema:datePublished 2007
7 schema:datePublishedReg 2007-01-01
8 schema:description With the increase in the complexity of computer systems, it becomes even more important to develop formal methods for ensuring their quality. Various techniques for automated and semi-automated analysis and verification have been proposed. In particular, model-checking has become a very practical technique due to its push-button character. The basic principle behind model-checking is to build a model of the system under consideration together with a formal description of the verified property in a suitable temporal logic. The model-checking algorithm is a decision procedure which in addition to the yes/no answer returns a trace of a faulty behaviour in case the checked property is not satisfied by the model. One of the additional advantages of this approach is that verification can be performed against partial specifications, by considering only a subset of all specification requirements. This allows for increased efficiency by checking correctness with respect to only the most relevant requirements that should be fulfilled.
9 schema:editor N99f243af4d3342758431c1d8329ab399
10 schema:genre chapter
11 schema:inLanguage en
12 schema:isAccessibleForFree false
13 schema:isPartOf N1ba3287731fd494d8c92c5981c594fc8
14 schema:keywords addition
15 additional advantage
16 advantages
17 algorithm
18 analysis
19 answers
20 approach
21 basic principles
22 behavior
23 cases
24 character
25 checking
26 complexity
27 computer systems
28 consideration
29 correctness
30 decision procedure
31 description
32 efficiency
33 faulty behavior
34 formal description
35 formal methods
36 increase
37 logic
38 method
39 model
40 model checking
41 model-checking algorithm
42 parallel model checking
43 partial specifications
44 practical technique
45 principles
46 procedure
47 properties
48 quality
49 relevant requirements
50 requirements
51 respect
52 specification
53 specification requirements
54 subset
55 suitable temporal logic
56 system
57 technique
58 temporal logic
59 traces
60 verification
61 verified properties
62 schema:name Tutorial: Parallel Model Checking
63 schema:pagination 2-3
64 schema:productId N1702ae9a09664a60b0fd191a868e6040
65 Nd6f2a5e752364652993064a97ad44f40
66 schema:publisher N4407da9371db4f0dbbe72110ceb96c6a
67 schema:sameAs https://app.dimensions.ai/details/publication/pub.1003860349
68 https://doi.org/10.1007/978-3-540-73370-6_2
69 schema:sdDatePublished 2022-05-20T07:46
70 schema:sdLicense https://scigraph.springernature.com/explorer/license/
71 schema:sdPublisher Nbca0aa8fbce8414a8a841cfb83d22792
72 schema:url https://doi.org/10.1007/978-3-540-73370-6_2
73 sgo:license sg:explorer/license/
74 sgo:sdDataset chapters
75 rdf:type schema:Chapter
76 N1702ae9a09664a60b0fd191a868e6040 schema:name doi
77 schema:value 10.1007/978-3-540-73370-6_2
78 rdf:type schema:PropertyValue
79 N1ba3287731fd494d8c92c5981c594fc8 schema:isbn 978-3-540-73369-0
80 978-3-540-73370-6
81 schema:name Model Checking Software
82 rdf:type schema:Book
83 N3ae54e206e934bfaa4c139e903b80280 rdf:first sg:person.0645117057.83
84 rdf:rest Nbba92242549f4e02bdfae4f8389be79b
85 N4407da9371db4f0dbbe72110ceb96c6a schema:name Springer Nature
86 rdf:type schema:Organisation
87 N8f28ee748fa0404f82d31987d54adb73 schema:familyName Edelkamp
88 schema:givenName Stefan
89 rdf:type schema:Person
90 N961cba3803344e6eaffb75887dc9cc19 rdf:first N8f28ee748fa0404f82d31987d54adb73
91 rdf:rest rdf:nil
92 N99f243af4d3342758431c1d8329ab399 rdf:first Ne8797268384b4d6a99f941e5de44d7d2
93 rdf:rest N961cba3803344e6eaffb75887dc9cc19
94 Nbba92242549f4e02bdfae4f8389be79b rdf:first sg:person.011367557177.46
95 rdf:rest rdf:nil
96 Nbca0aa8fbce8414a8a841cfb83d22792 schema:name Springer Nature - SN SciGraph project
97 rdf:type schema:Organization
98 Nd6f2a5e752364652993064a97ad44f40 schema:name dimensions_id
99 schema:value pub.1003860349
100 rdf:type schema:PropertyValue
101 Ne8797268384b4d6a99f941e5de44d7d2 schema:familyName Bošnački
102 schema:givenName Dragan
103 rdf:type schema:Person
104 anzsrc-for:08 schema:inDefinedTermSet anzsrc-for:
105 schema:name Information and Computing Sciences
106 rdf:type schema:DefinedTerm
107 anzsrc-for:0801 schema:inDefinedTermSet anzsrc-for:
108 schema:name Artificial Intelligence and Image Processing
109 rdf:type schema:DefinedTerm
110 anzsrc-for:0802 schema:inDefinedTermSet anzsrc-for:
111 schema:name Computation Theory and Mathematics
112 rdf:type schema:DefinedTerm
113 anzsrc-for:0803 schema:inDefinedTermSet anzsrc-for:
114 schema:name Computer Software
115 rdf:type schema:DefinedTerm
116 sg:person.011367557177.46 schema:affiliation grid-institutes:grid.10267.32
117 schema:familyName Barnat
118 schema:givenName Jiří
119 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011367557177.46
120 rdf:type schema:Person
121 sg:person.0645117057.83 schema:affiliation grid-institutes:grid.10267.32
122 schema:familyName Brim
123 schema:givenName Luboš
124 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.0645117057.83
125 rdf:type schema:Person
126 grid-institutes:grid.10267.32 schema:alternateName Faculty of Informatics, Masaryk University, Brno, Czech Republic
127 schema:name Faculty of Informatics, Masaryk University, Brno, Czech Republic
128 rdf:type schema:Organization
 




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


...