Tool Chain to Support Automated Formal Verification of Avionics Simulink Designs View Full Text


Ontology type: schema:Chapter     


Chapter Info

DATE

2012

AUTHORS

Jiri Barnat , Jan Beran , Lubos Brim , Tomas Kratochvíla , Petr Ročkai

ABSTRACT

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). More... »

PAGES

78-92

Identifiers

URI

http://scigraph.springernature.com/pub.10.1007/978-3-642-32469-7_6

DOI

http://dx.doi.org/10.1007/978-3-642-32469-7_6

DIMENSIONS

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


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/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

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




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


...