Taming Interrupts for Verifying Industrial Multifunction Vehicle Bus Controllers View Full Text


Ontology type: schema:Chapter     


Chapter Info

DATE

2016-11-08

AUTHORS

Han Liu , Yu Jiang , Huafeng Zhang , Ming Gu , Jiaguang Sun

ABSTRACT

Multifunction Vehicle Bus controllers (MVBC) are safety-critical sub-systems in the industrial train communication network. As an interrupt-driven system, MVBC is practically hard to verify. The reasons are twofold. First, MVBC introduces the concurrency semantics of deferred interrupt handlers and communication via hardware registers, making existing formalism infeasible. Second, verifying MVBC requires considering the environmental features (i.e., interrupt ordering), which is hard to model and reason. To overcome these limitations, we proposed a novel framework for formal verification on MVBC. First, we formalized the concurrency semantics of MVBC and described a sequentialization technique so that well-designed sequential analyses can be performed. Moreover, we introduced the happen-before interrupt graph to model interrupt dependency and further eliminate false alarms. The framework scaled well on an industrial MVBC product from CRRC Inc. and found 3 severe software bugs, which were all confirmed by engineers. More... »

PAGES

764-771

Identifiers

URI

http://scigraph.springernature.com/pub.10.1007/978-3-319-48989-6_48

DOI

http://dx.doi.org/10.1007/978-3-319-48989-6_48

DIMENSIONS

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


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": "School of Software, Tsinghua University, Beijing, China", 
          "id": "http://www.grid.ac/institutes/grid.12527.33", 
          "name": [
            "Key Laboratory for Information System Security, Ministry of Education, Beijing, China", 
            "Tsinghua National Laboratory for Information Science and Technology, Beijing, China", 
            "School of Software, Tsinghua University, Beijing, China"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Liu", 
        "givenName": "Han", 
        "id": "sg:person.014236537575.22", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.014236537575.22"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "School of Software, Tsinghua University, Beijing, China", 
          "id": "http://www.grid.ac/institutes/grid.12527.33", 
          "name": [
            "Key Laboratory for Information System Security, Ministry of Education, Beijing, China", 
            "Tsinghua National Laboratory for Information Science and Technology, Beijing, China", 
            "School of Software, Tsinghua University, Beijing, China"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Jiang", 
        "givenName": "Yu", 
        "id": "sg:person.011717277377.60", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011717277377.60"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "School of Software, Tsinghua University, Beijing, China", 
          "id": "http://www.grid.ac/institutes/grid.12527.33", 
          "name": [
            "Key Laboratory for Information System Security, Ministry of Education, Beijing, China", 
            "Tsinghua National Laboratory for Information Science and Technology, Beijing, China", 
            "School of Software, Tsinghua University, Beijing, China"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Zhang", 
        "givenName": "Huafeng", 
        "id": "sg:person.011726700363.09", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011726700363.09"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "China Railway Rolling Stock Corporation (CRRC), Beijing, China", 
          "id": "http://www.grid.ac/institutes/grid.484110.8", 
          "name": [
            "Key Laboratory for Information System Security, Ministry of Education, Beijing, China", 
            "Tsinghua National Laboratory for Information Science and Technology, Beijing, China", 
            "School of Software, Tsinghua University, Beijing, China", 
            "China Railway Rolling Stock Corporation (CRRC), Beijing, China"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Gu", 
        "givenName": "Ming", 
        "id": "sg:person.015646302766.82", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.015646302766.82"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "School of Software, Tsinghua University, Beijing, China", 
          "id": "http://www.grid.ac/institutes/grid.12527.33", 
          "name": [
            "Key Laboratory for Information System Security, Ministry of Education, Beijing, China", 
            "Tsinghua National Laboratory for Information Science and Technology, Beijing, China", 
            "School of Software, Tsinghua University, Beijing, China"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Sun", 
        "givenName": "Jiaguang", 
        "id": "sg:person.011411464635.59", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011411464635.59"
        ], 
        "type": "Person"
      }
    ], 
    "datePublished": "2016-11-08", 
    "datePublishedReg": "2016-11-08", 
    "description": "Multifunction Vehicle Bus controllers (MVBC) are safety-critical sub-systems in the industrial train communication network. As an interrupt-driven system, MVBC is practically hard to verify. The reasons are twofold. First, MVBC introduces the concurrency semantics of deferred interrupt handlers and communication via hardware registers, making existing formalism infeasible. Second, verifying MVBC requires considering the environmental features (i.e., interrupt ordering), which is hard to model and reason. To overcome these limitations, we proposed a novel framework for formal verification on MVBC. First, we formalized the concurrency semantics of MVBC and described a sequentialization technique so that well-designed sequential analyses can be performed. Moreover, we introduced the happen-before interrupt graph to model interrupt dependency and further eliminate false alarms. The framework scaled well on an industrial MVBC product from CRRC Inc. and found 3 severe software bugs, which were all confirmed by engineers.", 
    "editor": [
      {
        "familyName": "Fitzgerald", 
        "givenName": "John", 
        "type": "Person"
      }, 
      {
        "familyName": "Heitmeyer", 
        "givenName": "Constance", 
        "type": "Person"
      }, 
      {
        "familyName": "Gnesi", 
        "givenName": "Stefania", 
        "type": "Person"
      }, 
      {
        "familyName": "Philippou", 
        "givenName": "Anna", 
        "type": "Person"
      }
    ], 
    "genre": "chapter", 
    "id": "sg:pub.10.1007/978-3-319-48989-6_48", 
    "inLanguage": "en", 
    "isAccessibleForFree": false, 
    "isPartOf": {
      "isbn": [
        "978-3-319-48988-9", 
        "978-3-319-48989-6"
      ], 
      "name": "FM 2016: Formal Methods", 
      "type": "Book"
    }, 
    "keywords": [
      "Multifunction Vehicle Bus Controller", 
      "concurrency semantics", 
      "bus controller", 
      "interrupt-driven systems", 
      "Train Communication Network", 
      "formal verification", 
      "software bugs", 
      "sequentialization techniques", 
      "hardware registers", 
      "communication networks", 
      "interrupt handlers", 
      "novel framework", 
      "false alarms", 
      "semantics", 
      "controller", 
      "framework", 
      "interrupts", 
      "network", 
      "graph", 
      "bugs", 
      "verification", 
      "alarms", 
      "communication", 
      "engineers", 
      "handlers", 
      "environmental features", 
      "system", 
      "dependency", 
      "features", 
      "technique", 
      "formalism", 
      "limitations", 
      "Inc.", 
      "reasons", 
      "sequential analysis", 
      "Register", 
      "analysis", 
      "products", 
      "Vehicle Bus controllers", 
      "industrial train communication network", 
      "interrupt graph", 
      "interrupt dependency", 
      "industrial MVBC product", 
      "MVBC product", 
      "CRRC Inc.", 
      "severe software bugs", 
      "Verifying Industrial Multifunction Vehicle Bus Controllers", 
      "Industrial Multifunction Vehicle Bus Controllers"
    ], 
    "name": "Taming Interrupts for Verifying Industrial Multifunction Vehicle Bus Controllers", 
    "pagination": "764-771", 
    "productId": [
      {
        "name": "dimensions_id", 
        "type": "PropertyValue", 
        "value": [
          "pub.1008748752"
        ]
      }, 
      {
        "name": "doi", 
        "type": "PropertyValue", 
        "value": [
          "10.1007/978-3-319-48989-6_48"
        ]
      }
    ], 
    "publisher": {
      "name": "Springer Nature", 
      "type": "Organisation"
    }, 
    "sameAs": [
      "https://doi.org/10.1007/978-3-319-48989-6_48", 
      "https://app.dimensions.ai/details/publication/pub.1008748752"
    ], 
    "sdDataset": "chapters", 
    "sdDatePublished": "2022-01-01T19:27", 
    "sdLicense": "https://scigraph.springernature.com/explorer/license/", 
    "sdPublisher": {
      "name": "Springer Nature - SN SciGraph project", 
      "type": "Organization"
    }, 
    "sdSource": "s3://com-springernature-scigraph/baseset/20220101/entities/gbq_results/chapter/chapter_8.jsonl", 
    "type": "Chapter", 
    "url": "https://doi.org/10.1007/978-3-319-48989-6_48"
  }
]
 

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-48989-6_48'

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-48989-6_48'

Turtle is a human-readable linked data format.

curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/978-3-319-48989-6_48'

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-48989-6_48'


 

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

159 TRIPLES      23 PREDICATES      73 URIs      66 LITERALS      7 BLANK NODES

Subject Predicate Object
1 sg:pub.10.1007/978-3-319-48989-6_48 schema:about anzsrc-for:08
2 anzsrc-for:0803
3 schema:author N9fcc2a949b0b42719707af554fafbe33
4 schema:datePublished 2016-11-08
5 schema:datePublishedReg 2016-11-08
6 schema:description Multifunction Vehicle Bus controllers (MVBC) are safety-critical sub-systems in the industrial train communication network. As an interrupt-driven system, MVBC is practically hard to verify. The reasons are twofold. First, MVBC introduces the concurrency semantics of deferred interrupt handlers and communication via hardware registers, making existing formalism infeasible. Second, verifying MVBC requires considering the environmental features (i.e., interrupt ordering), which is hard to model and reason. To overcome these limitations, we proposed a novel framework for formal verification on MVBC. First, we formalized the concurrency semantics of MVBC and described a sequentialization technique so that well-designed sequential analyses can be performed. Moreover, we introduced the happen-before interrupt graph to model interrupt dependency and further eliminate false alarms. The framework scaled well on an industrial MVBC product from CRRC Inc. and found 3 severe software bugs, which were all confirmed by engineers.
7 schema:editor N18750d1aba494715993b828981adc5af
8 schema:genre chapter
9 schema:inLanguage en
10 schema:isAccessibleForFree false
11 schema:isPartOf N1dfdd52b9e7444698cb60326d861c538
12 schema:keywords CRRC Inc.
13 Inc.
14 Industrial Multifunction Vehicle Bus Controllers
15 MVBC product
16 Multifunction Vehicle Bus Controller
17 Register
18 Train Communication Network
19 Vehicle Bus controllers
20 Verifying Industrial Multifunction Vehicle Bus Controllers
21 alarms
22 analysis
23 bugs
24 bus controller
25 communication
26 communication networks
27 concurrency semantics
28 controller
29 dependency
30 engineers
31 environmental features
32 false alarms
33 features
34 formal verification
35 formalism
36 framework
37 graph
38 handlers
39 hardware registers
40 industrial MVBC product
41 industrial train communication network
42 interrupt dependency
43 interrupt graph
44 interrupt handlers
45 interrupt-driven systems
46 interrupts
47 limitations
48 network
49 novel framework
50 products
51 reasons
52 semantics
53 sequential analysis
54 sequentialization techniques
55 severe software bugs
56 software bugs
57 system
58 technique
59 verification
60 schema:name Taming Interrupts for Verifying Industrial Multifunction Vehicle Bus Controllers
61 schema:pagination 764-771
62 schema:productId N672efd61eaa54965b8fc6264d0d10fa9
63 Nfb8d6a6b62a840d198b9d960de69c6cf
64 schema:publisher N448cbfe19eeb40cc9581047040088015
65 schema:sameAs https://app.dimensions.ai/details/publication/pub.1008748752
66 https://doi.org/10.1007/978-3-319-48989-6_48
67 schema:sdDatePublished 2022-01-01T19:27
68 schema:sdLicense https://scigraph.springernature.com/explorer/license/
69 schema:sdPublisher N30d2d535b95f4096bb3a176538eef718
70 schema:url https://doi.org/10.1007/978-3-319-48989-6_48
71 sgo:license sg:explorer/license/
72 sgo:sdDataset chapters
73 rdf:type schema:Chapter
74 N18750d1aba494715993b828981adc5af rdf:first N7d5b56ef3ff946b8be96f2fc1f8ae3e8
75 rdf:rest N8c42acc3bed94d21b8e63ad2cb70689c
76 N1b90e21bd6e84bdd86a78a92f37e20d2 rdf:first sg:person.015646302766.82
77 rdf:rest N4f65357c1af1404989fc5f1cd5693c4d
78 N1dfdd52b9e7444698cb60326d861c538 schema:isbn 978-3-319-48988-9
79 978-3-319-48989-6
80 schema:name FM 2016: Formal Methods
81 rdf:type schema:Book
82 N30d2d535b95f4096bb3a176538eef718 schema:name Springer Nature - SN SciGraph project
83 rdf:type schema:Organization
84 N341c625ba16f4dc2a82c970a172068e8 rdf:first Naaaba877e77b4a168709d8becd8f1a5a
85 rdf:rest Nfd179d7bacca40e8940e8433434d5705
86 N371c647bc0e74eacbc8a3f5d5589b881 rdf:first sg:person.011726700363.09
87 rdf:rest N1b90e21bd6e84bdd86a78a92f37e20d2
88 N448cbfe19eeb40cc9581047040088015 schema:name Springer Nature
89 rdf:type schema:Organisation
90 N4f65357c1af1404989fc5f1cd5693c4d rdf:first sg:person.011411464635.59
91 rdf:rest rdf:nil
92 N627b775192b84302bd2c233ea17623b9 rdf:first sg:person.011717277377.60
93 rdf:rest N371c647bc0e74eacbc8a3f5d5589b881
94 N672efd61eaa54965b8fc6264d0d10fa9 schema:name dimensions_id
95 schema:value pub.1008748752
96 rdf:type schema:PropertyValue
97 N7d5b56ef3ff946b8be96f2fc1f8ae3e8 schema:familyName Fitzgerald
98 schema:givenName John
99 rdf:type schema:Person
100 N8c42acc3bed94d21b8e63ad2cb70689c rdf:first Naca7db9ddd084d0b8ee129564bfff433
101 rdf:rest N341c625ba16f4dc2a82c970a172068e8
102 N9fcc2a949b0b42719707af554fafbe33 rdf:first sg:person.014236537575.22
103 rdf:rest N627b775192b84302bd2c233ea17623b9
104 Na95191a057f44fdc828b8b49266aed16 schema:familyName Philippou
105 schema:givenName Anna
106 rdf:type schema:Person
107 Naaaba877e77b4a168709d8becd8f1a5a schema:familyName Gnesi
108 schema:givenName Stefania
109 rdf:type schema:Person
110 Naca7db9ddd084d0b8ee129564bfff433 schema:familyName Heitmeyer
111 schema:givenName Constance
112 rdf:type schema:Person
113 Nfb8d6a6b62a840d198b9d960de69c6cf schema:name doi
114 schema:value 10.1007/978-3-319-48989-6_48
115 rdf:type schema:PropertyValue
116 Nfd179d7bacca40e8940e8433434d5705 rdf:first Na95191a057f44fdc828b8b49266aed16
117 rdf:rest rdf:nil
118 anzsrc-for:08 schema:inDefinedTermSet anzsrc-for:
119 schema:name Information and Computing Sciences
120 rdf:type schema:DefinedTerm
121 anzsrc-for:0803 schema:inDefinedTermSet anzsrc-for:
122 schema:name Computer Software
123 rdf:type schema:DefinedTerm
124 sg:person.011411464635.59 schema:affiliation grid-institutes:grid.12527.33
125 schema:familyName Sun
126 schema:givenName Jiaguang
127 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011411464635.59
128 rdf:type schema:Person
129 sg:person.011717277377.60 schema:affiliation grid-institutes:grid.12527.33
130 schema:familyName Jiang
131 schema:givenName Yu
132 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011717277377.60
133 rdf:type schema:Person
134 sg:person.011726700363.09 schema:affiliation grid-institutes:grid.12527.33
135 schema:familyName Zhang
136 schema:givenName Huafeng
137 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011726700363.09
138 rdf:type schema:Person
139 sg:person.014236537575.22 schema:affiliation grid-institutes:grid.12527.33
140 schema:familyName Liu
141 schema:givenName Han
142 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.014236537575.22
143 rdf:type schema:Person
144 sg:person.015646302766.82 schema:affiliation grid-institutes:grid.484110.8
145 schema:familyName Gu
146 schema:givenName Ming
147 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.015646302766.82
148 rdf:type schema:Person
149 grid-institutes:grid.12527.33 schema:alternateName School of Software, Tsinghua University, Beijing, China
150 schema:name Key Laboratory for Information System Security, Ministry of Education, Beijing, China
151 School of Software, Tsinghua University, Beijing, China
152 Tsinghua National Laboratory for Information Science and Technology, Beijing, China
153 rdf:type schema:Organization
154 grid-institutes:grid.484110.8 schema:alternateName China Railway Rolling Stock Corporation (CRRC), Beijing, China
155 schema:name China Railway Rolling Stock Corporation (CRRC), Beijing, China
156 Key Laboratory for Information System Security, Ministry of Education, Beijing, China
157 School of Software, Tsinghua University, Beijing, China
158 Tsinghua National Laboratory for Information Science and Technology, Beijing, China
159 rdf:type schema:Organization
 




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


...