14:00 – 14:40 (subject to change)
The use of formal methods for specification and implementation in safety-critical applications drastically reduces source code based risks. Thus, the impact of defects introduced by development tools gains significance. The development of the world’s first generation of electronic engine controllers for emergency diesel generators in civil nuclear power plants requires full compliance with IEC 60880, category A and IEC 61508-3:2010, SCL 3. The qualification strategy applied is firmly based on formal, mathematically sound methods, representing the cutting edge of the state of the art in code generation and analysis techniques. The formal approach greatly enhances confidence in the correctness of the generated code. The significant reduction of qualification effort, memory consumption and code run time yield cost reductions in development, production and maintenance. Application of the benefits is not limited to safety-critical applications.
Marc Schlickling received the PhD degree in computer science from Saarland University, Saarbrücken, Germany, in 2012. His research interests include worst-case execution time analyses, predictability and the derivation of abstracted processor models. As a software engineer at Absint, his work has covered the development of runtime analyzers for high-end embedded controllers used in avionics, tool and process certification according to DO-178B and the analyzability of model-generated code. His work at MTU Friedrichshafen includes the design and implementation of safety-critical embedded digital controllers in full compliance with IEC 60880 and IEC 61508, process and tool qualification, and formal verification. Since 2018, he’s managing the development projects for ECU basic software.
Jörg Herter studied computer science and received his PhD on predictable dynamic memory allocation for hard real-time systems in 2014. He has been a research fellow at Saarland University and the Saarland University of Applied Sciences in Saarbrücken. His current work is focused on functional safety and the formal validation and verification of safety-critical software. He works as a senior technical consultant for Absint. He teaches static program analysis, embedded systems technology, compiler construction, and mathematics at the Saarland University of Applied Sciences and Cooperative Education. He’s also a lecturer at the University of Luxembourg and has been teaching at Saarland University and the technical university of Kaiserslautern.