http://dl.gi.de/handle/20.500.12116/40946 2026-07-21T14:24:38Z http://dl.gi.de/handle/20.500.12116/40971 Softwarezuverlässigkeitsbewertung auf Basis von Betriebsprofiltreue und Schnittstellenüberdeckung Meitner, Matthias; Saglietti, Francesca Dieser Artikel stellt einen neuen Ansatz zur Softwarezuverlässigkeitsbewertung vor, der über die Betriebstreue der auszuwertenden Testfälle hinaus auch eine hohe Überdeckung der Komponentenschnittstellen sicherstellt. Der Erfüllungsgrad der zugrunde liegenden Bedingungen hinsichtlich Profiltreue, Testdatenunabhängigkeit und Interaktionsüberdeckung wird durch geeignete Metriken erfasst und mittels genetischer Algorithmen multi-kriteriell optimiert. Insgesamt unterstützt das entwickelte Verfahren die automatische Generierung einer Testfallmenge, auf deren Basis eine konservative Softwarezuverlässigkeitsaussage bei gleichzeitiger Überdeckung der Komponenteninteraktionen ermöglicht wird. 2011-01-01T00:00:00Z http://dl.gi.de/handle/20.500.12116/40970 Verifikation von UML-Statecharts unter besonderer Berücksichtigung von Speicherverbrauch und Laufzeit des Model Checkers Ammann, Christian Ein Model Checker verifiziert, ob ein Modell bestimmte Anforderungen erfüllt. Eine Möglichkeit, das Verhalten von Softwaresystemen zu modellieren, sind endliche Automaten. Diese finden Einzug in die Unified Modelling Language in Form von Statecharts. UML-Statecharts können ein hohes Maß an Komplexitt erreichen, so dass sich ihr Zustandsraum nicht mehr komplett in den Hauptspeicher abbilden lsst. Dies führt dazu, dass eine vollstndige Verifikation mit einem Model Checker nicht mehr möglich ist, da der gesamte Zustandsraum nicht mehr untersucht werden kann. Um diesem Problem zu begegnen, stellt diese Arbeit die domnenspezifische Sprache UDL (UML-Statechart Description Language), sowie eine Transformation von UDL in die Model Checker Eingabesprache Promela vor. Der Schwerpunkt der Sprache UDL und des Übersetzungsprozesses liegt dabei auf der Generierung von effizientem Promelacode, der beim Verifizieren einen möglichst kleinen Zustandsraum belegt. Der Vorteil ist, dass durch diesen Ansatz auch größere Modelle wieder verifizierbar werden. Die Machbarkeit des Ansatzes und die daraus entstehenden Vorteile werden anhand einer Fallstudie mit dem 3D-Bewegungstrackingsystem AssyControl demonstriert. 2011-01-01T00:00:00Z http://dl.gi.de/handle/20.500.12116/40969 Hi-Lite - Verification by Contract Kanig, Johannes; Guitton, Jérôme; Moy, Yannick Formal methods and testing are often considered as disjoint technologies. The Hi-Lite project wants to show that both are actually complementary. The central concept are subprogram contracts, part of the upcoming Ada 2012 standard. A contract, which consists of pre- and postcondition, describes the specification of a subprogram, in the same syntax as Ada expressions. These contracts can be seen either as additional assertions in the case of testing, or they can be used to prove the correctness of the subprogram, using modern proof technology such as SMT solvers. This mechanism allows an easy adoption of modern formal methods, on a per-function basis. Hi-Lite fits in well with the upcoming DO-178C avionics safety standard, a revision to DO-178B, which, among other things, accounts for technologies such as formal methods. A contract is additional information a programmer has to write, and errors are possible. Another focus of the Hi-Lite project is to help the programmer write meaningful and complete contracts. Current proposals include the detection of runtime errors contained in contracts, meaningless or too strong contracts, incomplete contracts that do not mention modified variables and code that does not contribute to the contract. The goal of project Hi-Lite is to produce a verification toolchain combining formal methods and testing, integrated with the usual project structure in the two IDEs developed by AdaCore. 2011-01-01T00:00:00Z http://dl.gi.de/handle/20.500.12116/40968 ISO 26262 – Exemplary Tool Classification of Model-Based Design Tools Conrad, Mirko; Fey, Ines Tool classification is an important part of the tool qualification process required by ISO 26262 since it determines the required confidence level for each tool in use. To cover the variety of tools used by practitioners, the standard only provides a framework for tool classification and leaves it up to the applicant to instantiate this framework. To illustrate the ISO 26262 tool classification procedure, this paper provides an exemplary tool classification for the Model Advisor, a static analysis tool used in Model-Based Design, By putting this example into the context of a practical tool qualification approach for COTS tools, the author’s report their experiences in instantiating the ISO 26262-8 tool qualification framework. 2011-01-01T00:00:00Z