@prefix rdf: . @prefix dbpedia: . @prefix ns2: . dbpedia:Model_checking rdf:type ns2:ModelCheckers , ns2:FormalMethods . @prefix owl: . dbpedia:Model_checking owl:sameAs . @prefix foaf: . @prefix ns5: . dbpedia:Model_checking foaf:page ns5:Model_checking . @prefix dbpprop: . dbpedia:Model_checking dbpprop:reference , , . @prefix rdfs: . dbpedia:Model_checking rdfs:label "\u30E2\u30C7\u30EB\u691C\u67FB"@ja , "Model checking"@it , "Model checking"@fr , "Model Checking"@pt , "\u041F\u0440\u043E\u0432\u0435\u0440\u043A\u0430 \u043C\u043E\u0434\u0435\u043B\u0435\u0439"@ru , "Model Checking"@de , "Model checking"@en , "Model checking"@es ; dbpprop:abstract "No campo da Ci\u00EAncia da Computa\u00E7\u00E3o, Verifica\u00E7\u00E3o de Modelos (do ingl\u00EAs, Model Checking) refere-se ao problema de testar automaticamente se um modelo que representa um sistema atende a uma dada especifica\u00E7\u00E3o. Tipicamente estes s\u00E3o sistemas de hardware, software e protocolos de comunica\u00E7\u00E3o e suas especifica\u00E7\u00F5es cont\u00E9m requerimentos de seguran\u00E7a como a aus\u00EAncia de deadlocks e comportamentos similares que podem levar o sistema a falhar."@pt , "Model Checking (deutsch auch Modellpr\u00FCfung) ist ein Verfahren zur vollautomatischen Verifikation einer Systembeschreibung (Modell) gegen eine Spezifikation (Formel). Der Begriff ist motiviert durch die mathematische Formulierung des Problems: F\u00FCr eine gegebene Systembeschreibung <math>M</math> und eine gegebene logische Eigenschaft <math>\\phi</math>, pr\u00FCfe, ob <math>M</math> Modell ist f\u00FCr <math>\\phi</math> (formal <math>M \\models \\varphi</math>). 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 durch ein Transitionssystem. Der Zustandsraum des Systems muss nicht notwendigerweise endlich, jedoch endlich repr\u00E4sentierbar sein. Die Spezifikation ist die nachzuweisende formale Eigenschaft des Systems, gegeben zum Beispiel durch eine temporal-logische Formel oder durch einen Beobachtungsautomaten."@de , "In the field of logic in computer science, model checking refers to the following problem: Given a model of a system, test automatically whether this model meets a given specification. Typically, the systems one has in mind are hardware or software systems, and the specification contains safety requirements such as the absence of deadlocks and similar critical states that can cause the system to crash. In order to solve such a problem algorithmically, both the model of the system and the specification are formulated in some precise mathematical language: To this end, it is formulated as a task in Logic, namely to check whether a given structure satisfies a given logical formula. The concept is general and applies to all kinds of logics and suitable structures. A simple model-checking problem is verifying whether a given formula in the propositional logic is satisfied by a given structure."@en , "\u041F\u0440\u043E\u0432\u0435\u0440\u043A\u0430 \u043C\u043E\u0434\u0435\u043B\u0435\u0439 (\u043F\u0440\u043E\u0432\u0435\u0440\u043A\u0430 \u043D\u0430 \u043C\u043E\u0434\u0435\u043B\u0438, \u0430\u043D\u0433\u043B. model checking) \u2014 \u043C\u0435\u0442\u043E\u0434 \u0430\u0432\u0442\u043E\u043C\u0430\u0442\u0438\u0447\u0435\u0441\u043A\u043E\u0439 \u0444\u043E\u0440\u043C\u0430\u043B\u044C\u043D\u043E\u0439 \u0432\u0435\u0440\u0438\u0444\u0438\u043A\u0430\u0446\u0438\u0438 \u043F\u0430\u0440\u0430\u043B\u043B\u0435\u043B\u044C\u043D\u044B\u0445 \u0441\u0438\u0441\u0442\u0435\u043C \u0441 \u043A\u043E\u043D\u0435\u0447\u043D\u044B\u043C \u0447\u0438\u0441\u043B\u043E\u043C \u0441\u043E\u0441\u0442\u043E\u044F\u043D\u0438\u0439. \u041F\u043E\u0437\u0432\u043E\u043B\u044F\u0435\u0442 \u043F\u0440\u043E\u0432\u0435\u0440\u0438\u0442\u044C \u0443\u0434\u043E\u0432\u043B\u0435\u0442\u0432\u043E\u0440\u044F\u0435\u0442 \u043B\u0438 \u0437\u0430\u0434\u0430\u043D\u043D\u0430\u044F \u043C\u043E\u0434\u0435\u043B\u044C \u0441\u0438\u0441\u0442\u0435\u043C\u044B \u0444\u043E\u0440\u043C\u0430\u043B\u044C\u043D\u044B\u043C \u0441\u043F\u0435\u0446\u0438\u0444\u0438\u043A\u0430\u0446\u0438\u044F\u043C. \u0412 \u043A\u0430\u0447\u0435\u0441\u0442\u0432\u0435 \u043C\u043E\u0434\u0435\u043B\u0438 \u043E\u0431\u044B\u0447\u043D\u043E \u0438\u0441\u043F\u043E\u043B\u044C\u0437\u0443\u0435\u0442\u0441\u044F, \u0442\u0430\u043A \u043D\u0430\u0437\u044B\u0432\u0430\u0435\u043C\u0430\u044F, \u043C\u043E\u0434\u0435\u043B\u044C \u041A\u0440\u0438\u043F\u043A\u0435, \u043A\u043E\u0442\u043E\u0440\u0430\u044F \u0444\u043E\u0440\u043C\u0430\u043B\u044C\u043D\u043E \u0437\u0430\u0434\u0430\u0451\u0442\u0441\u044F \u0441\u043B\u0435\u0434\u0443\u044E\u0449\u0438\u043C \u043E\u0431\u0440\u0430\u0437\u043E\u043C: <math>M = \\left(S, S_0, R, L\\right)</math>, \u0433\u0434\u0435 <math>S</math> \u2014 \u043C\u043D\u043E\u0436\u0435\u0441\u0442\u0432\u043E \u0441\u043E\u0441\u0442\u043E\u044F\u043D\u0438\u0439, <math>S_0</math> \u2014 \u043C\u043D\u043E\u0436\u0435\u0441\u0442\u0432\u043E \u043D\u0430\u0447\u0430\u043B\u044C\u043D\u044B\u0445 \u0441\u043E\u0441\u0442\u043E\u044F\u043D\u0438\u0439, <math>R \\subseteq S \\times S</math> \u2014 \u043E\u0442\u043D\u043E\u0448\u0435\u043D\u0438\u0435 \u043F\u0435\u0440\u0435\u0445\u043E\u0434\u043E\u0432, <math>L: S \\rightarrow 2^{AP}</math> \u2014 \u0444\u0443\u043D\u043A\u0446\u0438\u044F \u0440\u0430\u0437\u043C\u0435\u0442\u043A\u0438. \u041E\u0431\u044B\u0447\u043D\u043E \u0441\u043F\u0435\u0446\u0438\u0444\u0438\u043A\u0430\u0446\u0438\u0438 \u0437\u0430\u0434\u0430\u044E\u0442\u0441\u044F \u043D\u0430 \u044F\u0437\u044B\u043A\u0435 \u0444\u043E\u0440\u043C\u0430\u043B\u044C\u043D\u043E\u0439 \u043B\u043E\u0433\u0438\u043A\u0438. \u0414\u043B\u044F \u0441\u043F\u0435\u0446\u0438\u0444\u0438\u043A\u0430\u0446\u0438\u0438 \u0430\u043F\u043F\u0430\u0440\u0430\u0442\u043D\u043E\u0433\u043E \u0438 \u043F\u0440\u043E\u0433\u0440\u0430\u043C\u043C\u043D\u043E\u0433\u043E \u043E\u0431\u0435\u0441\u043F\u0435\u0447\u0435\u043D\u0438\u044F, \u043A\u0430\u043A \u043F\u0440\u0430\u0432\u0438\u043B\u043E, \u043F\u0440\u0438\u043C\u0435\u043D\u044F\u044E\u0442 \u0442\u0435\u043C\u043F\u043E\u0440\u0430\u043B\u044C\u043D\u0443\u044E \u043B\u043E\u0433\u0438\u043A\u0443 \u2014 \u0441\u043F\u0435\u0446\u0438\u0430\u043B\u044C\u043D\u044B\u0439 \u044F\u0437\u044B\u043A, \u043F\u043E\u0437\u0432\u043E\u043B\u044F\u044E\u0449\u0438\u0439 \u043E\u043F\u0438\u0441\u044B\u0432\u0430\u0442\u044C \u043F\u043E\u0432\u0435\u0434\u0435\u043D\u0438\u0435 \u0441\u0438\u0441\u0442\u0435\u043C\u044B \u0432\u043E \u0432\u0440\u0435\u043C\u0435\u043D\u0438. \u0412\u0430\u0436\u043D\u044B\u043C \u0432\u043E\u043F\u0440\u043E\u0441\u043E\u043C \u0441\u043F\u0435\u0446\u0438\u0444\u0438\u043A\u0430\u0446\u0438\u0438 \u044F\u0432\u043B\u044F\u0435\u0442\u0441\u044F \u043F\u043E\u043B\u043D\u043E\u0442\u0430. \u041C\u0435\u0442\u043E\u0434 \u043F\u0440\u043E\u0432\u0435\u0440\u043A\u0438 \u043D\u0430 \u043C\u043E\u0434\u0435\u043B\u0438 \u043F\u043E\u0437\u0432\u043E\u043B\u044F\u0435\u0442 \u0443\u0431\u0435\u0434\u0438\u0442\u044C\u0441\u044F, \u0447\u0442\u043E \u043C\u043E\u0434\u0435\u043B\u044C \u043F\u0440\u043E\u0435\u043A\u0442\u0438\u0440\u0443\u0435\u043C\u043E\u0439 \u0441\u0438\u0441\u0442\u0435\u043C\u044B \u0441\u043E\u043E\u0442\u0432\u0435\u0442\u0441\u0442\u0432\u0443\u0435\u0442 \u0437\u0430\u0434\u0430\u043D\u043D\u043E\u0439 \u0441\u043F\u0435\u0446\u0438\u0444\u0438\u043A\u0430\u0446\u0438\u0438, \u043E\u0434\u043D\u0430\u043A\u043E \u043E\u043F\u0440\u0435\u0434\u0435\u043B\u0438\u0442\u044C, \u043E\u0445\u0432\u0430\u0442\u044B\u0432\u0430\u0435\u0442 \u043B\u0438 \u0437\u0430\u0434\u0430\u043D\u043D\u0430\u044F \u0441\u043F\u0435\u0446\u0438\u0444\u0438\u043A\u0430\u0446\u0438\u044F \u0432\u0441\u0435 \u0441\u0432\u043E\u0439\u0441\u0442\u0432\u0430, \u043A\u043E\u0442\u043E\u0440\u044B\u043C \u0434\u043E\u043B\u0436\u043D\u0430 \u0443\u0434\u043E\u0432\u043B\u0435\u0442\u0432\u043E\u0440\u044F\u0442\u044C \u0441\u0438\u0441\u0442\u0435\u043C\u0430, \u043D\u0435\u0432\u043E\u0437\u043C\u043E\u0436\u043D\u043E. \u041E\u0441\u043D\u043E\u0432\u043D\u0430\u044F \u0442\u0440\u0443\u0434\u043D\u043E\u0441\u0442\u044C, \u043A\u043E\u0442\u043E\u0440\u0443\u044E \u043F\u0440\u0438\u0445\u043E\u0434\u0438\u0442\u0441\u044F \u043F\u0440\u0435\u043E\u0434\u043E\u043B\u0435\u0432\u0430\u0442\u044C \u0432 \u0445\u043E\u0434\u0435 \u043F\u0440\u043E\u0432\u0435\u0440\u043A\u0438 \u043D\u0430 \u043C\u043E\u0434\u0435\u043B\u0438, \u0441\u0432\u044F\u0437\u0430\u043D\u0430 \u0441 \u044D\u0444\u0444\u0435\u043A\u0442\u043E\u043C \u00AB\u043A\u043E\u043C\u0431\u0438\u043D\u0430\u0442\u043E\u0440\u043D\u043E\u0433\u043E \u0432\u0437\u0440\u044B\u0432\u0430\u00BB \u0432 \u043F\u0440\u043E\u0441\u0442\u0440\u0430\u043D\u0441\u0442\u0432\u0435 \u0441\u043E\u0441\u0442\u043E\u044F\u043D\u0438\u0439. \u042D\u0442\u0430 \u043F\u0440\u043E\u0431\u043B\u0435\u043C\u0430 \u0432\u043E\u0437\u043D\u0438\u043A\u0430\u0435\u0442 \u0432 \u0441\u0438\u0441\u0442\u0435\u043C\u0430\u0445, \u0441\u043E\u0441\u0442\u043E\u044F\u0449\u0438\u0445 \u0438\u0437 \u043C\u043D\u043E\u0433\u0438\u0445 \u043A\u043E\u043C\u043F\u043E\u043D\u0435\u043D\u0442\u043E\u0432, \u0432\u0437\u0430\u0438\u043C\u043E\u0434\u0435\u0439\u0441\u0442\u0432\u0443\u044E\u0449\u0438\u0445 \u0434\u0440\u0443\u0433 \u0441 \u0434\u0440\u0443\u0433\u043E\u043C, \u0430 \u0442\u0430\u043A\u0436\u0435 \u0432 \u0441\u0438\u0441\u0442\u0435\u043C\u0430\u0445, \u043E\u0431\u043B\u0430\u0434\u0430\u044E\u0449\u0438\u0445 \u0441\u0442\u0440\u0443\u043A\u0442\u0443\u0440\u0430\u043C\u0438 \u0434\u0430\u043D\u043D\u044B\u0445, \u0441\u043F\u043E\u0441\u043E\u0431\u043D\u044B\u0445 \u043F\u0440\u0438\u043D\u0438\u043C\u0430\u0442\u044C \u0431\u043E\u043B\u044C\u0448\u043E\u0435 \u0447\u0438\u0441\u043B\u043E \u0437\u043D\u0430\u0447\u0435\u043D\u0438\u0439."@ru , "Il model checking \u00E8 un metodo per verificare algoritmicamente i sistemi formali. Viene realizzato mediante la verifica del modello, spesso derivato dal modello hardware o software, soddisfacendo una specifica formale. La specifica \u00E8 spesso scritta come formule logiche temporali. Il modello solitamente viene espresso come un sistema di transizioni, cio\u00E8 grafo orientato formato da nodi (o vertici) e archi. Un insieme di proposizioni atomiche \u00E8 associato ad ogni nodo. I nodi rappresentano gli stati di un sistema, gli archi rappresentano le possibili esecuzioni che alterino lo stato, mentre le proposizioni atomiche rappresentano le propriet\u00E0 fondamentali che caratterizzano un punto di esecuzione. Formalmente il problema posto cos\u00EC: scelta una propriet\u00E0 da verificare, espressa come una formula logica temporale p, e un modello M avente stato iniziale s, decidere se <math>M,s \\models p</math>. Gli strumenti del model checking si scontrano con la crescita esponenziale dell'insieme degli stati, comunemente conosciuto come il problema dell'esplosione combinatoria, che deve servire a risolvere la maggior parte dei problemi del mondo reale. I ricercatori hanno sviluppato algoritmi simbolici, riduzione parziale dell'ordine, diagrammi decisionali, astrazioni e model checking al volo per risolvere il problema. Questi strumenti furono inizialmente sviluppati per la correttezza logica dei sistemi a stati discreti, ma da allora sono stati estesi per trattare sistemi real-time e forme limitate di sistemi ibridi."@it , "Con el nombre Model checking se conoce a un m\u00E9todo autom\u00E1tico de verificaci\u00F3n de un sistema formal, en la mayor\u00EDa de las ocasiones derivado del hardware o del software de un sistema inform\u00E1tico. El sistema es descrito mediante un modelo, que debe satisfacer una especificaci\u00F3n formal descrita mediante una f\u00F3rmula, a menudo escrita en alguna variedad de l\u00F3gica temporal. El modelo suele estar expresado como un sistema de transiciones, es decir, un grafo dirigido, que consta de un conjunto de v\u00E9rtices y arcos. Un conjunto de proposiciones at\u00F3micas se asocia a cada nodo. As\u00ED pues, los nodos representan los estados posibles de un sistema, los arcos posibles evoluciones del mismo, mediante ejecuciones permitidas, que alteran el estado, mientras que las proposiciones representan las propiedades b\u00E1sicas que se satisfacen en cada punto de la ejecuci\u00F3n. Formalmente, el problema se representa de la siguiente manera: Dada una propiedad deseada, expresada como una f\u00F3rmula en l\u00F3gica temporal p, y un modelo M con un estado inicial s; decidir si <math>M,s \\models p</math>. Existen herramientas autom\u00E1ticas para realizar el Model checking, basadas en t\u00E9cnicas combinatorias, explorando el espacio de estados posibles; lo que conduce al problema de explosi\u00F3n de estados. Para evitarlo, diversos investigadores han desarrollado t\u00E9cnicas basadas en algoritmos simb\u00F3licos, abstracci\u00F3n, reducci\u00F3n de orden parcial y model checking al vuelo. Inicialmente, las herramientas se dise\u00F1aron para trabajar con sistemas discretos, pero han sido extendidas a sistemas de tiempo real, o sistemas h\u00EDbridos. Los inventores del m\u00E9todo, Edmund M. Clarke, E. Allen Emerson y Joseph Sifakis, recibieron el Premio Turing 2007 de la ACM, en reconocimiento de su fundamental contribuci\u00F3n al campo de las ciencias de la computaci\u00F3n."@es , "\u30E2\u30C7\u30EB\u691C\u67FB\uFF08Model Checking\uFF09\u3068\u306F\u3001\u5F62\u5F0F\u30B7\u30B9\u30C6\u30E0\u3092\u30A2\u30EB\u30B4\u30EA\u30BA\u30E0\u7684\u306B\u691C\u8A3C\u3059\u308B\u624B\u6CD5\u3067\u3042\u308B\u3002\u30CF\u30FC\u30C9\u30A6\u30A7\u30A2\u3084\u30BD\u30D5\u30C8\u30A6\u30A7\u30A2\u306E\u8A2D\u8A08\u304B\u3089\u5C0E\u51FA\u3055\u308C\u305F\u30E2\u30C7\u30EB\u304C\u5F62\u5F0F\u4ED5\u69D8\u3092\u6E80\u8DB3\u3059\u308B\u304B\u3069\u3046\u304B\u691C\u8A3C\u3059\u308B\u3002\u4ED5\u69D8\u306F\u6642\u76F8\u8AD6\u7406\u306E\u8AD6\u7406\u5F0F\u306E\u5F62\u5F0F\u3067\u8A18\u8FF0\u3059\u308B\u3053\u3068\u304C\u591A\u3044\u3002"@ja , "Le Model Checking d\u00E9signe une famille de techniques de v\u00E9rification automatique des syst\u00E8mes dynamiques. Il s'agit de v\u00E9rifier algorithmiquement si un mod\u00E8le donn\u00E9, le syst\u00E8me lui-m\u00EAme ou une abstraction du syst\u00E8me, satisfait une sp\u00E9cification, souvent formul\u00E9e en termes de logique temporelle. On peut distinguer 2 aspects du model checking: Il peut s'agir de d\u00E9montrer qu'une certaine classe de propri\u00E9t\u00E9s, ou une certaine logique, est d\u00E9cidable, ou que sa d\u00E9cision appartient \u00E0 une certaine classe de complexit\u00E9. Il peut s'agir de rechercher des algorithmes efficaces sur des cas int\u00E9ressants en pratique, de les impl\u00E9menter, et de les appliquer \u00E0 des probl\u00E8mes r\u00E9els. Les premiers travaux sur le model checking de formules de logique temporelle ont \u00E9t\u00E9 men\u00E9s par Edmund M. Clarke et E. Allen Emerson en 1981, ainsi que par Jean-Pierre Queille et Joseph Sifakis en 1982. Clarke, Emerson et Sifakis se sont vu attribuer le Prix Turing 2007 pour leurs travaux sur le model checking."@fr ; rdfs:comment "\u041F\u0440\u043E\u0432\u0435\u0440\u043A\u0430 \u043C\u043E\u0434\u0435\u043B\u0435\u0439 (\u043F\u0440\u043E\u0432\u0435\u0440\u043A\u0430 \u043D\u0430 \u043C\u043E\u0434\u0435\u043B\u0438, \u0430\u043D\u0433\u043B. model checking) \u2014 \u043C\u0435\u0442\u043E\u0434 \u0430\u0432\u0442\u043E\u043C\u0430\u0442\u0438\u0447\u0435\u0441\u043A\u043E\u0439 \u0444\u043E\u0440\u043C\u0430\u043B\u044C\u043D\u043E\u0439 \u0432\u0435\u0440\u0438\u0444\u0438\u043A\u0430\u0446\u0438\u0438 \u043F\u0430\u0440\u0430\u043B\u043B\u0435\u043B\u044C\u043D\u044B\u0445 \u0441\u0438\u0441\u0442\u0435\u043C \u0441 \u043A\u043E\u043D\u0435\u0447\u043D\u044B\u043C \u0447\u0438\u0441\u043B\u043E\u043C \u0441\u043E\u0441\u0442\u043E\u044F\u043D\u0438\u0439. \u041F\u043E\u0437\u0432\u043E\u043B\u044F\u0435\u0442 \u043F\u0440\u043E\u0432\u0435\u0440\u0438\u0442\u044C \u0443\u0434\u043E\u0432\u043B\u0435\u0442\u0432\u043E\u0440\u044F\u0435\u0442 \u043B\u0438 \u0437\u0430\u0434\u0430\u043D\u043D\u0430\u044F \u043C\u043E\u0434\u0435\u043B\u044C \u0441\u0438\u0441\u0442\u0435\u043C\u044B \u0444\u043E\u0440\u043C\u0430\u043B\u044C\u043D\u044B\u043C \u0441\u043F\u0435\u0446\u0438\u0444\u0438\u043A\u0430\u0446\u0438\u044F\u043C."@ru , "Model Checking (deutsch auch Modellpr\u00FCfung) ist ein Verfahren zur vollautomatischen Verifikation einer Systembeschreibung (Modell) gegen eine Spezifikation (Formel)."@de , "Il model checking \u00E8 un metodo per verificare algoritmicamente i sistemi formali. Viene realizzato mediante la verifica del modello, spesso derivato dal modello hardware o software, soddisfacendo una specifica formale. La specifica \u00E8 spesso scritta come formule logiche temporali. Il modello solitamente viene espresso come un sistema di transizioni, cio\u00E8 grafo orientato formato da nodi (o vertici) e archi. Un insieme di proposizioni atomiche \u00E8 associato ad ogni nodo."@it , "Con el nombre Model checking se conoce a un m\u00E9todo autom\u00E1tico de verificaci\u00F3n de un sistema formal, en la mayor\u00EDa de las ocasiones derivado del hardware o del software de un sistema inform\u00E1tico. El sistema es descrito mediante un modelo, que debe satisfacer una especificaci\u00F3n formal descrita mediante una f\u00F3rmula, a menudo escrita en alguna variedad de l\u00F3gica temporal."@es , "In the field of logic in computer science, model checking refers to the following problem: Given a model of a system, test automatically whether this model meets a given specification. Typically, the systems one has in mind are hardware or software systems, and the specification contains safety requirements such as the absence of deadlocks and similar critical states that can cause the system to crash."@en , "Le Model Checking d\u00E9signe une famille de techniques de v\u00E9rification automatique des syst\u00E8mes dynamiques. Il s'agit de v\u00E9rifier algorithmiquement si un mod\u00E8le donn\u00E9, le syst\u00E8me lui-m\u00EAme ou une abstraction du syst\u00E8me, satisfait une sp\u00E9cification, souvent formul\u00E9e en termes de logique temporelle."@fr , "\u30E2\u30C7\u30EB\u691C\u67FB\uFF08Model Checking\uFF09\u3068\u306F\u3001\u5F62\u5F0F\u30B7\u30B9\u30C6\u30E0\u3092\u30A2\u30EB\u30B4\u30EA\u30BA\u30E0\u7684\u306B\u691C\u8A3C\u3059\u308B\u624B\u6CD5\u3067\u3042\u308B\u3002\u30CF\u30FC\u30C9\u30A6\u30A7\u30A2\u3084\u30BD\u30D5\u30C8\u30A6\u30A7\u30A2\u306E\u8A2D\u8A08\u304B\u3089\u5C0E\u51FA\u3055\u308C\u305F\u30E2\u30C7\u30EB\u304C\u5F62\u5F0F\u4ED5\u69D8\u3092\u6E80\u8DB3\u3059\u308B\u304B\u3069\u3046\u304B\u691C\u8A3C\u3059\u308B\u3002\u4ED5\u69D8\u306F\u6642\u76F8\u8AD6\u7406\u306E\u8AD6\u7406\u5F0F\u306E\u5F62\u5F0F\u3067\u8A18\u8FF0\u3059\u308B\u3053\u3068\u304C\u591A\u3044\u3002"@ja , "No campo da Ci\u00EAncia da Computa\u00E7\u00E3o, Verifica\u00E7\u00E3o de Modelos (do ingl\u00EAs, Model Checking) refere-se ao problema de testar automaticamente se um modelo que representa um sistema atende a uma dada especifica\u00E7\u00E3o. Tipicamente estes s\u00E3o sistemas de hardware, software e protocolos de comunica\u00E7\u00E3o e suas especifica\u00E7\u00F5es cont\u00E9m requerimentos de seguran\u00E7a como a aus\u00EAncia de deadlocks e comportamentos similares que podem levar o sistema a falhar."@pt . @prefix skos: . @prefix ns9: . dbpedia:Model_checking skos:subject ns9:Formal_methods , ns9:Logic_in_computer_science , ns9:Finite_model_theory , ns9:Model_checkers . @prefix ns10: . dbpedia:Model_checking dbpprop:wikiPageUsesTemplate ns10:otheruses4 ; dbpprop:otheruses4Property "the checking of models in statistics"@en , "statistical model validation"@en , "checking of models in computer science"@en . @prefix ns11: . dbpedia:Model_checking dbpprop:hasPhotoCollection ns11:Model_checking . @prefix dbpedia-owl: . dbpedia:Libdmc dbpedia-owl:genre dbpedia:Model_checking . @prefix ns13: . dbpedia:Libdmc ns13:genre dbpedia:Model_checking ; dbpprop:genre dbpedia:Model_checking . dbpedia:Java_Pathfinder dbpedia-owl:genre dbpedia:Model_checking ; ns13:genre dbpedia:Model_checking ; dbpprop:genre dbpedia:Model_checking . dbpedia:Model_checkers dbpprop:redirect dbpedia:Model_checking . dbpedia:Symbolic_Model_Verification dbpprop:redirect dbpedia:Model_checking . dbpedia:Symbolic_model_verification dbpprop:redirect dbpedia:Model_checking . dbpedia:Model_checker dbpprop:redirect dbpedia:Model_checking . @prefix yago: . yago:Model_checking owl:sameAs dbpedia:Model_checking .