2007
AUTHORS ABSTRACTWith 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... »
PAGES2-3
Model Checking Software
ISBN
978-3-540-73369-0
978-3-540-73370-6
http://scigraph.springernature.com/pub.10.1007/978-3-540-73370-6_2
DOIhttp://dx.doi.org/10.1007/978-3-540-73370-6_2
DIMENSIONShttps://app.dimensions.ai/details/publication/pub.1003860349
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
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 |