Suche   Â
Toyota verwendet SPARK Pro in einem Forschungsprojekt für Ultra-Low-Defect-Software
ID: 863583
Paris, 30. April 2013 – Das Zentrum für Informationstechnologie von Toyota verwendet die auf Ada basierende Programmiersprache SPARK und das SPARK Pro Toolset für die Entwicklung sicherheitskritischer Lösungen in der Automobilherstellung. SPARK und das von Altran und AdaCore entwickelte SPARK Pro bieten Toyota neue Möglichkeiten bei der Konzeption und Realisierung von Ultra-Low-Defect-Software.
(firmenpresse) - Das Toyota InfoTechnology Center (ITC) in Japan hat die Programmiersprache SPARK und das SPARK Pro Toolset für den Einsatz in einem Forschungsprojekt für die Entwicklung von Software höchster Zuverlässigkeit ausgewählt. Das Ziel des Projektes ist es, zu zeigen, dass Software-Requirements nachweislich frei von Laufzeitfehlern in eine Implementierung überführt werden können. Dies bietet entscheidende Vorteile der Bereitstellung von Ultra-Low-Defect-Software für erhöhte Zuverlässigkeit von Fahrzeug-Komponenten. Ein weiterer Vorteil ist die Reduzierung des Entwicklungs- und Wartungsaufwands, da der verwendete formale Ansatz eine Reihe von erwünschten Eigenschaften mathematisch beweisen kann. Bestimmte Testaktivitäten werden dadurch überflüssig, nachträgliche Korrekturen seltener.
Das Forschungsprojekt geht vom bewährten Design einer einzigen Fahrzeug-System-Komponente aus und erstellt eine vollständig sichere Code-Implementierung. Mit der SPARK-Pro-Technologie kann eine Software hergestellt werden, die unter allen Betriebsbedingungen ohne Laufzeitfehler läuft. Dies stellt einen ersten Schritt für die Erstellung großer Ultra-Low-Defect-Systeme dar. Alternative Ansätze mit herkömmlichen Methoden der Softwareentwicklung stoßen hier auf fundamentale Grenzen, denn das Testen kann immer nur für eine begrenzte Anzahl von Bedingungen den Nachweis der Fehlerfreiheit erbringen, und statische Analysen von vorhandenem Code hinsichtlich Schwachstellen oder Fehler können immer nur auf bereits vorhandene Fehler reagieren, sie aber nicht von vornherein ausschließen. Mit der Programmiersprache SPARK, dem Toolset und den dazugehörigen Methoden wird dieses grundlegende Problem gelöst und ein klarer Wettbewerbsvorteil für diese Komponente erreicht.
Ãœber SPARK
SPARK ist ein Subset der Programmiersprache Ada, das die genaue Spezifikation des Designs oder Anforderungen im Quellcode mit einer formalen Notation für Contracts unterstützt, einschließlich Pre- und Post-Bedingungen für Funktionen und Abhängigkeiten im Informationsaustausch zwischen Modulen. Mit dem SPARK Pro Toolset können Anwender sicherstellen, dass die Software das Design richtig implementiert beziehungsweise seinen Anforderungen entspricht, indem überprüft wird, ob die Logik des Quellcodes den spezifizierten Contracts entspricht.
SPARK kann sowohl Systemanforderungen präzise ausdrücken als auch eine ausführbare Implementierung definieren, die formal nachweisen kann, dass sie die jeweiligen Anforderungen erfüllt. Formale Richtigkeit (Correctness) kann somit von Anfang an gezeigt werden, sie lässt sich dann schrittweise mit der Weiterentwicklung des Systems anpassen. Dies ist ein völlig neuer Ansatz, der sehr viel zuverlässiger ist als die herkömmliche Entwicklung eines Systems mit anschließenden Tests oder statischen Analysen zur Reduzierung von Fehlern, die in früheren Phasen entstanden sind.
Ãœber SPARK Pro
SPARK Pro wurde gemeinsam von Altran und AdaCore entwickelt. Es bietet eine State-of-the-Art-Sprache und ein Engineering-Toolset für hochsicherheitskritische Software. SPARK Pro verbindet die Sprache und Verifikations-Tools von Altrans SPARK mit dem GNAT Programming Studio (GPS) und GNATbench Integrated Development Environments von AdaCore. Verfügbar sind SPARK-Versionen auf Basis von Ada 83, Ada 95 und Ada 2005, so dass alle gängigen Ada-Compiler und -Tools Out-of-the-Box mit SPARK arbeiten können.
Die Sprache SPARK Pro und das Toolset sind speziell für die Entwicklung von Anwendungen konzipiert, bei denen ein fehlerloser Betrieb von entscheidender Bedeutung für die Sicherheit ist. SPARK Pro bietet statische Überprüfung, die hinsichtlich ihrer Solidität konkurrenzlos ist – beispielsweise keine "false negatives" –, eine niedrige Fehler-Alarm-Rate und Effizienz. Das Toolset garantiert die Korrektheit sowie die Abwesenheit von Laufzeitfehlern und kann verwendet werden, um die Anforderungen von Sicherheitszertifizierungen wie ISO 26262, DO-178B, DO-178C und der Common Criteria (CC) zu erfüllen. SPARK Pro lässt sich insbesondere im Zusammenhang mit dem Anhang "Formal Methods" zu DO-178C verwenden.
Ãœber Toyota InfoTechnology Center
Toyota InfoTechnology Center Co. bietet Spitzentechnologie mit überlegenem Know-how und Innovationskraft für Kraftfahrzeug-IT. Toyota ITC befasst sich mit der Entwicklung von fortgeschrittenen, anspruchsvollen Informationstechnologien, um den Anforderungen des Marktes gerecht zu werden. Dazu zählen Forschung, Entwicklung und Evaluierung von Technologien, Hardware- und Software-Studien, die Analyse und Planung von Markt- und Geschäftsmodellen sowie das Management von Rechten an geistigem Eigentum. Der Hauptsitz von Toyota ITC ist in Tokio, in Mountain View, Kalifornien, besteht eine Niederlassung; Website: www.toyota-itc.com
Ãœber Altran
Altran ist globaler Marktführer in Innovationen und High-Tech Consulting. Altran berät seit über 30 Jahren Marktführer aus den Bereichen Automobilbau, Energie, Finanzen, Healthcare, Luft- und Raumfahrt, Schienen- und Transportwesen sowie Telekommunikation.
Altran deckt mit seinen Beratungsangeboten sämtliche Stufen der Projektentwicklung ab und kann dabei auf umfangreiches Technologie-Know-how aus vier Solutions zurückgreifen: Innovative Technologies, Sustainable Products, Sustainable Concepts sowie Sustainability Enterprise Performance.
Diese Presseinformation kann auch unter www.pr-com.de abgerufen werden.
Unternehmensinformation / Kurzprofil:
AdaCore wurde 1994 gegründet und ist der führende Anbieter von kommerziellen Softwarelösungen für Ada, einer modernen Programmiersprache für große, langlebige Anwendungen, bei denen Sicherheit und Verlässlichkeit kritisch sind. Das wichtigste Produkt des Unternehmens ist die Entwicklungsumgebung GNAT Pro, die Online-Support bietet und auf mehr Plattformen als jede andere Ada-Technologie verfügbar ist. AdaCore hat eine große, weltweite Kundenbasis; bitte finden Sie weitere Informationen auf der folgenden Seite: http://www.adacore.com/home/company/customers/
Sowohl Ada als auch GNAT Pro werden immer häufiger im High-integrity-Bereich und für sicherheitszertifizierte Anwendungen eingesetzt, so vor allem in sicherheitssensiblen Bereichen wie der Luftfahrt, militärischen Systemen, der Flugverkehrskontrolle, dem Flugverkehrsmanagement, dem Eisenbahnbereich, der medizinischen Produkte oder dem Finanzsektor.
AdaCore hat seinen nordamerikanischen Hauptsitz in New York, der europäische Hauptsitz ist in Paris. Weitere Informationen unter www.adacore.com
AdaCore
Jamie Ayre
press(at)AdaCore.com
www.AdaCore.com
http://twitter.com/AdaCoreCompany
PR-COM GmbH
Romana Redtenbacher
romana.redtenbacher(at)pr-com.de
www.pr-com.de
Tel. +49-89-59997-761
  
  
  
Datum: 30.04.2013 - 13:03 Uhr
Sprache: Deutsch
News-ID 863583
Anzahl Zeichen: 6085
Kontakt-Informationen:
Ansprechpartner: Romana Redtenbacher
Stadt:
Paris
Telefon: +49-89-59997-761
Kategorie:
Computer & Technik
Meldungsart: Unternehmensinformation
Versandart: Veröffentlichung
Diese Pressemitteilung wurde bisher 0 mal aufgerufen.
Die Pressemitteilung mit dem Titel:
"Toyota verwendet SPARK Pro in einem Forschungsprojekt für Ultra-Low-Defect-Software"
steht unter der journalistisch-redaktionellen Verantwortung von
AdaCore (Nachricht senden)
Beachten Sie bitte die weiteren Informationen zum Haftungsauschluß (gemäß TMG - TeleMedianGesetz) und dem Datenschutz (gemäß der DSGVO).