Software Dependability

Zentrale Herausforderung

Die derzeit am Markt verfügbaren Methoden und Technologien zur Validierung, Verifikation und Qualifizierung verlässlicher und sicherheits-relevanter Software sind ressourcen-intensiv (oftmals 50-70% des Gesamtaufwands in der Entwicklung), und nicht direkt anwendbar auf hochautomatisierte, offene, dynamische, daten-getrieben evolvierende und optimierende Cyber-Physikalische System (CPS), wie sie derzeit in der Automobilindustrie, der Luft- und Raumfahrt, der Industrieautomatisierung und der Medizintechnik allgegenwärtig konzipiert und entwickelt werden.

Neue Ansätze, Methoden und Techniken zur beherrschbaren und erschwinglichen Entwicklung, Absicherung und Betrieb komplexer, software-basierter CPS sind deshalb Grundvoraussetzung für Einsatz und Erfolg dieser Produkte im Markt, und zur Realisierung zugehöriger CPS-basierter, innovativer Geschäfts- und Dienstmodelle.

Forschungsbeiträge

Wir erforschen und erproben neuartige Algorithmen, Methoden und Werkzeuge, basierend auf Verfahren der symbolischen Analyse und Synthese für nachweislich verlässliche und sichere software-intensive CPS.

Diese Verfahren können über den gesamten Entwicklungszyklus, von der Validierung von Anforderungen, der Architekturanalyse als auch der eigentlichen Software-Verifikation, angewandt werden; sie unterstützen auch agile Software-Entwicklung; sie funktionieren auch für unvollständige Spezifikationen und Modelle; Verifikation offener Systeme ermöglicht Wiederverwendbarkeit über verschiedenste operative Umgebungen hinweg, und ist die Schlüsseltechnologie zur modularen Verifikation und Zertifizierung.

Wir erschließen, in enger Kooperation mit Partnern aus Industrie und akademischer Forschung, die Themenfelder:

  1. Sicherheits-Architekturen und -Richtlinien (security policies) zur komponenten-basierten Entwicklung sicherheits-gerichteter und verteilter Echtzeitsysteme (Mils Sicherheits-Architektur und -Plattform)
  2. Evidenz-basierte Kopplung von Software-Verifikations-Werkzeugen zur automatisierten und effizienten Verifikation und Validierung von Software-Artefakten in agilen Software-Entwicklungsprozessen
  3. Automatisierte Generierung von Steuerungs-Software aus strukturierten und formalisierten Anforderungen (Corrct-By-Construction)
  4. Automatisierte Verlässlichkeits- und Sicherheitsanalyse von Software-Artefakten (Assurance/Dependability Case)
  5. Alternative Ansätze, Verfahren und Techniken zur Zertifizierung hochautomatisierter bzw. autonomer, offener und dynamischer Systeme (Modular / Runtime / Just-in-time Certification).

Leistungsangebot

  1. Anwendung formaler Software- und System-Analyse für sicherheits-gerichtete Entwicklung nach den Industriestandards DO178C/DO333, ISO 61508, ISO/IEC 15408
  2. Konzeption und Anpassung moderner Werkzeugketten zur Verifikation & Validierung zertifizierbarer Software-Systeme
  3. Architektur-zentrierte Zuverlässlichkeits- und Sicherheitsanalysen, sowie wiss. Unterstützung bei der Konstruktion zugehöriger Assurance Cases
  4. Entwicklung und Erprobung von Methoden und Techniken produkt-basierter Zertifizierung für hoch-automatisierte und autonome Systeme

Forschungsprojekte (Auswahl)

  • CPS Engineering Labs (European Commission, H2020)
  • Platforms4CPS (European Commission, H2020)
  • Certification of Safety GNC (European Space Agency)
  • Open Certifiable UAV (Airbus Group)
  • Formal methods for ISO262626-conformant Software (Siemens AG)
  • Software Quality (Intel)
  • openMOS (European Commission, H2020
  • BeInCPPS (European Commission, H2020)
  • Transatlantic CPS Summit (European Commission, H2020)
  • Distributed Mils (European Commission, FP7)

Software

  • autoAnalyzer (LGPL V3.0 License) <link to be provided>
  • autoCoder (LGPL V3.0 License) <link to be provided>

Präsentationen

Eine Auswahl unserer Präsentationen sind verfügbar auf Slideshare.

VERÖFFENTLICHUNGEN

Liste als BibTeX-Datei exportieren

  • Martin Hofmann, Christian Neukirchen und Harald Rueß. Certification for u-Calculus with Winning Strategies. In Model Checking Software - 23rd International Symposium, SPIN 2016, Co-located with ETAPS 2016, Eindhoven, The Netherlands, April 7-8, 2016, Proceedings, pages 111–128, 2016. Details DOI BibTeX
  • Lacramioara Astefanoaei, Saddek Bensalem und Marius Bozga. A Compositional Approach to the Verification of Hybrid Systems. In Theory and Practice of Formal Methods - Essays Dedicated to Frank de Boer on the Occasion of His 60th Birthday, pages 88–103, 2016. Details DOI BibTeX
  • Chih-Hong Cheng, Yassine Hamza und Harald Rueß. Structural Synthesis for GXW Specifications. In Computer Aided Verification - 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part I, pages 95–117, 2016. Details DOI BibTeX
  • Denis Bytschkow, Jean Quilbeuf, Georgeta Igna und Harald Rueß. Distributed MILS architectural approach for secure smart grids. In . Springer International Publishing, 2014. Details BibTeX
  • Chih-Hong Cheng, Chung-Hao Huang, Harald Rueß und Stefan Stattelmann. G4LTL-ST: Automatic Generation of PLC Programs. In Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings, pages 541–549, 2014. Details DOI BibTeX
  • Chih-Hong Cheng, Harald Rueß und Natarajan Shankar. JBernstein: A Validity Checker for Generalized Polynomial Constraints. In Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings, pages 656–661, 2013. Details DOI BibTeX
  • Chih-Hong Cheng, Michael Geisinger und Christian Buckl. Synthesizing Controllers for Automation Tasks with Performance Guarantees. In Model Checking Software - 20th International Symposium, SPIN 2013, Stony Brook, NY, USA, July 8-9, 2013. Proceedings, pages 154–159, 2013. Details DOI BibTeX
  • Jan Olaf Blech, Yliès Falcone, Harald Rueß und Bernhard Schätz. Behavioral Specification Based Runtime Monitors for OSGi Services. In Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change - 5th International Symposium, ISoLA 2012, Heraklion, Crete, Greece, October 15-18, 2012, Proceedings, P, pages 405–419, 2012. Details DOI BibTeX
  • Chih-Hong Cheng, Rongjie Yan, Harald Rueß und Saddek Bensalem. Distributed priority synthesis using knowledge. In Proceedings of the 2nd edition on Programming systems, languages and applications based on actors, agents, and decentralized control abstractions, AGERE! 2012, October 21-22, 2012, Tucson, Arizona, USA, pages 129–132, 2012. Details DOI BibTeX
  • Chih-Hong Cheng, Michael Geisinger, Harald Rueß, Christian Buckl und Alois Knoll. MGSyn: Automatic Synthesis for Industrial Automation. In Computer Aided Verification - 24th International Conference, CAV 2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings, pages 658–664, 2012. Details DOI BibTeX
  • Chih-Hong Cheng, Michael Geisinger, Harald Rueß, Christian Buckl und Alois Knoll. Game solving for industrial automation and control. In IEEE International Conference on Robotics and Automation, ICRA 2012, 14-18 May, 2012, St. Paul, Minnesota, USA, pages 4367–4372, 2012. Details DOI BibTeX
  • Chih-Hong Cheng, Rongjie Yan, Saddek Bensalem und Harald Rueß. Distributed Priority Synthesis. In Proceedings Seventh Conference on Systems Software Verification, SSV 2012, Sydney, Australia, 28-30 November 2012., pages 57–72, 2012. Details DOI BibTeX
  • Chih-Hong Cheng, Saddek Bensalem, Yu-Fang Chen, Rongjie Yan, Barbara Jobstmann, Harald Rueß, Christian Buckl und Alois Knoll. Algorithms for Synthesizing Priorities in Component-Based Systems. In Automated Technology for Verification and Analysis, 9th International Symposium, ATVA 2011, Taipei, Taiwan, October 11-14, 2011. Proceedings, pages 150–167, 2011. Details DOI BibTeX
  • Chih-Hong Cheng, Saddek Bensalem, Barbara Jobstmann, Rongjie Yan, Alois Knoll und Harald Rueß. Model Construction and Priority Synthesis for Simple Interaction Systems. In NASA Formal Methods - Third International Symposium, NFM 2011, Pasadena, CA, USA, April 18-20, 2011. Proceedings, pages 466–471, 2011. Details DOI BibTeX
  • Chih-Hong Cheng, Alois Knoll, Michael Luttenberger und Christian Buckl. GAVS+: An Open Platform for the Research of Algorithmic Game Solving. In Tools and Algorithms for the Construction and Analysis of Systems - 17th International Conference, TACAS 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, , pages 258–261, 2011. Details DOI BibTeX
  • Chih-Hong Cheng, Harald Rueß, Alois Knoll und Christian Buckl. Synthesis of Fault-Tolerant Embedded Systems Using Games: From Theory to Practice. In Verification, Model Checking, and Abstract Interpretation - 12th International Conference, VMCAI 2011, Austin, TX, USA, January 23-25, 2011. Proceedings, pages 118–133, 2011. Details DOI BibTeX
  • Chih-Hong Cheng, Christian Buckl, Michael Luttenberger und Alois Knoll. GAVS: Game Arena Visualization and Synthesis. In Automated Technology for Verification and Analysis - 8th International Symposium, ATVA 2010, Singapore, September 21-24, 2010. Proceedings, pages 347–352, 2010. Details DOI BibTeX
  • Chih-Hong Cheng. GAVS: Game Arena Visualization and Synthesis. In Proceedings of the Joint Workshop of the German Research Training Groups in Computer Science, Algorithmic synthesis of reactive and discrete-continuous systems, AlgoSyn 2010, May 31 - June 2, 2010, pages 147, 2010. Details BibTeX
  • Chih-Hong Cheng, Alois Knoll, Christian Buckl, Javier Esparza und Yang Chen. Examining robotic systems with shape-adjustable manipulators under dynamic environments: From simulation to verification. In MariaSimonetta Balsamo, William J. Knottenbelt und Andrea Marin, editor, Proceedings of the IEEE International Symposium on Computational Intelligence in Robotics and Automation, CIRA 2009, 15-18 December 2009, Daejeon, Korea, pages 72–77, 2009. Details DOI BibTeX
  • Chih-Hong Cheng, Markus Rickert, Christian Buckl, Edward A. Lee und Alois Knoll. Toward the Design of Robotic Software with Verifiable Safety. In Proceedings of the 33rd Annual IEEE International Computer Software and Applications Conference, COMPSAC 2009, Seattle, Washington, USA, July 20-24, 2009. Volume 1, pages 622–623, 2009. Details DOI BibTeX
  • Chih-Hong Cheng, Christian Buckl, Javier Esparza und Alois Knoll. Modeling and Verification for Timing Satisfaction of Fault-Tolerant Systems with Finiteness. In 13th IEEE/ACM International Symposium on Distributed Simulation and Real Time Applications, Singapore, 25-28 October 2009, pages 208–215, 2009. Details DOI BibTeX
  • Chih-Hong Cheng, Christian Buckl, Javier Esparza und Alois Knoll. Modeling and Verification for Timing Satisfaction of Fault-Tolerant Systems with Finiteness. CoRR, abs/0905.3951():, 2009. Details BibTeX
  • Chih-Hong Cheng, Natarajan Shankar, Harald Rueß und Saddek Bensalem. EFSMT: A Logical Framework for Cyber-Physical Systems. CoRR, abs/1306.3456():, 2013. Details BibTeX
  • Jan Olaf Blech, Harald Rueß und Bernhard Schätz. On Behavioral Types for OSGi: From Theory to Implementation. CoRR, abs/1306.6115():, 2013. Details BibTeX
  • Jean Quilbeuf, Georgeta Igna, Denis Bytschkow und Harald Rueß. Security policies for distributed systems. CoRR, abs/1310.3723():, 2013. Details BibTeX
  • Chih-Hong Cheng, Harald Rueß, Alois Knoll und Christian Buckl. A Game-theoretic Approach for Synthesizing Fault-Tolerant Embedded Systems. CoRR, abs/1011.0268():, 2010. Details BibTeX
  • Chih-Hong Cheng, Christian Buckl, Javier Esparza und Alois Knoll. FTOS-Verify: Analysis and Verification of Non-Functional Properties for Fault-Tolerant Systems. CoRR, abs/0905.3946():, 2009. Details BibTeX

Ansprechpartner

Harald Rueß

Dr. rer. nat.
Harald Rueß

TELEFON
+49 89 3603522 10

E-MAIL

ruess(at)fortiss.org