Model Checking (deutsch auch Modellprüfung) ist ein Verfahrenzur vollautomatischen Verifikation einer Systembeschreibung (Modell) gegen eine Spezifikation (Formel).Der Begriff ist motiviert durch die mathematische Formulierung des Problems:Für eine gegebene Systembeschreibung und eine gegebene logische Eigenschaft , prüfe, ob Modell ist für (formal ).

Property Value
dbo:abstract
  • Model Checking (deutsch auch Modellprüfung) ist ein Verfahrenzur vollautomatischen Verifikation einer Systembeschreibung (Modell) gegen eine Spezifikation (Formel).Der Begriff ist motiviert durch die mathematische Formulierung des Problems:Für eine gegebene Systembeschreibung und eine gegebene logische Eigenschaft , prüfe, ob Modell ist für (formal ). Das Verfahren wird als vollautomatisch bezeichnet, weil es keiner Benutzerinteraktion bedarf (im Gegensatz zu einigen deduktiven Verfahren, wie zum Beispiel interaktives Theorembeweisen). Die Systembeschreibung erfolgt in einer formalen Sprache, zum Beispiel durch ein Programm, einen endlichen Automaten oder ein Transitionssystem. Der Zustandsraum des Systems muss nicht notwendigerweise endlich, jedoch endlich repräsentierbar sein. Die Spezifikation ist die nachzuweisende formale Eigenschaft des Systems, gegeben zum Beispiel durch eine temporal-logische Formel oder durch einen Beobachtungsautomaten. (de)
  • Model Checking (deutsch auch Modellprüfung) ist ein Verfahrenzur vollautomatischen Verifikation einer Systembeschreibung (Modell) gegen eine Spezifikation (Formel).Der Begriff ist motiviert durch die mathematische Formulierung des Problems:Für eine gegebene Systembeschreibung und eine gegebene logische Eigenschaft , prüfe, ob Modell ist für (formal ). Das Verfahren wird als vollautomatisch bezeichnet, weil es keiner Benutzerinteraktion bedarf (im Gegensatz zu einigen deduktiven Verfahren, wie zum Beispiel interaktives Theorembeweisen). Die Systembeschreibung erfolgt in einer formalen Sprache, zum Beispiel durch ein Programm, einen endlichen Automaten oder ein Transitionssystem. Der Zustandsraum des Systems muss nicht notwendigerweise endlich, jedoch endlich repräsentierbar sein. Die Spezifikation ist die nachzuweisende formale Eigenschaft des Systems, gegeben zum Beispiel durch eine temporal-logische Formel oder durch einen Beobachtungsautomaten. (de)
dbo:wikiPageExternalLink
dbo:wikiPageID
  • 333489 (xsd:integer)
dbo:wikiPageRevisionID
  • 133235584 (xsd:integer)
dct:subject
rdfs:comment
  • Model Checking (deutsch auch Modellprüfung) ist ein Verfahrenzur vollautomatischen Verifikation einer Systembeschreibung (Modell) gegen eine Spezifikation (Formel).Der Begriff ist motiviert durch die mathematische Formulierung des Problems:Für eine gegebene Systembeschreibung und eine gegebene logische Eigenschaft , prüfe, ob Modell ist für (formal ). (de)
  • Model Checking (deutsch auch Modellprüfung) ist ein Verfahrenzur vollautomatischen Verifikation einer Systembeschreibung (Modell) gegen eine Spezifikation (Formel).Der Begriff ist motiviert durch die mathematische Formulierung des Problems:Für eine gegebene Systembeschreibung und eine gegebene logische Eigenschaft , prüfe, ob Modell ist für (formal ). (de)
rdfs:label
  • Model Checking (de)
  • Model Checking (de)
owl:sameAs
prov:wasDerivedFrom
foaf:isPrimaryTopicOf
is dbo:wikiPageRedirects of
is foaf:primaryTopic of