Symbolisches Model Checking variabler Verhaltensspezifikationen

Die Nutzung von Software beschränkt sich aufgrund der steigenden Durchdringung des wirtschaftlichen und sozialen Lebens mit Technologie nicht nur auf Informationssysteme im Unternehmen, sie findet auch zunehmenden Gebrauch in Automobilen, in der Unterhaltungselektronik und anderen Gegenständen des alltäglichen Gebrauchs. Der Markt erfordert zudem eine zunehmende Individualisierbarkeit und schnelle Innovationszyklen dieser Produkte, denen durch die Softwareproduktlinienentwicklung begegnet wird. Die vorliegende Arbeit stellt dazu einen Beitrag zur Qualitätssicherung früher Softwareartefakte in der Domänenentwicklung einer Softwareproduktlinie dar. Der beschriebene Ansatz konzentriert sich dabei auf das Model Checking formaler Verhaltensspezifikationen als Ergebnis der Designphase gegen formale Anforderungsspezifikationen aus der Anforderungsanalyse. Er dient damit der zeitnahen Aufdeckung von Designfehlern in Basisartefakten einer Produktlinie mit Methoden der Inter-Modell- Konsistenzprüfung. In dieser Arbeit wird das symbolische Model Checking für den Einsatz zur Konsistenzprüfung variabler Verhaltensspezifikationen und variablen CTL- Spezifikationen erweitert.