Safety-Assured Formal Model-Driven Design of the Multifunction Vehicle Bus Controller View Full Text


Ontology type: schema:Chapter      Open Access: True


Chapter Info

DATE

2016-11-08

AUTHORS

Yu Jiang , Han Liu , Houbing Song , Hui Kong , Ming Gu , Jiaguang Sun , Lui Sha

ABSTRACT

In this paper, we present a formal model-driven engineering approach to establishing a safety-assured implementation of Multifunction vehicle bus controller (MVBC) based on the generic reference models and requirements described in the International Electrotechnical Commission (IEC) standard IEC-61375. First, the generic models described in IEC-61375 are translated into a network of timed automata, and some safety requirements tested in IEC-61375 are formalized as timed computation tree logic (TCTL) formulas. With the help of Uppaal, we check and debug whether the timed automata satisfy the formulas or not. Within this step, several logic inconsistencies in the original standard are detected and corrected. Then, we apply the tool Times to generate C code from the verified model, which was later synthesized into a real MVBC chip. Finally, the runtime verification tool RMOR is applied to verify some safety requirements at the implementation level. We set up a real platform with worldwide mostly used MVBC D113, and verify the correctness and the scalability of the synthesized MVBC chip more comprehensively. The errors in the standard has been confirmed and the resulted MVBC has been deployed in real train communication network. More... »

PAGES

757-763

Identifiers

URI

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

DOI

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

DIMENSIONS

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


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": "TNLIST, KLISS, School of Software, Tsinghua University, Beijing, China", 
          "id": "http://www.grid.ac/institutes/grid.12527.33", 
          "name": [
            "TNLIST, KLISS, 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": "TNLIST, KLISS, School of Software, Tsinghua University, Beijing, China", 
          "id": "http://www.grid.ac/institutes/grid.12527.33", 
          "name": [
            "TNLIST, KLISS, 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": "Department of Electrical and Computer Engineering, West Virginia University, Morgantown, USA", 
          "id": "http://www.grid.ac/institutes/grid.268154.c", 
          "name": [
            "Department of Electrical and Computer Engineering, West Virginia University, Morgantown, USA"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Song", 
        "givenName": "Houbing", 
        "id": "sg:person.014653416425.46", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.014653416425.46"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "Institute of Science and Technology Austria, Klosterneuburg, Austria", 
          "id": "http://www.grid.ac/institutes/grid.33565.36", 
          "name": [
            "Institute of Science and Technology Austria, Klosterneuburg, Austria"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Kong", 
        "givenName": "Hui", 
        "id": "sg:person.014714203123.91", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.014714203123.91"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "TNLIST, KLISS, School of Software, Tsinghua University, Beijing, China", 
          "id": "http://www.grid.ac/institutes/grid.12527.33", 
          "name": [
            "TNLIST, KLISS, School of Software, Tsinghua University, 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": "TNLIST, KLISS, School of Software, Tsinghua University, Beijing, China", 
          "id": "http://www.grid.ac/institutes/grid.12527.33", 
          "name": [
            "TNLIST, KLISS, 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"
      }, 
      {
        "affiliation": {
          "alternateName": "Department of Computer Science, UIUC, Champaign, USA", 
          "id": "http://www.grid.ac/institutes/grid.35403.31", 
          "name": [
            "Department of Computer Science, UIUC, Champaign, USA"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Sha", 
        "givenName": "Lui", 
        "id": "sg:person.01242454134.87", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.01242454134.87"
        ], 
        "type": "Person"
      }
    ], 
    "datePublished": "2016-11-08", 
    "datePublishedReg": "2016-11-08", 
    "description": "In this paper, we present a formal model-driven engineering approach to establishing a safety-assured implementation of Multifunction vehicle bus controller (MVBC) based on the generic reference models and requirements described in the International Electrotechnical Commission (IEC) standard IEC-61375. First, the generic models described in IEC-61375 are translated into a network of timed automata, and some safety requirements tested in IEC-61375 are formalized as timed computation tree logic (TCTL) formulas. With the help of Uppaal, we check and debug whether the timed automata satisfy the formulas or not. Within this step, several logic inconsistencies in the original standard are detected and corrected. Then, we apply the tool Times to generate C code from the verified model, which was later synthesized into a real MVBC chip. Finally, the runtime verification tool RMOR is applied to verify some safety requirements at the implementation level. We set up a real platform with worldwide mostly used MVBC D113, and verify the correctness and the scalability of the synthesized MVBC chip more comprehensively. The errors in the standard has been confirmed and the resulted MVBC has been deployed in real train communication network.", 
    "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_47", 
    "inLanguage": "en", 
    "isAccessibleForFree": true, 
    "isPartOf": {
      "isbn": [
        "978-3-319-48988-9", 
        "978-3-319-48989-6"
      ], 
      "name": "FM 2016: Formal Methods", 
      "type": "Book"
    }, 
    "keywords": [
      "Multifunction Vehicle Bus Controller", 
      "model-driven engineering approach", 
      "Model-Driven Design", 
      "bus controller", 
      "computation tree logic formulas", 
      "Train Communication Network", 
      "generic reference model", 
      "safety requirements", 
      "real platform", 
      "logic formulas", 
      "communication networks", 
      "Timed Automata", 
      "tool time", 
      "implementation level", 
      "reference model", 
      "generic model", 
      "engineering approach", 
      "original standard", 
      "network", 
      "requirements", 
      "automata", 
      "controller", 
      "UPPAAL", 
      "scalability", 
      "correctness", 
      "platform", 
      "implementation", 
      "verified model", 
      "chip", 
      "RMOR", 
      "code", 
      "standards", 
      "model", 
      "error", 
      "design", 
      "help", 
      "inconsistencies", 
      "step", 
      "time", 
      "formula", 
      "D113", 
      "levels", 
      "paper", 
      "approach", 
      "formal model-driven engineering approach", 
      "safety-assured implementation", 
      "vehicle bus controller", 
      "International Electrotechnical Commission (IEC) standard IEC-61375", 
      "Electrotechnical Commission (IEC) standard IEC-61375", 
      "Commission (IEC) standard IEC-61375", 
      "standard IEC-61375", 
      "IEC-61375", 
      "tree logic (TCTL) formulas", 
      "help of Uppaal", 
      "logic inconsistencies", 
      "real MVBC chip", 
      "MVBC chip", 
      "runtime verification tool RMOR", 
      "verification tool RMOR", 
      "tool RMOR", 
      "MVBC D113", 
      "synthesized MVBC chip", 
      "real train communication network", 
      "Safety-Assured Formal Model-Driven Design", 
      "Formal Model-Driven Design"
    ], 
    "name": "Safety-Assured Formal Model-Driven Design of the Multifunction Vehicle Bus Controller", 
    "pagination": "757-763", 
    "productId": [
      {
        "name": "dimensions_id", 
        "type": "PropertyValue", 
        "value": [
          "pub.1047400220"
        ]
      }, 
      {
        "name": "doi", 
        "type": "PropertyValue", 
        "value": [
          "10.1007/978-3-319-48989-6_47"
        ]
      }
    ], 
    "publisher": {
      "name": "Springer Nature", 
      "type": "Organisation"
    }, 
    "sameAs": [
      "https://doi.org/10.1007/978-3-319-48989-6_47", 
      "https://app.dimensions.ai/details/publication/pub.1047400220"
    ], 
    "sdDataset": "chapters", 
    "sdDatePublished": "2022-01-01T19:28", 
    "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_85.jsonl", 
    "type": "Chapter", 
    "url": "https://doi.org/10.1007/978-3-319-48989-6_47"
  }
]
 

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_47'

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_47'

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_47'

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_47'


 

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

191 TRIPLES      23 PREDICATES      90 URIs      83 LITERALS      7 BLANK NODES

Subject Predicate Object
1 sg:pub.10.1007/978-3-319-48989-6_47 schema:about anzsrc-for:08
2 anzsrc-for:0803
3 schema:author N6be0fb6e91bf427d8bd4498426c2425c
4 schema:datePublished 2016-11-08
5 schema:datePublishedReg 2016-11-08
6 schema:description In this paper, we present a formal model-driven engineering approach to establishing a safety-assured implementation of Multifunction vehicle bus controller (MVBC) based on the generic reference models and requirements described in the International Electrotechnical Commission (IEC) standard IEC-61375. First, the generic models described in IEC-61375 are translated into a network of timed automata, and some safety requirements tested in IEC-61375 are formalized as timed computation tree logic (TCTL) formulas. With the help of Uppaal, we check and debug whether the timed automata satisfy the formulas or not. Within this step, several logic inconsistencies in the original standard are detected and corrected. Then, we apply the tool Times to generate C code from the verified model, which was later synthesized into a real MVBC chip. Finally, the runtime verification tool RMOR is applied to verify some safety requirements at the implementation level. We set up a real platform with worldwide mostly used MVBC D113, and verify the correctness and the scalability of the synthesized MVBC chip more comprehensively. The errors in the standard has been confirmed and the resulted MVBC has been deployed in real train communication network.
7 schema:editor N911459ed91da4c7d9610e1d6ce8a2b67
8 schema:genre chapter
9 schema:inLanguage en
10 schema:isAccessibleForFree true
11 schema:isPartOf N5ee6fd09257a41f29419a3b0c736c88b
12 schema:keywords Commission (IEC) standard IEC-61375
13 D113
14 Electrotechnical Commission (IEC) standard IEC-61375
15 Formal Model-Driven Design
16 IEC-61375
17 International Electrotechnical Commission (IEC) standard IEC-61375
18 MVBC D113
19 MVBC chip
20 Model-Driven Design
21 Multifunction Vehicle Bus Controller
22 RMOR
23 Safety-Assured Formal Model-Driven Design
24 Timed Automata
25 Train Communication Network
26 UPPAAL
27 approach
28 automata
29 bus controller
30 chip
31 code
32 communication networks
33 computation tree logic formulas
34 controller
35 correctness
36 design
37 engineering approach
38 error
39 formal model-driven engineering approach
40 formula
41 generic model
42 generic reference model
43 help
44 help of Uppaal
45 implementation
46 implementation level
47 inconsistencies
48 levels
49 logic formulas
50 logic inconsistencies
51 model
52 model-driven engineering approach
53 network
54 original standard
55 paper
56 platform
57 real MVBC chip
58 real platform
59 real train communication network
60 reference model
61 requirements
62 runtime verification tool RMOR
63 safety requirements
64 safety-assured implementation
65 scalability
66 standard IEC-61375
67 standards
68 step
69 synthesized MVBC chip
70 time
71 tool RMOR
72 tool time
73 tree logic (TCTL) formulas
74 vehicle bus controller
75 verification tool RMOR
76 verified model
77 schema:name Safety-Assured Formal Model-Driven Design of the Multifunction Vehicle Bus Controller
78 schema:pagination 757-763
79 schema:productId N60035218d4574b96bb4aca11b1083b98
80 N751c56d405d142769bc8e6610b8c9f5d
81 schema:publisher Nc089f1528fe84cd292356ae1d2b1cc1f
82 schema:sameAs https://app.dimensions.ai/details/publication/pub.1047400220
83 https://doi.org/10.1007/978-3-319-48989-6_47
84 schema:sdDatePublished 2022-01-01T19:28
85 schema:sdLicense https://scigraph.springernature.com/explorer/license/
86 schema:sdPublisher Nfadb887f976f423788271c59acd536fd
87 schema:url https://doi.org/10.1007/978-3-319-48989-6_47
88 sgo:license sg:explorer/license/
89 sgo:sdDataset chapters
90 rdf:type schema:Chapter
91 N3abe7993b5a34d9cb9db6b91f7f1fad2 schema:familyName Philippou
92 schema:givenName Anna
93 rdf:type schema:Person
94 N4831e5b10f3a4cd9a35bccd7ba00d1d6 rdf:first sg:person.014236537575.22
95 rdf:rest Nfc49fab9034b43d099acfd97e536d171
96 N57c630c910724bc5a7ca19f89eacc121 schema:familyName Fitzgerald
97 schema:givenName John
98 rdf:type schema:Person
99 N5ee6fd09257a41f29419a3b0c736c88b schema:isbn 978-3-319-48988-9
100 978-3-319-48989-6
101 schema:name FM 2016: Formal Methods
102 rdf:type schema:Book
103 N60035218d4574b96bb4aca11b1083b98 schema:name doi
104 schema:value 10.1007/978-3-319-48989-6_47
105 rdf:type schema:PropertyValue
106 N6be0fb6e91bf427d8bd4498426c2425c rdf:first sg:person.011717277377.60
107 rdf:rest N4831e5b10f3a4cd9a35bccd7ba00d1d6
108 N751c56d405d142769bc8e6610b8c9f5d schema:name dimensions_id
109 schema:value pub.1047400220
110 rdf:type schema:PropertyValue
111 N86177d3fda4846e9ab5599565fa34266 rdf:first sg:person.01242454134.87
112 rdf:rest rdf:nil
113 N911459ed91da4c7d9610e1d6ce8a2b67 rdf:first N57c630c910724bc5a7ca19f89eacc121
114 rdf:rest Nc8fa38c734e94aa2a028498762087886
115 N978962ece17b4da0ae40f058ef330f1a rdf:first N3abe7993b5a34d9cb9db6b91f7f1fad2
116 rdf:rest rdf:nil
117 Nb3e53bb175b04b8ebca995c896d257b9 rdf:first sg:person.014714203123.91
118 rdf:rest Nfac2dfdb4a494f5c8233e6f1fd866208
119 Nb9574216435743d0bf28fdf67535dbb3 schema:familyName Heitmeyer
120 schema:givenName Constance
121 rdf:type schema:Person
122 Nbc33e85743924566a7e55b57131ab4bb schema:familyName Gnesi
123 schema:givenName Stefania
124 rdf:type schema:Person
125 Nc089f1528fe84cd292356ae1d2b1cc1f schema:name Springer Nature
126 rdf:type schema:Organisation
127 Nc8fa38c734e94aa2a028498762087886 rdf:first Nb9574216435743d0bf28fdf67535dbb3
128 rdf:rest Nf5005d49918d47df8b85eaf8ea52f3b2
129 Nf5005d49918d47df8b85eaf8ea52f3b2 rdf:first Nbc33e85743924566a7e55b57131ab4bb
130 rdf:rest N978962ece17b4da0ae40f058ef330f1a
131 Nf6ff170a480042eaa48832e28d32554d rdf:first sg:person.011411464635.59
132 rdf:rest N86177d3fda4846e9ab5599565fa34266
133 Nfac2dfdb4a494f5c8233e6f1fd866208 rdf:first sg:person.015646302766.82
134 rdf:rest Nf6ff170a480042eaa48832e28d32554d
135 Nfadb887f976f423788271c59acd536fd schema:name Springer Nature - SN SciGraph project
136 rdf:type schema:Organization
137 Nfc49fab9034b43d099acfd97e536d171 rdf:first sg:person.014653416425.46
138 rdf:rest Nb3e53bb175b04b8ebca995c896d257b9
139 anzsrc-for:08 schema:inDefinedTermSet anzsrc-for:
140 schema:name Information and Computing Sciences
141 rdf:type schema:DefinedTerm
142 anzsrc-for:0803 schema:inDefinedTermSet anzsrc-for:
143 schema:name Computer Software
144 rdf:type schema:DefinedTerm
145 sg:person.011411464635.59 schema:affiliation grid-institutes:grid.12527.33
146 schema:familyName Sun
147 schema:givenName Jiaguang
148 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011411464635.59
149 rdf:type schema:Person
150 sg:person.011717277377.60 schema:affiliation grid-institutes:grid.12527.33
151 schema:familyName Jiang
152 schema:givenName Yu
153 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011717277377.60
154 rdf:type schema:Person
155 sg:person.01242454134.87 schema:affiliation grid-institutes:grid.35403.31
156 schema:familyName Sha
157 schema:givenName Lui
158 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.01242454134.87
159 rdf:type schema:Person
160 sg:person.014236537575.22 schema:affiliation grid-institutes:grid.12527.33
161 schema:familyName Liu
162 schema:givenName Han
163 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.014236537575.22
164 rdf:type schema:Person
165 sg:person.014653416425.46 schema:affiliation grid-institutes:grid.268154.c
166 schema:familyName Song
167 schema:givenName Houbing
168 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.014653416425.46
169 rdf:type schema:Person
170 sg:person.014714203123.91 schema:affiliation grid-institutes:grid.33565.36
171 schema:familyName Kong
172 schema:givenName Hui
173 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.014714203123.91
174 rdf:type schema:Person
175 sg:person.015646302766.82 schema:affiliation grid-institutes:grid.12527.33
176 schema:familyName Gu
177 schema:givenName Ming
178 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.015646302766.82
179 rdf:type schema:Person
180 grid-institutes:grid.12527.33 schema:alternateName TNLIST, KLISS, School of Software, Tsinghua University, Beijing, China
181 schema:name TNLIST, KLISS, School of Software, Tsinghua University, Beijing, China
182 rdf:type schema:Organization
183 grid-institutes:grid.268154.c schema:alternateName Department of Electrical and Computer Engineering, West Virginia University, Morgantown, USA
184 schema:name Department of Electrical and Computer Engineering, West Virginia University, Morgantown, USA
185 rdf:type schema:Organization
186 grid-institutes:grid.33565.36 schema:alternateName Institute of Science and Technology Austria, Klosterneuburg, Austria
187 schema:name Institute of Science and Technology Austria, Klosterneuburg, Austria
188 rdf:type schema:Organization
189 grid-institutes:grid.35403.31 schema:alternateName Department of Computer Science, UIUC, Champaign, USA
190 schema:name Department of Computer Science, UIUC, Champaign, USA
191 rdf:type schema:Organization
 




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


...