Forum für Wissenschaft, Industrie und Wirtschaft

Hauptsponsoren:     3M 
Datenbankrecherche:

 

Analyse- und Lösungsmotor übertrifft XSB Prolog

21.09.2004


Ein als Succinct Solver V2.0 bekannter Analysemotor zur Lösung von Daten- und Kontrollflussproblemen wurde entwickelt. Hierbei handelt es sich eigentlich um nichts Besonderes, aber dieser spezielle Motor ist in einer Standard Manipulation Language geschrieben und übertrifft daher die Leistung von XSB Prolog deutlich.

... mehr zu:
»Analysator »Java »Prolog »Solver »Succinct »XSB

In den letzten Jahren hat sich die statische Programmanalyse zu einer bewährten Technologie für den Einsatz von Compilern und Interpretern entwickelt. Zwei gute Beispiele für den Einsatz von statischen Analyseverfahren sind die Software-Reengineering-Verfahren, die im Zusammenhang mit den Problemen der Jahrtausendwende verwendet wurden sowie die für Ariane V genutzten Softwarevalidationsprogramme.

Das ins Leben gerufene Projekt zielte darauf ab, die Skalierbarkeit von statischen Analysetechnologien zu bewerten sowie die sicherheitstechnischen Aspekte für realistische Sprachen und Anwendungen zu überprüfen. Das führte zur Identifizierung von zwei überaus wichtigen Sicherheitsbereichen, nämlich den SmartCards und der Internetprogrammierung. Daraufhin konzentrierten sich die Bemühungen des Projekts auf Java und den Java-Dialekt Java Card.


Der Succinct Solver selbst wurde über Reqs vereinfacht. Hierbei handelt es sich um ein Backend eines Programmanalysators, der durch Inria erzeugt und innerhalb eines restriktionsbasierten statischen Analysators entwickelt wurde. Dieser verwendet die Carmel-Sprache, die eine Zwischendarstellung des Byte-Codes der Java Card ist. Reqs löst mit Hilfe von Gittern Restriktionen, während der Analysator selbst unter Verwendung einer modularen Restriktionserzeugungstechnik implementiert wird und für die Analyse von Java-Programmteilen genutzt wird.

Der restriktionsbasierte statische Analysator stellt eine sichere Grundlage für die Untersuchung von Java-Komponenten und -Schnittstellen zur Verfügung und analysiert in Verbindung mit einer modularen Verifikationstechnik Java-Programmfragmente. Bei einem Vergleich des Succinct Solver mit anderen Lösungsmotoren, die in erster Linie XSB Prolog und DeMoney als Haupttestprogramm nutzen, zeigte sich, dass Succint Solver die Wettbewerber leistungsmäßig übertrifft.

Daher ist dieser Problemlöser besonders für die Sicherheitsmerkmale des Byte-Codes der Java Card, für die Bewertung der Steuerungseigenschaften von mobilen und unbeschränkten Umgebungen sowie für die Validation der Protokollkommunikation in geeigneten Algebraprozessen von großem Nutzen. Deshalb können Entwicklungen wie der Succinct Solver, Reqs und der restriktionsbasierte statische Analysator die zukünftige Sicherheit von Sichtmodifikatoren und gemeinsam nutzbaren Schnittstellen gewährleisten.

Prof. Flemming Nielson | ctm
Weitere Informationen:
http://www.imm.dtu.dk
http://www.imm.dtu.dk/~nielson

Weitere Berichte zu: Analysator Java Prolog Solver Succinct XSB

Weitere Nachrichten aus der Kategorie Verfahrenstechnologie:

nachricht Staubarmes Recycling wertvoller Rohstoffe aus Elektronikschrott
16.11.2016 | Fraunhofer-Institut für Produktionstechnologie IPT

nachricht Mikrostrukturen mit dem Laser ätzen
25.10.2016 | Fraunhofer-Institut für Lasertechnik ILT

Alle Nachrichten aus der Kategorie: Verfahrenstechnologie >>>

Die aktuellsten Pressemeldungen zum Suchbegriff Innovation >>>

Die letzten 5 Focus-News des innovations-reports im Überblick:

Im Focus: Wie sich Zellen gegen Salmonellen verteidigen

Bioinformatiker der Goethe-Universität haben das erste mathematische Modell für einen zentralen Verteidigungsmechanismus der Zelle gegen das Bakterium Salmonella entwickelt. Sie können ihren experimentell arbeitenden Kollegen damit wertvolle Anregungen zur Aufklärung der beteiligten Signalwege geben.

Jedes Jahr sind Salmonellen weltweit für Millionen von Infektionen und tausende Todesfälle verantwortlich. Die Körperzellen können sich aber gegen die...

Im Focus: Shape matters when light meets atom

Mapping the interaction of a single atom with a single photon may inform design of quantum devices

Have you ever wondered how you see the world? Vision is about photons of light, which are packets of energy, interacting with the atoms or molecules in what...

Im Focus: Greifswalder Forscher dringen mit superauflösendem Mikroskop in zellulären Mikrokosmos ein

Das Institut für Anatomie und Zellbiologie weiht am Montag, 05.12.2016, mit einem wissenschaftlichen Symposium das erste Superresolution-Mikroskop in Greifswald ein. Das Forschungsmikroskop wurde von der Deutschen Forschungsgemeinschaft (DFG) und dem Land Mecklenburg-Vorpommern finanziert. Nun können die Greifswalder Wissenschaftler Strukturen bis zu einer Größe von einigen Millionstel Millimetern mittels Laserlicht sichtbar machen.

Weit über hundert Jahre lang galt die von Ernst Abbe 1873 publizierte Theorie zur Auflösungsgrenze von Lichtmikroskopen als ein in Stein gemeißeltes Gesetz....

Im Focus: Durchbruch in der Diabetesforschung: Pankreaszellen produzieren Insulin durch Malariamedikament

Artemisinine, eine zugelassene Wirkstoffgruppe gegen Malaria, wandelt Glukagon-produzierende Alpha-Zellen der Bauchspeicheldrüse (Pankreas) in insulinproduzierende Zellen um – genau die Zellen, die bei Typ-1-Diabetes geschädigt sind. Das haben Forscher des CeMM Forschungszentrum für Molekulare Medizin der Österreichischen Akademie der Wissenschaften im Rahmen einer internationalen Zusammenarbeit mit modernsten Einzelzell-Analysen herausgefunden. Ihre bahnbrechenden Ergebnisse werden in Cell publiziert und liefern eine vielversprechende Grundlage für neue Therapien gegen Typ-1 Diabetes.

Seit einigen Jahren hatten sich Forscher an diesem Kunstgriff versucht, der eine simple und elegante Heilung des Typ-1 Diabetes versprach: Die vom eigenen...

Im Focus: Makromoleküle: Mit Licht zu Präzisionspolymeren

Chemikern am Karlsruher Institut für Technologie (KIT) ist es gelungen, den Aufbau von Präzisionspolymeren durch lichtgetriebene chemische Reaktionen gezielt zu steuern. Das Verfahren ermöglicht die genaue, geplante Platzierung der Kettengliedern, den Monomeren, entlang von Polymerketten einheitlicher Länge. Die präzise aufgebauten Makromoleküle bilden festgelegte Eigenschaften aus und eignen sich möglicherweise als Informationsspeicher oder synthetische Biomoleküle. Über die neuartige Synthesereaktion berichten die Wissenschaftler nun in der Open Access Publikation Nature Communications. (DOI: 10.1038/NCOMMS13672)

Chemische Reaktionen lassen sich durch Einwirken von Licht bei Zimmertemperatur auslösen. Die Forscher am KIT nutzen diesen Effekt, um unter Licht die...

Alle Focus-News des Innovations-reports >>>

Anzeige

Anzeige

IHR
JOB & KARRIERE
SERVICE
im innovations-report
in Kooperation mit academics
Veranstaltungen

Von „Coopetition“ bis „Digitale Union“ – Die Fertigungsindustrien im digitalen Wandel

02.12.2016 | Veranstaltungen

Experten diskutieren Perspektiven schrumpfender Regionen

01.12.2016 | Veranstaltungen

Die Perspektiven der Genom-Editierung in der Landwirtschaft

01.12.2016 | Veranstaltungen

 
VideoLinks
B2B-VideoLinks
Weitere VideoLinks >>>
Aktuelle Beiträge

Wie sich Zellen gegen Salmonellen verteidigen

05.12.2016 | Biowissenschaften Chemie

Fraunhofer WKI koordiniert vom BMEL geförderten Forschungsverbund zu Zusatznutzen von Dämmstoffen aus nachwachsenden Rohstoffen

05.12.2016 | Förderungen Preise

Höhere Energieeffizienz durch Brennhilfsmittel aus Porenkeramik

05.12.2016 | Energie und Elektrotechnik