Defining and Model Checking Abstractions of Complex Railway Models Using CSP||B View Full Text


Ontology type: schema:Chapter      Open Access: True


Chapter Info

DATE

2013

AUTHORS

Faron Moller , Hoang Nga Nguyen , Markus Roggenbach , Steve Schneider , Helen Treharne

ABSTRACT

The safety analysis of interlocking railway systems involves verifying collision and derailment freedom. In this paper we propose a structured way of refining track plans, in order to expand track segments so that they form collections of track segments. We show how the abstract model can be model checked to ensure the safety properties, which must also hold in the corresponding concrete track plan, so that we will never need to model check the concrete track plan directly. We also identify the minimal number of trains that needs to be considered as part of the model checking, and we demonstrate the practicality of the approach on various scenarios. More... »

PAGES

193-208

Book

TITLE

Hardware and Software: Verification and Testing

ISBN

978-3-642-39610-6
978-3-642-39611-3

Identifiers

URI

http://scigraph.springernature.com/pub.10.1007/978-3-642-39611-3_20

DOI

http://dx.doi.org/10.1007/978-3-642-39611-3_20

DIMENSIONS

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


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/09", 
        "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
        "name": "Engineering", 
        "type": "DefinedTerm"
      }, 
      {
        "id": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/0905", 
        "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
        "name": "Civil Engineering", 
        "type": "DefinedTerm"
      }
    ], 
    "author": [
      {
        "affiliation": {
          "alternateName": "Swansea University, Wales, UK", 
          "id": "http://www.grid.ac/institutes/grid.4827.9", 
          "name": [
            "Swansea University, Wales, UK"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Moller", 
        "givenName": "Faron", 
        "id": "sg:person.010425236217.29", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.010425236217.29"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "Swansea University, Wales, UK", 
          "id": "http://www.grid.ac/institutes/grid.4827.9", 
          "name": [
            "Swansea University, Wales, UK"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Nguyen", 
        "givenName": "Hoang Nga", 
        "id": "sg:person.014355405221.01", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.014355405221.01"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "Swansea University, Wales, UK", 
          "id": "http://www.grid.ac/institutes/grid.4827.9", 
          "name": [
            "Swansea University, Wales, UK"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Roggenbach", 
        "givenName": "Markus", 
        "id": "sg:person.014634147051.77", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.014634147051.77"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "University of Surrey, England, UK", 
          "id": "http://www.grid.ac/institutes/grid.5475.3", 
          "name": [
            "University of Surrey, England, UK"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Schneider", 
        "givenName": "Steve", 
        "id": "sg:person.011014111222.37", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011014111222.37"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "University of Surrey, England, UK", 
          "id": "http://www.grid.ac/institutes/grid.5475.3", 
          "name": [
            "University of Surrey, England, UK"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Treharne", 
        "givenName": "Helen", 
        "id": "sg:person.012731025010.44", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.012731025010.44"
        ], 
        "type": "Person"
      }
    ], 
    "datePublished": "2013", 
    "datePublishedReg": "2013-01-01", 
    "description": "The safety analysis of interlocking railway systems involves verifying collision and derailment freedom. In this paper we propose a structured way of refining track plans, in order to expand track segments so that they form collections of track segments. We show how the abstract model can be model checked to ensure the safety properties, which must also hold in the corresponding concrete track plan, so that we will never need to model check the concrete track plan directly. We also identify the minimal number of trains that needs to be considered as part of the model checking, and we demonstrate the practicality of the approach on various scenarios.", 
    "editor": [
      {
        "familyName": "Biere", 
        "givenName": "Armin", 
        "type": "Person"
      }, 
      {
        "familyName": "Nahir", 
        "givenName": "Amir", 
        "type": "Person"
      }, 
      {
        "familyName": "Vos", 
        "givenName": "Tanja", 
        "type": "Person"
      }
    ], 
    "genre": "chapter", 
    "id": "sg:pub.10.1007/978-3-642-39611-3_20", 
    "inLanguage": "en", 
    "isAccessibleForFree": true, 
    "isPartOf": {
      "isbn": [
        "978-3-642-39610-6", 
        "978-3-642-39611-3"
      ], 
      "name": "Hardware and Software: Verification and Testing", 
      "type": "Book"
    }, 
    "keywords": [
      "track plan", 
      "railway system", 
      "track segments", 
      "railway model", 
      "safety analysis", 
      "model checking", 
      "abstract model", 
      "safety properties", 
      "structured way", 
      "model", 
      "properties", 
      "train", 
      "minimal number", 
      "system", 
      "order", 
      "checking", 
      "scenarios", 
      "practicality", 
      "abstraction", 
      "freedom", 
      "collisions", 
      "approach", 
      "plan", 
      "analysis", 
      "part", 
      "segments", 
      "collection", 
      "way", 
      "number", 
      "paper"
    ], 
    "name": "Defining and Model Checking Abstractions of Complex Railway Models Using CSP||B", 
    "pagination": "193-208", 
    "productId": [
      {
        "name": "dimensions_id", 
        "type": "PropertyValue", 
        "value": [
          "pub.1021640272"
        ]
      }, 
      {
        "name": "doi", 
        "type": "PropertyValue", 
        "value": [
          "10.1007/978-3-642-39611-3_20"
        ]
      }
    ], 
    "publisher": {
      "name": "Springer Nature", 
      "type": "Organisation"
    }, 
    "sameAs": [
      "https://doi.org/10.1007/978-3-642-39611-3_20", 
      "https://app.dimensions.ai/details/publication/pub.1021640272"
    ], 
    "sdDataset": "chapters", 
    "sdDatePublished": "2022-05-20T07:44", 
    "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_268.jsonl", 
    "type": "Chapter", 
    "url": "https://doi.org/10.1007/978-3-642-39611-3_20"
  }
]
 

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-39611-3_20'

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-39611-3_20'

Turtle is a human-readable linked data format.

curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/978-3-642-39611-3_20'

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-39611-3_20'


 

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

131 TRIPLES      23 PREDICATES      56 URIs      49 LITERALS      7 BLANK NODES

Subject Predicate Object
1 sg:pub.10.1007/978-3-642-39611-3_20 schema:about anzsrc-for:09
2 anzsrc-for:0905
3 schema:author N59d7d9752f9d401d84d7dbfaa2566af3
4 schema:datePublished 2013
5 schema:datePublishedReg 2013-01-01
6 schema:description The safety analysis of interlocking railway systems involves verifying collision and derailment freedom. In this paper we propose a structured way of refining track plans, in order to expand track segments so that they form collections of track segments. We show how the abstract model can be model checked to ensure the safety properties, which must also hold in the corresponding concrete track plan, so that we will never need to model check the concrete track plan directly. We also identify the minimal number of trains that needs to be considered as part of the model checking, and we demonstrate the practicality of the approach on various scenarios.
7 schema:editor N10fe2cb117154509a3e51990fb96e4be
8 schema:genre chapter
9 schema:inLanguage en
10 schema:isAccessibleForFree true
11 schema:isPartOf N60fb7d3ed2bf4d98895461fa15a24db7
12 schema:keywords abstract model
13 abstraction
14 analysis
15 approach
16 checking
17 collection
18 collisions
19 freedom
20 minimal number
21 model
22 model checking
23 number
24 order
25 paper
26 part
27 plan
28 practicality
29 properties
30 railway model
31 railway system
32 safety analysis
33 safety properties
34 scenarios
35 segments
36 structured way
37 system
38 track plan
39 track segments
40 train
41 way
42 schema:name Defining and Model Checking Abstractions of Complex Railway Models Using CSP||B
43 schema:pagination 193-208
44 schema:productId N275bb637962545ebab61cf93cace4bfb
45 Nad5719ec76de4fed88c72e36f6313426
46 schema:publisher Ne7ad0fc0a0574a1288f7024eb1a897da
47 schema:sameAs https://app.dimensions.ai/details/publication/pub.1021640272
48 https://doi.org/10.1007/978-3-642-39611-3_20
49 schema:sdDatePublished 2022-05-20T07:44
50 schema:sdLicense https://scigraph.springernature.com/explorer/license/
51 schema:sdPublisher N996db279b63d4c09993ad7f5d89ee30a
52 schema:url https://doi.org/10.1007/978-3-642-39611-3_20
53 sgo:license sg:explorer/license/
54 sgo:sdDataset chapters
55 rdf:type schema:Chapter
56 N10fe2cb117154509a3e51990fb96e4be rdf:first N523f282f816141d89f0b302c0640a21b
57 rdf:rest N5b864b1b25434ea3ad6cd39220f3a27f
58 N1fa6cd1ed8a44d00b9209d52b76e1097 rdf:first Nceaa2a2c12ee4e51bf5cab1fad07d5c3
59 rdf:rest rdf:nil
60 N275bb637962545ebab61cf93cace4bfb schema:name doi
61 schema:value 10.1007/978-3-642-39611-3_20
62 rdf:type schema:PropertyValue
63 N523f282f816141d89f0b302c0640a21b schema:familyName Biere
64 schema:givenName Armin
65 rdf:type schema:Person
66 N54a7522415ca4408b972e96c8b6eb3ee schema:familyName Nahir
67 schema:givenName Amir
68 rdf:type schema:Person
69 N59d7d9752f9d401d84d7dbfaa2566af3 rdf:first sg:person.010425236217.29
70 rdf:rest N9ed7e8ab7cc94d01a2b1abed2c513e19
71 N5b864b1b25434ea3ad6cd39220f3a27f rdf:first N54a7522415ca4408b972e96c8b6eb3ee
72 rdf:rest N1fa6cd1ed8a44d00b9209d52b76e1097
73 N60fb7d3ed2bf4d98895461fa15a24db7 schema:isbn 978-3-642-39610-6
74 978-3-642-39611-3
75 schema:name Hardware and Software: Verification and Testing
76 rdf:type schema:Book
77 N996db279b63d4c09993ad7f5d89ee30a schema:name Springer Nature - SN SciGraph project
78 rdf:type schema:Organization
79 N9b4b019508714347ba071db70aff066e rdf:first sg:person.011014111222.37
80 rdf:rest Nec7e6040fa18447fb4453f25db03bf2b
81 N9ed7e8ab7cc94d01a2b1abed2c513e19 rdf:first sg:person.014355405221.01
82 rdf:rest Nce0945fbca394798954b28a437d02823
83 Nad5719ec76de4fed88c72e36f6313426 schema:name dimensions_id
84 schema:value pub.1021640272
85 rdf:type schema:PropertyValue
86 Nce0945fbca394798954b28a437d02823 rdf:first sg:person.014634147051.77
87 rdf:rest N9b4b019508714347ba071db70aff066e
88 Nceaa2a2c12ee4e51bf5cab1fad07d5c3 schema:familyName Vos
89 schema:givenName Tanja
90 rdf:type schema:Person
91 Ne7ad0fc0a0574a1288f7024eb1a897da schema:name Springer Nature
92 rdf:type schema:Organisation
93 Nec7e6040fa18447fb4453f25db03bf2b rdf:first sg:person.012731025010.44
94 rdf:rest rdf:nil
95 anzsrc-for:09 schema:inDefinedTermSet anzsrc-for:
96 schema:name Engineering
97 rdf:type schema:DefinedTerm
98 anzsrc-for:0905 schema:inDefinedTermSet anzsrc-for:
99 schema:name Civil Engineering
100 rdf:type schema:DefinedTerm
101 sg:person.010425236217.29 schema:affiliation grid-institutes:grid.4827.9
102 schema:familyName Moller
103 schema:givenName Faron
104 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.010425236217.29
105 rdf:type schema:Person
106 sg:person.011014111222.37 schema:affiliation grid-institutes:grid.5475.3
107 schema:familyName Schneider
108 schema:givenName Steve
109 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011014111222.37
110 rdf:type schema:Person
111 sg:person.012731025010.44 schema:affiliation grid-institutes:grid.5475.3
112 schema:familyName Treharne
113 schema:givenName Helen
114 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.012731025010.44
115 rdf:type schema:Person
116 sg:person.014355405221.01 schema:affiliation grid-institutes:grid.4827.9
117 schema:familyName Nguyen
118 schema:givenName Hoang Nga
119 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.014355405221.01
120 rdf:type schema:Person
121 sg:person.014634147051.77 schema:affiliation grid-institutes:grid.4827.9
122 schema:familyName Roggenbach
123 schema:givenName Markus
124 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.014634147051.77
125 rdf:type schema:Person
126 grid-institutes:grid.4827.9 schema:alternateName Swansea University, Wales, UK
127 schema:name Swansea University, Wales, UK
128 rdf:type schema:Organization
129 grid-institutes:grid.5475.3 schema:alternateName University of Surrey, England, UK
130 schema:name University of Surrey, England, UK
131 rdf:type schema:Organization
 




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


...