Verification of Solid State Interlocking Programs View Full Text


Ontology type: schema:Chapter      Open Access: True


Chapter Info

DATE

2014-03-08

AUTHORS

Phillip James , Andy Lawrence , Faron Moller , Markus Roggenbach , Monika Seisenberger , Anton Setzer , Karim Kanso , Simon Chadwick

ABSTRACT

We report on the inclusion of a formal method into an industrial design process. Concretely, we suggest carrying out a verification step in railway interlocking design between programming the interlocking and testing this program. Safety still relies on testing, but the burden of guaranteeing completeness and correctness of the validation is in this way greatly reduced. We present a complete methodology for carrying out this verification step in the case of ladder logic programs and give results for real world railway interlockings. As this verification step reduces costs for testing, Invensys Rail is working to include such a verification step into their design process of solid state interlockings. More... »

PAGES

253-268

Identifiers

URI

http://scigraph.springernature.com/pub.10.1007/978-3-319-05032-4_19

DOI

http://dx.doi.org/10.1007/978-3-319-05032-4_19

DIMENSIONS

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


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/0803", 
        "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
        "name": "Computer Software", 
        "type": "DefinedTerm"
      }
    ], 
    "author": [
      {
        "affiliation": {
          "alternateName": "Swansea Railway Verification Group, Swansea University, Wales, UK", 
          "id": "http://www.grid.ac/institutes/grid.4827.9", 
          "name": [
            "Swansea Railway Verification Group, Swansea University, Wales, UK"
          ], 
          "type": "Organization"
        }, 
        "familyName": "James", 
        "givenName": "Phillip", 
        "id": "sg:person.012345226005.23", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.012345226005.23"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "Swansea Railway Verification Group, Swansea University, Wales, UK", 
          "id": "http://www.grid.ac/institutes/grid.4827.9", 
          "name": [
            "Swansea Railway Verification Group, Swansea University, Wales, UK"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Lawrence", 
        "givenName": "Andy", 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "Swansea Railway Verification Group, Swansea University, Wales, UK", 
          "id": "http://www.grid.ac/institutes/grid.4827.9", 
          "name": [
            "Swansea Railway Verification Group, 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 Railway Verification Group, Swansea University, Wales, UK", 
          "id": "http://www.grid.ac/institutes/grid.4827.9", 
          "name": [
            "Swansea Railway Verification Group, 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": "Swansea Railway Verification Group, Swansea University, Wales, UK", 
          "id": "http://www.grid.ac/institutes/grid.4827.9", 
          "name": [
            "Swansea Railway Verification Group, Swansea University, Wales, UK"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Seisenberger", 
        "givenName": "Monika", 
        "id": "sg:person.015333130005.81", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.015333130005.81"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "Swansea Railway Verification Group, Swansea University, Wales, UK", 
          "id": "http://www.grid.ac/institutes/grid.4827.9", 
          "name": [
            "Swansea Railway Verification Group, Swansea University, Wales, UK"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Setzer", 
        "givenName": "Anton", 
        "id": "sg:person.016555714573.74", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.016555714573.74"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "Critical Software Technologies, Southampton, England, UK", 
          "id": "http://www.grid.ac/institutes/None", 
          "name": [
            "Critical Software Technologies, Southampton, England, UK"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Kanso", 
        "givenName": "Karim", 
        "id": "sg:person.07425437205.83", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.07425437205.83"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "Invensys Rail, Chippenham, England, UK", 
          "id": "http://www.grid.ac/institutes/None", 
          "name": [
            "Invensys Rail, Chippenham, England, UK"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Chadwick", 
        "givenName": "Simon", 
        "id": "sg:person.010223017605.64", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.010223017605.64"
        ], 
        "type": "Person"
      }
    ], 
    "datePublished": "2014-03-08", 
    "datePublishedReg": "2014-03-08", 
    "description": "We report on the inclusion of a formal method into an industrial design process. Concretely, we suggest carrying out a verification step in railway interlocking design between programming the interlocking and testing this program. Safety still relies on testing, but the burden of guaranteeing completeness and correctness of the validation is in this way greatly reduced. We present a complete methodology for carrying out this verification step in the case of ladder logic programs and give results for real world railway interlockings. As this verification step reduces costs for testing, Invensys Rail is working to include such a verification step into their design process of solid state interlockings.", 
    "editor": [
      {
        "familyName": "Counsell", 
        "givenName": "Steve", 
        "type": "Person"
      }, 
      {
        "familyName": "N\u00fa\u00f1ez", 
        "givenName": "Manuel", 
        "type": "Person"
      }
    ], 
    "genre": "chapter", 
    "id": "sg:pub.10.1007/978-3-319-05032-4_19", 
    "inLanguage": "en", 
    "isAccessibleForFree": true, 
    "isPartOf": {
      "isbn": [
        "978-3-319-05031-7", 
        "978-3-319-05032-4"
      ], 
      "name": "Software Engineering and Formal Methods", 
      "type": "Book"
    }, 
    "keywords": [
      "verification step", 
      "ladder logic program", 
      "Solid State Interlocking", 
      "design process", 
      "railway interlocking", 
      "formal methods", 
      "industrial design process", 
      "logic programs", 
      "complete methodology", 
      "correctness", 
      "verification", 
      "step", 
      "completeness", 
      "cost", 
      "methodology", 
      "program", 
      "design", 
      "process", 
      "way", 
      "validation", 
      "testing", 
      "method", 
      "railway", 
      "results", 
      "safety", 
      "burden", 
      "interlocking", 
      "cases", 
      "rail", 
      "inclusion"
    ], 
    "name": "Verification of Solid State Interlocking Programs", 
    "pagination": "253-268", 
    "productId": [
      {
        "name": "dimensions_id", 
        "type": "PropertyValue", 
        "value": [
          "pub.1049952676"
        ]
      }, 
      {
        "name": "doi", 
        "type": "PropertyValue", 
        "value": [
          "10.1007/978-3-319-05032-4_19"
        ]
      }
    ], 
    "publisher": {
      "name": "Springer Nature", 
      "type": "Organisation"
    }, 
    "sameAs": [
      "https://doi.org/10.1007/978-3-319-05032-4_19", 
      "https://app.dimensions.ai/details/publication/pub.1049952676"
    ], 
    "sdDataset": "chapters", 
    "sdDatePublished": "2022-05-10T10:46", 
    "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_314.jsonl", 
    "type": "Chapter", 
    "url": "https://doi.org/10.1007/978-3-319-05032-4_19"
  }
]
 

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-319-05032-4_19'

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-319-05032-4_19'

Turtle is a human-readable linked data format.

curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/978-3-319-05032-4_19'

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-319-05032-4_19'


 

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

148 TRIPLES      23 PREDICATES      55 URIs      48 LITERALS      7 BLANK NODES

Subject Predicate Object
1 sg:pub.10.1007/978-3-319-05032-4_19 schema:about anzsrc-for:08
2 anzsrc-for:0803
3 schema:author Nb73bf36602f340b089924aabf020afd7
4 schema:datePublished 2014-03-08
5 schema:datePublishedReg 2014-03-08
6 schema:description We report on the inclusion of a formal method into an industrial design process. Concretely, we suggest carrying out a verification step in railway interlocking design between programming the interlocking and testing this program. Safety still relies on testing, but the burden of guaranteeing completeness and correctness of the validation is in this way greatly reduced. We present a complete methodology for carrying out this verification step in the case of ladder logic programs and give results for real world railway interlockings. As this verification step reduces costs for testing, Invensys Rail is working to include such a verification step into their design process of solid state interlockings.
7 schema:editor N85cc01ff87a344af9031540e373596e2
8 schema:genre chapter
9 schema:inLanguage en
10 schema:isAccessibleForFree true
11 schema:isPartOf N5c813c695e56445aac2412165bcd1d0f
12 schema:keywords Solid State Interlocking
13 burden
14 cases
15 complete methodology
16 completeness
17 correctness
18 cost
19 design
20 design process
21 formal methods
22 inclusion
23 industrial design process
24 interlocking
25 ladder logic program
26 logic programs
27 method
28 methodology
29 process
30 program
31 rail
32 railway
33 railway interlocking
34 results
35 safety
36 step
37 testing
38 validation
39 verification
40 verification step
41 way
42 schema:name Verification of Solid State Interlocking Programs
43 schema:pagination 253-268
44 schema:productId N2458732e700a4fa0ba0585e9200c6d30
45 N3ca916060a7145e5bc54d7b69719f6e4
46 schema:publisher N1df5aac412fe4ccfa87c821ec5e26b2e
47 schema:sameAs https://app.dimensions.ai/details/publication/pub.1049952676
48 https://doi.org/10.1007/978-3-319-05032-4_19
49 schema:sdDatePublished 2022-05-10T10:46
50 schema:sdLicense https://scigraph.springernature.com/explorer/license/
51 schema:sdPublisher N64526f2dda2a46488ebd4be5d067c538
52 schema:url https://doi.org/10.1007/978-3-319-05032-4_19
53 sgo:license sg:explorer/license/
54 sgo:sdDataset chapters
55 rdf:type schema:Chapter
56 N037627aa7baf40a28821b5b57b6921d2 schema:affiliation grid-institutes:grid.4827.9
57 schema:familyName Lawrence
58 schema:givenName Andy
59 rdf:type schema:Person
60 N06e7c676177f4342b2b8604e4366846a rdf:first sg:person.016555714573.74
61 rdf:rest Nbc25f28b6c8a4454afc37a292f2028f2
62 N1df5aac412fe4ccfa87c821ec5e26b2e schema:name Springer Nature
63 rdf:type schema:Organisation
64 N2458732e700a4fa0ba0585e9200c6d30 schema:name dimensions_id
65 schema:value pub.1049952676
66 rdf:type schema:PropertyValue
67 N3ca916060a7145e5bc54d7b69719f6e4 schema:name doi
68 schema:value 10.1007/978-3-319-05032-4_19
69 rdf:type schema:PropertyValue
70 N3d025c7543fd4cb19383dd130e1a33ae schema:familyName Núñez
71 schema:givenName Manuel
72 rdf:type schema:Person
73 N4d317db337fb4d9aa145e5dbdbe263a6 rdf:first sg:person.015333130005.81
74 rdf:rest N06e7c676177f4342b2b8604e4366846a
75 N53139482b94c4802bd716a1e7c1219ec rdf:first N037627aa7baf40a28821b5b57b6921d2
76 rdf:rest Ndd1b4d74474742619c2dd4254ed95152
77 N5c813c695e56445aac2412165bcd1d0f schema:isbn 978-3-319-05031-7
78 978-3-319-05032-4
79 schema:name Software Engineering and Formal Methods
80 rdf:type schema:Book
81 N64526f2dda2a46488ebd4be5d067c538 schema:name Springer Nature - SN SciGraph project
82 rdf:type schema:Organization
83 N85446c1a705b40d9805dec39c837aadf rdf:first N3d025c7543fd4cb19383dd130e1a33ae
84 rdf:rest rdf:nil
85 N85cc01ff87a344af9031540e373596e2 rdf:first N91fdb46a81df4559978a7af32372e2c8
86 rdf:rest N85446c1a705b40d9805dec39c837aadf
87 N91fdb46a81df4559978a7af32372e2c8 schema:familyName Counsell
88 schema:givenName Steve
89 rdf:type schema:Person
90 Nb73bf36602f340b089924aabf020afd7 rdf:first sg:person.012345226005.23
91 rdf:rest N53139482b94c4802bd716a1e7c1219ec
92 Nbc25f28b6c8a4454afc37a292f2028f2 rdf:first sg:person.07425437205.83
93 rdf:rest Nea43e83c695049268b58e8e8cb7e1dca
94 Nd0f329ca38b84c11b1232bff9d7be762 rdf:first sg:person.014634147051.77
95 rdf:rest N4d317db337fb4d9aa145e5dbdbe263a6
96 Ndd1b4d74474742619c2dd4254ed95152 rdf:first sg:person.010425236217.29
97 rdf:rest Nd0f329ca38b84c11b1232bff9d7be762
98 Nea43e83c695049268b58e8e8cb7e1dca rdf:first sg:person.010223017605.64
99 rdf:rest rdf:nil
100 anzsrc-for:08 schema:inDefinedTermSet anzsrc-for:
101 schema:name Information and Computing Sciences
102 rdf:type schema:DefinedTerm
103 anzsrc-for:0803 schema:inDefinedTermSet anzsrc-for:
104 schema:name Computer Software
105 rdf:type schema:DefinedTerm
106 sg:person.010223017605.64 schema:affiliation grid-institutes:None
107 schema:familyName Chadwick
108 schema:givenName Simon
109 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.010223017605.64
110 rdf:type schema:Person
111 sg:person.010425236217.29 schema:affiliation grid-institutes:grid.4827.9
112 schema:familyName Moller
113 schema:givenName Faron
114 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.010425236217.29
115 rdf:type schema:Person
116 sg:person.012345226005.23 schema:affiliation grid-institutes:grid.4827.9
117 schema:familyName James
118 schema:givenName Phillip
119 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.012345226005.23
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 sg:person.015333130005.81 schema:affiliation grid-institutes:grid.4827.9
127 schema:familyName Seisenberger
128 schema:givenName Monika
129 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.015333130005.81
130 rdf:type schema:Person
131 sg:person.016555714573.74 schema:affiliation grid-institutes:grid.4827.9
132 schema:familyName Setzer
133 schema:givenName Anton
134 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.016555714573.74
135 rdf:type schema:Person
136 sg:person.07425437205.83 schema:affiliation grid-institutes:None
137 schema:familyName Kanso
138 schema:givenName Karim
139 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.07425437205.83
140 rdf:type schema:Person
141 grid-institutes:None schema:alternateName Critical Software Technologies, Southampton, England, UK
142 Invensys Rail, Chippenham, England, UK
143 schema:name Critical Software Technologies, Southampton, England, UK
144 Invensys Rail, Chippenham, England, UK
145 rdf:type schema:Organization
146 grid-institutes:grid.4827.9 schema:alternateName Swansea Railway Verification Group, Swansea University, Wales, UK
147 schema:name Swansea Railway Verification Group, Swansea University, Wales, UK
148 rdf:type schema:Organization
 




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


...