2010-02-03
AUTHORS ABSTRACTRecent development in computer hardware has brought more widespread emergence of shared memory, multi-core systems. These architectures offer opportunities to speed up various tasks—model checking and reachability analysis among others. In this paper, we present a design for a parallel shared memory LTL model checker that is based on a distributed memory algorithm. To improve the scalability of our tool, we have devised a number of implementation techniques which we present in this paper. We also report on a number of experiments we conducted to analyse the behaviour of our tool under different conditions using various models. We demonstrate that our tool exhibits significant speedup in comparison with sequential tools, which improves the workflow of verification in general. More... »
PAGES139-153
http://scigraph.springernature.com/pub.10.1007/s10009-010-0136-z
DOIhttp://dx.doi.org/10.1007/s10009-010-0136-z
DIMENSIONShttps://app.dimensions.ai/details/publication/pub.1004479089
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/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": "Barnat",
"givenName": "J.",
"id": "sg:person.011367557177.46",
"sameAs": [
"https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011367557177.46"
],
"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": "Brim",
"givenName": "L.",
"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": "Ro\u010dkai",
"givenName": "P.",
"id": "sg:person.07377571657.86",
"sameAs": [
"https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.07377571657.86"
],
"type": "Person"
}
],
"citation": [
{
"id": "sg:pub.10.1007/10722167_19",
"sameAs": [
"https://app.dimensions.ai/details/publication/pub.1009249763",
"https://doi.org/10.1007/10722167_19"
],
"type": "CreativeWork"
},
{
"id": "sg:pub.10.1007/3-540-45294-x_9",
"sameAs": [
"https://app.dimensions.ai/details/publication/pub.1012003768",
"https://doi.org/10.1007/3-540-45294-x_9"
],
"type": "CreativeWork"
},
{
"id": "sg:pub.10.1007/3-540-45319-9_29",
"sameAs": [
"https://app.dimensions.ai/details/publication/pub.1007959034",
"https://doi.org/10.1007/3-540-45319-9_29"
],
"type": "CreativeWork"
},
{
"id": "sg:pub.10.1007/3-540-45139-0_13",
"sameAs": [
"https://app.dimensions.ai/details/publication/pub.1026265425",
"https://doi.org/10.1007/3-540-45139-0_13"
],
"type": "CreativeWork"
},
{
"id": "sg:pub.10.1007/3-540-45139-0_14",
"sameAs": [
"https://app.dimensions.ai/details/publication/pub.1024798383",
"https://doi.org/10.1007/3-540-45139-0_14"
],
"type": "CreativeWork"
},
{
"id": "sg:pub.10.1007/978-3-540-30494-4_25",
"sameAs": [
"https://app.dimensions.ai/details/publication/pub.1034078638",
"https://doi.org/10.1007/978-3-540-30494-4_25"
],
"type": "CreativeWork"
},
{
"id": "sg:pub.10.1007/11817963_26",
"sameAs": [
"https://app.dimensions.ai/details/publication/pub.1032919459",
"https://doi.org/10.1007/11817963_26"
],
"type": "CreativeWork"
},
{
"id": "sg:pub.10.1007/978-3-540-73370-6_13",
"sameAs": [
"https://app.dimensions.ai/details/publication/pub.1020358888",
"https://doi.org/10.1007/978-3-540-73370-6_13"
],
"type": "CreativeWork"
},
{
"id": "sg:pub.10.1007/bf00121128",
"sameAs": [
"https://app.dimensions.ai/details/publication/pub.1017183522",
"https://doi.org/10.1007/bf00121128"
],
"type": "CreativeWork"
},
{
"id": "sg:pub.10.1007/978-3-540-31980-1_12",
"sameAs": [
"https://app.dimensions.ai/details/publication/pub.1050210627",
"https://doi.org/10.1007/978-3-540-31980-1_12"
],
"type": "CreativeWork"
},
{
"id": "sg:pub.10.1007/s10009-003-0129-2",
"sameAs": [
"https://app.dimensions.ai/details/publication/pub.1000360168",
"https://doi.org/10.1007/s10009-003-0129-2"
],
"type": "CreativeWork"
},
{
"id": "sg:pub.10.1007/11804192_13",
"sameAs": [
"https://app.dimensions.ai/details/publication/pub.1026730916",
"https://doi.org/10.1007/11804192_13"
],
"type": "CreativeWork"
},
{
"id": "sg:pub.10.1007/s10009-004-0159-4",
"sameAs": [
"https://app.dimensions.ai/details/publication/pub.1031088090",
"https://doi.org/10.1007/s10009-004-0159-4"
],
"type": "CreativeWork"
},
{
"id": "sg:pub.10.1007/3-540-44829-2_4",
"sameAs": [
"https://app.dimensions.ai/details/publication/pub.1030278825",
"https://doi.org/10.1007/3-540-44829-2_4"
],
"type": "CreativeWork"
},
{
"id": "sg:pub.10.1007/3-540-44585-4_32",
"sameAs": [
"https://app.dimensions.ai/details/publication/pub.1024361338",
"https://doi.org/10.1007/3-540-44585-4_32"
],
"type": "CreativeWork"
},
{
"id": "sg:pub.10.1007/s10703-006-0008-z",
"sameAs": [
"https://app.dimensions.ai/details/publication/pub.1033073224",
"https://doi.org/10.1007/s10703-006-0008-z"
],
"type": "CreativeWork"
},
{
"id": "sg:pub.10.1007/3-540-45319-9_37",
"sameAs": [
"https://app.dimensions.ai/details/publication/pub.1029394493",
"https://doi.org/10.1007/3-540-45319-9_37"
],
"type": "CreativeWork"
},
{
"id": "sg:pub.10.1007/978-3-540-88387-6_20",
"sameAs": [
"https://app.dimensions.ai/details/publication/pub.1028071874",
"https://doi.org/10.1007/978-3-540-88387-6_20"
],
"type": "CreativeWork"
},
{
"id": "sg:pub.10.1007/978-3-540-73370-6_17",
"sameAs": [
"https://app.dimensions.ai/details/publication/pub.1028539011",
"https://doi.org/10.1007/978-3-540-73370-6_17"
],
"type": "CreativeWork"
},
{
"id": "sg:pub.10.1007/11560548_12",
"sameAs": [
"https://app.dimensions.ai/details/publication/pub.1035834889",
"https://doi.org/10.1007/11560548_12"
],
"type": "CreativeWork"
},
{
"id": "sg:pub.10.1007/978-3-540-69738-1_10",
"sameAs": [
"https://app.dimensions.ai/details/publication/pub.1021934512",
"https://doi.org/10.1007/978-3-540-69738-1_10"
],
"type": "CreativeWork"
},
{
"id": "sg:pub.10.1007/3-540-60029-9_40",
"sameAs": [
"https://app.dimensions.ai/details/publication/pub.1017109609",
"https://doi.org/10.1007/3-540-60029-9_40"
],
"type": "CreativeWork"
}
],
"datePublished": "2010-02-03",
"datePublishedReg": "2010-02-03",
"description": "Recent development in computer hardware has brought more widespread emergence of shared memory, multi-core systems. These architectures offer opportunities to speed up various tasks\u2014model checking and reachability analysis among others. In this paper, we present a design for a parallel shared memory LTL model checker that is based on a distributed memory algorithm. To improve the scalability of our tool, we have devised a number of implementation techniques which we present in this paper. We also report on a number of experiments we conducted to analyse the behaviour of our tool under different conditions using various models. We demonstrate that our tool exhibits significant speedup in comparison with sequential tools, which improves the workflow of verification in general.",
"genre": "article",
"id": "sg:pub.10.1007/s10009-010-0136-z",
"inLanguage": "en",
"isAccessibleForFree": false,
"isPartOf": [
{
"id": "sg:journal.1052641",
"issn": [
"1433-2779",
"1433-2787"
],
"name": "International Journal on Software Tools for Technology Transfer",
"publisher": "Springer Nature",
"type": "Periodical"
},
{
"issueNumber": "2",
"type": "PublicationIssue"
},
{
"type": "PublicationVolume",
"volumeNumber": "12"
}
],
"keywords": [
"LTL model checker",
"multi-core systems",
"model checker",
"computer hardware",
"memory algorithm",
"significant speedup",
"LTL model",
"implementation techniques",
"sequential tools",
"reachability analysis",
"number of experiments",
"tool",
"scalability",
"Scalable",
"checker",
"speedup",
"hardware",
"checking",
"architecture",
"workflow",
"algorithm",
"verification",
"model",
"recent developments",
"memory",
"system",
"design",
"technique",
"number",
"experiments",
"opportunities",
"different conditions",
"widespread emergence",
"development",
"emergence",
"behavior",
"comparison",
"analysis",
"conditions",
"paper"
],
"name": "Scalable shared memory LTL model checking",
"pagination": "139-153",
"productId": [
{
"name": "dimensions_id",
"type": "PropertyValue",
"value": [
"pub.1004479089"
]
},
{
"name": "doi",
"type": "PropertyValue",
"value": [
"10.1007/s10009-010-0136-z"
]
}
],
"sameAs": [
"https://doi.org/10.1007/s10009-010-0136-z",
"https://app.dimensions.ai/details/publication/pub.1004479089"
],
"sdDataset": "articles",
"sdDatePublished": "2022-05-10T09:59",
"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/article/article_526.jsonl",
"type": "ScholarlyArticle",
"url": "https://doi.org/10.1007/s10009-010-0136-z"
}
]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/s10009-010-0136-z'
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/s10009-010-0136-z'
Turtle is a human-readable linked data format.
curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/s10009-010-0136-z'
RDF/XML is a standard XML format for linked data.
curl -H 'Accept: application/rdf+xml' 'https://scigraph.springernature.com/pub.10.1007/s10009-010-0136-z'
This table displays all metadata directly associated to this object as RDF triples.
204 TRIPLES
22 PREDICATES
88 URIs
57 LITERALS
6 BLANK NODES