<![CDATA[
<BODY>
<H1>www.duv24.net : Formale Verifikation von Simulink/Stateflow-Modellen</H1>
<P> <BR>
[<A href="/">www.duv24.net</A>] [<A href="../index.html">back</A>]
</P>
<TABLE WIDTH=100% BORDER=0 CELLSPACING=0 CELLPADDING=0>
<TR>
<TD VALIGN=top>
<TABLE WIDTH=100% BORDER=0 CELLSPACING=0 CELLPADDING=0>
<TR>
<TD VALIGN=TOP CLASS=detailBereichRedaktion>Bereich >
Redaktion
> <B><FONT color="#CC3300">Nachrichten</FONT></B></TD>
<TD ALIGN=right VALIGN=bottom CLASS=detailDatum>26.08.2004</TD>
</TR>
</TABLE>
</TD>
<TD VALIGN=top> </TD>
<TD VALIGN=top> </TD>
</TR>
<TR>
<TD VALIGN=top CLASS=detailFirma ID=topSpace>OSC - Embedded Systems:</TD>
<TD VALIGN=top> </TD>
<TD VALIGN=top> </TD>
</TR>
<TR>
<TD VALIGN=top CLASS=detailTitel>Formale Verifikation von Simulink/Stateflow-Modellen</TD>
<TD VALIGN=top> </TD>
<TD VALIGN=top> </TD>
</TR>
<TR>
<TD VALIGN=top CLASS=detailSubtitel></TD>
<TD VALIGN=top> </TD>
<TD VALIGN=top> </TD>
</TR>
<TR>
<TD VALIGN=top>
<TABLE BORDER=0 CELLSPACING=0 CELLPADDING=0>
<TR>
<TD VALIGN=top CLASS=detailContent>Die OSC - Embedded Systems AG hat mit dem EmbeddedValidator ein leistungsfähiges Werkzeug zur automatischen Validierung von Simulink/Stateflow-Modellen auf der Basis von TargetLink generiertem C-Code entwickelt. EmbeddedValidator stellt eine Toolsuite bereit, um mittels Model-Checking eine modellbasierte formale Verifikation von reaktiven eingebetteten Systemen, die mit Simulink, Stateflow, und TargetLink entwickelt wurden, durchzuführen. Im Gegensatz zu konventionellen Testansätzen ist die Model-Checking Technologie eine vollautomatische und im mathematischen Sinne vollständige Methode. Mathematisch vollständig bedeutet in diesem Zusammenhang, dass keine Simulationssequenz existiert, die eine vom EmbeddedValidator als gültig bewiesene funktionale Anforderung verletzt. Das bedeutet, dass jeder logische Entwurfsfehler in einem zu analysierenden Modell aufgedeckt werden kann. EmbeddedValidator analysiert ein System bezüglich beliebiger Input-Szenarios und kann deshalb als „vollständiger Test“ betrachtet werden, wobei der Test gegen eine formal spezifizierte Anforderung ausgeführt wird. EmbeddedValidator bietet formale Verifikation für Simulink/Stateflow Modelle, die im Kern kontrollorientierte Applikationen darstellen. Dazu unterstützt EmbeddedValidator eine große Anzahl relevanter Simulink/TargetLink Blöcke. Der von TargetLink generierte C-Code wird verwendet, um die Semantik des Simulink/Stateflow Modells in die Verifikationsumgebung zu transportieren. Diese Technologie ermöglicht, dass ein zu entwickelndes Design hohen Qualitätsansprüchen bezüglich Robustheit und Korrektheit genügt, so dass Designfehler sowie Kosten minimiert werden können.</TD>
</TR>
<TR>
<TD CLASS=detailQuelle> </TD>
</TR>
</TABLE>
</TD>
<TD WIDTH=28 VALIGN=top><IMG NAME="" SRC=/pi/spacer.gif WIDTH=1 HEIGHT=1 ALT=""></TD>
<TD WIDTH=174 VALIGN=top></TD>
</TR>
<TR>
<TD VALIGN=top><IMG NAME="" SRC=/pi/spacer.gif WIDTH=393 HEIGHT=1 ALT=""></TD>
<TD WIDTH=28 VALIGN=top><IMG NAME="" SRC=/pi/spacer.gif WIDTH=28 HEIGHT=1 ALT=""></TD>
<TD WIDTH=174 VALIGN=top><IMG NAME="" SRC=/pi/spacer.gif WIDTH=174 HEIGHT=1 ALT=""></TD>
</TR>
</TABLE>
<P><I>Diese Seite wurde am 25.09.2004, 13:13 Uhr aktualisiert</I></P>
</BODY>
]]>