Can we build it: formal synthesis of control strategies for cooperative driver assistance systems

Autor: Werner Damm, Hans-Jörg Peter, Bernd Westphal, Jan-Hendrik Rakow

Publikováno v: Mathematical Structures in Computer Science. 23:676-725

We propose a design and verification methodology supporting the early phases of system design for cooperative driver assistance systems, focusing on the realisability of new automotive functions. Specifically, we focus on applications where drivers a

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::c04b6d1d2698e778907d5b720a03d058
https://doi.org/10.1017/s0960129512000230

Improving the Efficiency of Formal Verification: The Case of Clock-Domain Crossings

Autor: Dominique Borrione, Guillaume Plassan, Hans-Jörg Peter, Shaker Sarwary, Katell Morin-Allory

Publikováno v: IFIP Advances in Information and Communication Technology
24th IFIP/IEEE International Conference on Very Large Scale Integration-System on a Chip (VLSISOC)
24th IFIP/IEEE International Conference on Very Large Scale Integration-System on a Chip (VLSISOC), Sep 2016, Tallinn, Estonia. pp.108-129, ⟨10.1007/978-3-319-67104-8_6⟩
IFIP Advances in Information and Communication Technology ISBN: 9783319671031
VLSI-SoC (Selected Papers)

International audience; We propose a novel semi-automatic methodology to formally verify clock-domain synchronization protocols in industrial-scale hardware designs. To establish the functional correctness of all clock-domain crossings (CDCs) in a sy

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::5dd65965b186af870e52750a6306ec48
https://hal.inria.fr/hal-01675192/file/456609_1_En_6_Chapter.pdf

FlexRay for Avionics: Automatic Verification with Parametric Physical Layers

Autor: Bernd Finkbeiner, Michael Gerke, Hans-Jörg Peter, Rüdiger Ehlers

Publikováno v: Infotech@Aerospace

The automotive FlexRay standard is increasingly attracting attention in the aeronautics industry. Upgrading existing physical layers, such as CAN-based systems, with FlexRay is attractive, especially given that inexpensive FlexRay hardware is availab

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::f3be17334b0b587b60e10e999da59032
https://doi.org/10.2514/6.2012-2583

Template-Based Controller Synthesis for Timed Systems

Autor: Bernd Finkbeiner, Hans-Jörg Peter

Publikováno v: Tools and Algorithms for the Construction and Analysis of Systems ISBN: 9783642287558
TACAS

We present an effective controller synthesis method for real-time systems modeled as timed automata with safety requirements. Under the realistic assumption of partial observability, the problem is undecidable in general, and prohibitively expensive

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::0359d1f21b6b0cd85a31a6dbdebf47a0
https://doi.org/10.1007/978-3-642-28756-5_27

Fully Symbolic Timed Model Checking Using Constraint Matrix Diagrams

Autor: Rüdiger Ehlers, Hans-Jörg Peter, Daniel Fass, Michael Gerke

Publikováno v: RTSS

We present constraint matrix diagrams (CMDs), a novel data structure for the fully symbolic reach ability analysis of timed automata. CMDs combine matrix-based and diagram-based state space representations generalizing the concepts of difference boun

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::6c1cd39c42682fbc0c67c6181cd21cdb
https://doi.org/10.1109/rtss.2010.36