Ontology type: schema:Chapter
2012
AUTHORSJiri Barnat , Jan Beran , Lubos Brim , Tomas Kratochvíla , Petr Ročkai
ABSTRACTEmbedded systems have become an inevitable part of control systems in many industrial domains including avionics. The nature of this domain traditionally requires the highest possible degree of system availability and integrity. While embedded systems have become extremely complex and they have been continuously replacing legacy mechanical components, the amount of defects of hardware and software has to be kept to absolute minimum to avoid casualties and material damages. Despite the above-mentioned facts, significant improvements are still required in the validation and verification processes accompanying embedded systems development. In this paper we report on integration of a parallel, explicit-state LTL model checker (DiVinE) and a tool for requirements-based verification of aerospace system components (HiLiTE, a tool implemented and used by Honeywell). HiLiTE and the proposed partial toolchain use MATLAB Simulink/Stateflow as the primary design language. The work has been conducted within the Artemis project industrial Framework for Embedded Systems Tools (iFEST). More... »
PAGES78-92
Formal Methods for Industrial Critical Systems
ISBN
978-3-642-32468-0
978-3-642-32469-7
http://scigraph.springernature.com/pub.10.1007/978-3-642-32469-7_6
DOIhttp://dx.doi.org/10.1007/978-3-642-32469-7_6
DIMENSIONShttps://app.dimensions.ai/details/publication/pub.1024950309
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/0802",
"inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/",
"name": "Computation Theory and Mathematics",
"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": "Jiri",
"id": "sg:person.011367557177.46",
"sameAs": [
"https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011367557177.46"
],
"type": "Person"
},
{
"affiliation": {
"alternateName": "Honeywell International, Aerospace Advanced Technology Europe, Brno, Czech Republic",
"id": "http://www.grid.ac/institutes/None",
"name": [
"Honeywell International, Aerospace Advanced Technology Europe, Brno, Czech Republic"
],
"type": "Organization"
},
"familyName": "Beran",
"givenName": "Jan",
"id": "sg:person.011412056231.34",
"sameAs": [
"https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011412056231.34"
],
"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": "Lubos",
"id": "sg:person.0645117057.83",
"sameAs": [
"https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.0645117057.83"
],
"type": "Person"
},
{
"affiliation": {
"alternateName": "Honeywell International, Aerospace Advanced Technology Europe, Brno, Czech Republic",
"id": "http://www.grid.ac/institutes/None",
"name": [
"Honeywell International, Aerospace Advanced Technology Europe, Brno, Czech Republic"
],
"type": "Organization"
},
"familyName": "Kratochv\u00edla",
"givenName": "Tomas",
"id": "sg:person.012207436631.09",
"sameAs": [
"https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.012207436631.09"
],
"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": "Petr",
"id": "sg:person.07377571657.86",
"sameAs": [
"https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.07377571657.86"
],
"type": "Person"
}
],
"datePublished": "2012",
"datePublishedReg": "2012-01-01",
"description": "Embedded systems have become an inevitable part of control systems in many industrial domains including avionics. The nature of this domain traditionally requires the highest possible degree of system availability and integrity. While embedded systems have become extremely complex and they have been continuously replacing legacy mechanical components, the amount of defects of hardware and software has to be kept to absolute minimum to avoid casualties and material damages. Despite the above-mentioned facts, significant improvements are still required in the validation and verification processes accompanying embedded systems development. In this paper we report on integration of a parallel, explicit-state LTL model checker (DiVinE) and a tool for requirements-based verification of aerospace system components (HiLiTE, a tool implemented and used by Honeywell). HiLiTE and the proposed partial toolchain use MATLAB Simulink/Stateflow as the primary design language. The work has been conducted within the Artemis project industrial Framework for Embedded Systems Tools (iFEST).",
"editor": [
{
"familyName": "Stoelinga",
"givenName": "Mari\u00eblle",
"type": "Person"
},
{
"familyName": "Pinger",
"givenName": "Ralf",
"type": "Person"
}
],
"genre": "chapter",
"id": "sg:pub.10.1007/978-3-642-32469-7_6",
"inLanguage": "en",
"isAccessibleForFree": false,
"isPartOf": {
"isbn": [
"978-3-642-32468-0",
"978-3-642-32469-7"
],
"name": "Formal Methods for Industrial Critical Systems",
"type": "Book"
},
"keywords": [
"MATLAB Simulink/Stateflow",
"embedded system development",
"embedded systems tools",
"LTL model checker",
"Simulink/Stateflow",
"formal verification",
"tool chain",
"model checker",
"industrial domains",
"verification process",
"design language",
"system tools",
"system development",
"system availability",
"Simulink design",
"industrial framework",
"system components",
"control system",
"highest possible degree",
"aerospace system components",
"verification",
"inevitable part",
"checker",
"hardware",
"Stateflow",
"avionics",
"software",
"system",
"tool",
"mechanical components",
"language",
"domain",
"possible degree",
"framework",
"significant improvement",
"integration",
"HiLite",
"design",
"validation",
"work",
"availability",
"components",
"improvement",
"process",
"integrity",
"amount",
"part",
"development",
"fact",
"casualties",
"nature",
"minimum",
"chain",
"degree",
"material damage",
"defects",
"amount of defects",
"damage",
"paper"
],
"name": "Tool Chain to Support Automated Formal Verification of Avionics Simulink Designs",
"pagination": "78-92",
"productId": [
{
"name": "dimensions_id",
"type": "PropertyValue",
"value": [
"pub.1024950309"
]
},
{
"name": "doi",
"type": "PropertyValue",
"value": [
"10.1007/978-3-642-32469-7_6"
]
}
],
"publisher": {
"name": "Springer Nature",
"type": "Organisation"
},
"sameAs": [
"https://doi.org/10.1007/978-3-642-32469-7_6",
"https://app.dimensions.ai/details/publication/pub.1024950309"
],
"sdDataset": "chapters",
"sdDatePublished": "2022-05-20T07:48",
"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_442.jsonl",
"type": "Chapter",
"url": "https://doi.org/10.1007/978-3-642-32469-7_6"
}
]
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/978-3-642-32469-7_6'
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-32469-7_6'
Turtle is a human-readable linked data format.
curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/978-3-642-32469-7_6'
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-32469-7_6'
This table displays all metadata directly associated to this object as RDF triples.
159 TRIPLES
23 PREDICATES
86 URIs
78 LITERALS
7 BLANK NODES
Subject | Predicate | Object | |
---|---|---|---|
1 | sg:pub.10.1007/978-3-642-32469-7_6 | schema:about | anzsrc-for:08 |
2 | ″ | ″ | anzsrc-for:0802 |
3 | ″ | ″ | anzsrc-for:0803 |
4 | ″ | schema:author | N2d2b28e691d74dff85e2226f3f9eb164 |
5 | ″ | schema:datePublished | 2012 |
6 | ″ | schema:datePublishedReg | 2012-01-01 |
7 | ″ | schema:description | Embedded systems have become an inevitable part of control systems in many industrial domains including avionics. The nature of this domain traditionally requires the highest possible degree of system availability and integrity. While embedded systems have become extremely complex and they have been continuously replacing legacy mechanical components, the amount of defects of hardware and software has to be kept to absolute minimum to avoid casualties and material damages. Despite the above-mentioned facts, significant improvements are still required in the validation and verification processes accompanying embedded systems development. In this paper we report on integration of a parallel, explicit-state LTL model checker (DiVinE) and a tool for requirements-based verification of aerospace system components (HiLiTE, a tool implemented and used by Honeywell). HiLiTE and the proposed partial toolchain use MATLAB Simulink/Stateflow as the primary design language. The work has been conducted within the Artemis project industrial Framework for Embedded Systems Tools (iFEST). |
8 | ″ | schema:editor | Nad3eb07f910c42fe968937bf5b976aeb |
9 | ″ | schema:genre | chapter |
10 | ″ | schema:inLanguage | en |
11 | ″ | schema:isAccessibleForFree | false |
12 | ″ | schema:isPartOf | N03420d5119b0410fb6c1070e4dc35693 |
13 | ″ | schema:keywords | HiLite |
14 | ″ | ″ | LTL model checker |
15 | ″ | ″ | MATLAB Simulink/Stateflow |
16 | ″ | ″ | Simulink design |
17 | ″ | ″ | Simulink/Stateflow |
18 | ″ | ″ | Stateflow |
19 | ″ | ″ | aerospace system components |
20 | ″ | ″ | amount |
21 | ″ | ″ | amount of defects |
22 | ″ | ″ | availability |
23 | ″ | ″ | avionics |
24 | ″ | ″ | casualties |
25 | ″ | ″ | chain |
26 | ″ | ″ | checker |
27 | ″ | ″ | components |
28 | ″ | ″ | control system |
29 | ″ | ″ | damage |
30 | ″ | ″ | defects |
31 | ″ | ″ | degree |
32 | ″ | ″ | design |
33 | ″ | ″ | design language |
34 | ″ | ″ | development |
35 | ″ | ″ | domain |
36 | ″ | ″ | embedded system development |
37 | ″ | ″ | embedded systems tools |
38 | ″ | ″ | fact |
39 | ″ | ″ | formal verification |
40 | ″ | ″ | framework |
41 | ″ | ″ | hardware |
42 | ″ | ″ | highest possible degree |
43 | ″ | ″ | improvement |
44 | ″ | ″ | industrial domains |
45 | ″ | ″ | industrial framework |
46 | ″ | ″ | inevitable part |
47 | ″ | ″ | integration |
48 | ″ | ″ | integrity |
49 | ″ | ″ | language |
50 | ″ | ″ | material damage |
51 | ″ | ″ | mechanical components |
52 | ″ | ″ | minimum |
53 | ″ | ″ | model checker |
54 | ″ | ″ | nature |
55 | ″ | ″ | paper |
56 | ″ | ″ | part |
57 | ″ | ″ | possible degree |
58 | ″ | ″ | process |
59 | ″ | ″ | significant improvement |
60 | ″ | ″ | software |
61 | ″ | ″ | system |
62 | ″ | ″ | system availability |
63 | ″ | ″ | system components |
64 | ″ | ″ | system development |
65 | ″ | ″ | system tools |
66 | ″ | ″ | tool |
67 | ″ | ″ | tool chain |
68 | ″ | ″ | validation |
69 | ″ | ″ | verification |
70 | ″ | ″ | verification process |
71 | ″ | ″ | work |
72 | ″ | schema:name | Tool Chain to Support Automated Formal Verification of Avionics Simulink Designs |
73 | ″ | schema:pagination | 78-92 |
74 | ″ | schema:productId | N9cb117c34c7040e0a8eab5db418a313c |
75 | ″ | ″ | Na90228423ba24beab39669333a5a9373 |
76 | ″ | schema:publisher | Na28be3494a0e443daf09ad142503f42f |
77 | ″ | schema:sameAs | https://app.dimensions.ai/details/publication/pub.1024950309 |
78 | ″ | ″ | https://doi.org/10.1007/978-3-642-32469-7_6 |
79 | ″ | schema:sdDatePublished | 2022-05-20T07:48 |
80 | ″ | schema:sdLicense | https://scigraph.springernature.com/explorer/license/ |
81 | ″ | schema:sdPublisher | N969fb8d519494d7aaeff32f61749c8e8 |
82 | ″ | schema:url | https://doi.org/10.1007/978-3-642-32469-7_6 |
83 | ″ | sgo:license | sg:explorer/license/ |
84 | ″ | sgo:sdDataset | chapters |
85 | ″ | rdf:type | schema:Chapter |
86 | N03420d5119b0410fb6c1070e4dc35693 | schema:isbn | 978-3-642-32468-0 |
87 | ″ | ″ | 978-3-642-32469-7 |
88 | ″ | schema:name | Formal Methods for Industrial Critical Systems |
89 | ″ | rdf:type | schema:Book |
90 | N050cb0910a7d43418249bb9f5a43c69a | rdf:first | sg:person.0645117057.83 |
91 | ″ | rdf:rest | N979eb74847a6427ebada38727f30cc61 |
92 | N13b82f8e67454326b009db41caafab29 | rdf:first | sg:person.07377571657.86 |
93 | ″ | rdf:rest | rdf:nil |
94 | N2d2b28e691d74dff85e2226f3f9eb164 | rdf:first | sg:person.011367557177.46 |
95 | ″ | rdf:rest | Nc4902c4e7f5c454381b48c64a196a747 |
96 | N53afa3a065d34d0c94bf7693bffe9ac5 | schema:familyName | Pinger |
97 | ″ | schema:givenName | Ralf |
98 | ″ | rdf:type | schema:Person |
99 | N969fb8d519494d7aaeff32f61749c8e8 | schema:name | Springer Nature - SN SciGraph project |
100 | ″ | rdf:type | schema:Organization |
101 | N979eb74847a6427ebada38727f30cc61 | rdf:first | sg:person.012207436631.09 |
102 | ″ | rdf:rest | N13b82f8e67454326b009db41caafab29 |
103 | N9cb117c34c7040e0a8eab5db418a313c | schema:name | doi |
104 | ″ | schema:value | 10.1007/978-3-642-32469-7_6 |
105 | ″ | rdf:type | schema:PropertyValue |
106 | Na28be3494a0e443daf09ad142503f42f | schema:name | Springer Nature |
107 | ″ | rdf:type | schema:Organisation |
108 | Na90228423ba24beab39669333a5a9373 | schema:name | dimensions_id |
109 | ″ | schema:value | pub.1024950309 |
110 | ″ | rdf:type | schema:PropertyValue |
111 | Nac71c4f810844d7f9706fb090f1a8a68 | schema:familyName | Stoelinga |
112 | ″ | schema:givenName | Mariëlle |
113 | ″ | rdf:type | schema:Person |
114 | Nad3eb07f910c42fe968937bf5b976aeb | rdf:first | Nac71c4f810844d7f9706fb090f1a8a68 |
115 | ″ | rdf:rest | Ne5ff0983a3b842b9ae61b82ebf794078 |
116 | Nc4902c4e7f5c454381b48c64a196a747 | rdf:first | sg:person.011412056231.34 |
117 | ″ | rdf:rest | N050cb0910a7d43418249bb9f5a43c69a |
118 | Ne5ff0983a3b842b9ae61b82ebf794078 | rdf:first | N53afa3a065d34d0c94bf7693bffe9ac5 |
119 | ″ | rdf:rest | rdf:nil |
120 | anzsrc-for:08 | schema:inDefinedTermSet | anzsrc-for: |
121 | ″ | schema:name | Information and Computing Sciences |
122 | ″ | rdf:type | schema:DefinedTerm |
123 | anzsrc-for:0802 | schema:inDefinedTermSet | anzsrc-for: |
124 | ″ | schema:name | Computation Theory and Mathematics |
125 | ″ | rdf:type | schema:DefinedTerm |
126 | anzsrc-for:0803 | schema:inDefinedTermSet | anzsrc-for: |
127 | ″ | schema:name | Computer Software |
128 | ″ | rdf:type | schema:DefinedTerm |
129 | sg:person.011367557177.46 | schema:affiliation | grid-institutes:grid.10267.32 |
130 | ″ | schema:familyName | Barnat |
131 | ″ | schema:givenName | Jiri |
132 | ″ | schema:sameAs | https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011367557177.46 |
133 | ″ | rdf:type | schema:Person |
134 | sg:person.011412056231.34 | schema:affiliation | grid-institutes:None |
135 | ″ | schema:familyName | Beran |
136 | ″ | schema:givenName | Jan |
137 | ″ | schema:sameAs | https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011412056231.34 |
138 | ″ | rdf:type | schema:Person |
139 | sg:person.012207436631.09 | schema:affiliation | grid-institutes:None |
140 | ″ | schema:familyName | Kratochvíla |
141 | ″ | schema:givenName | Tomas |
142 | ″ | schema:sameAs | https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.012207436631.09 |
143 | ″ | rdf:type | schema:Person |
144 | sg:person.0645117057.83 | schema:affiliation | grid-institutes:grid.10267.32 |
145 | ″ | schema:familyName | Brim |
146 | ″ | schema:givenName | Lubos |
147 | ″ | schema:sameAs | https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.0645117057.83 |
148 | ″ | rdf:type | schema:Person |
149 | sg:person.07377571657.86 | schema:affiliation | grid-institutes:grid.10267.32 |
150 | ″ | schema:familyName | Ročkai |
151 | ″ | schema:givenName | Petr |
152 | ″ | schema:sameAs | https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.07377571657.86 |
153 | ″ | rdf:type | schema:Person |
154 | grid-institutes:None | schema:alternateName | Honeywell International, Aerospace Advanced Technology Europe, Brno, Czech Republic |
155 | ″ | schema:name | Honeywell International, Aerospace Advanced Technology Europe, Brno, Czech Republic |
156 | ″ | rdf:type | schema:Organization |
157 | grid-institutes:grid.10267.32 | schema:alternateName | Faculty of Informatics, Masaryk University, Brno, Czech Republic |
158 | ″ | schema:name | Faculty of Informatics, Masaryk University, Brno, Czech Republic |
159 | ″ | rdf:type | schema:Organization |