Scipediacontent: Scipediacontent moved page Draft Content 755838517 to Taha et al 2018a

2021-01-28T17:23:22Z

Scipediacontent moved page Draft Content 755838517 to Taha et al 2018a

Scipediacontent: Created page with " == Abstract == International audience; The ever-increasing complexity of automotive embedded systems and the need for safe advanced driver assistance systems (ADAS) represen..."

2021-01-28T17:23:19Z

Created page with " == Abstract == International audience; The ever-increasing complexity of automotive embedded systems and the need for safe advanced driver assistance systems (ADAS) represen..."

New page

== Abstract ==

International audience; The ever-increasing complexity of automotive embedded systems and the need for safe advanced driver assistance systems (ADAS) represent a great challenge for car manufacturers. Furthermore, we expect that in the near future, authorities require a software certification in order to get convinced that ADAS are safe enough. Theoretical research and experience show that when using conventional design approaches it is impossible to guarantee high confidence to those systems. The way taken by some industries (e.g. aerospace, railway, nuclear) was by partially using formal verification techniques. In this paper, we first present a background of the formal verification techniques and how they can contribute to achieve the requirements of some safety standards. Next, we share our experience with the application of those techniques that seem to be mature enough to be used in an industrial context: Static analysis based on Abstract Interpretation, SMT-based software Model checking and Deductive proof. Finally, we make a detailed analysis about our experiments and propose an approach introducing formal methods into the development of automotive embedded software. CCS CONCEPTS • Software and its engineering → Software verification; KEYWORDS Software verification · Formal methods · ADAS · Certification ACM Reference Format: Vassil Todorov, Frédéric Boulanger, and Safouan Taha. 2018. Formal verification of automotive embedded software. In FormaliSE '18: FormaliSE

== Original document ==

The different versions of the original document can be found in:

* [https://hal.archives-ouvertes.fr/hal-01768687/file/article-auteur.pdf https://hal.archives-ouvertes.fr/hal-01768687/file/article-auteur.pdf]

* [http://dl.acm.org/ft_gateway.cfm?id=3194003&ftid=1988632&dwn=1 http://dl.acm.org/ft_gateway.cfm?id=3194003&ftid=1988632&dwn=1],
: [http://dx.doi.org/10.1145/3193992.3194003 http://dx.doi.org/10.1145/3193992.3194003] under the license http://www.acm.org/publications/policies/copyright_policy#Background

* [https://hal.archives-ouvertes.fr/hal-01768687 https://hal.archives-ouvertes.fr/hal-01768687],
: [https://hal.archives-ouvertes.fr/hal-01768687/document https://hal.archives-ouvertes.fr/hal-01768687/document],
: [https://hal.archives-ouvertes.fr/hal-01768687/file/article-auteur.pdf https://hal.archives-ouvertes.fr/hal-01768687/file/article-auteur.pdf]

* [https://hal.archives-ouvertes.fr/hal-01768687/document https://hal.archives-ouvertes.fr/hal-01768687/document],
: [https://dblp.uni-trier.de/db/conf/icse/formalise2018.html#TodorovBT18 https://dblp.uni-trier.de/db/conf/icse/formalise2018.html#TodorovBT18],
: [https://hal.archives-ouvertes.fr/hal-01768687 https://hal.archives-ouvertes.fr/hal-01768687],
: [https://academic.microsoft.com/#/detail/2884526401 https://academic.microsoft.com/#/detail/2884526401]

← Older revision	Revision as of 17:23, 28 January 2021
(No difference)

Taha et al 2018a - Revision history

Scipediacontent: Scipediacontent moved page Draft Content 755838517 to Taha et al 2018a

Scipediacontent: Created page with " == Abstract == International audience; The ever-increasing complexity of automotive embedded systems and the need for safe advanced driver assistance systems (ADAS) represen..."