Model checking
http://dbpedia.org/resource/Model_checking an entity of type: Ability105616246
En informatique, la vérification de modèles, ou model checking en anglais, est le problème suivant : vérifier si le modèle d'un système (souvent informatique ou électronique) satisfait une propriété. Par exemple, on souhaite vérifier qu'un programme ne se bloque pas, qu'une variable n'est jamais nulle, etc. Généralement, la propriété est écrite dans un langage, souvent en logique temporelle. La vérification est généralement faite de manière automatique. Sur le plan pratique, la vérification de modèles est devenue, au niveau industriel, la méthode de vérification de code et de systèmes matériels la plus populaire et la plus utilisée aujourd'hui[réf. nécessaire].
rdf:langString
モデル検査（モデルけんさ、Model Checking）とは、形式システムをアルゴリズム的に検証する手法である。ハードウェアやソフトウェアの設計から導出されたモデルが形式仕様を満足するかどうか検証する。仕様は時相論理の論理式の形式で記述することが多い。
rdf:langString
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 ).
rdf:langString
Στο πεδίο της , ο όρος έλεγχος μοντέλων (Αγγλικά: model checking) αναφέρεται στο εξής πρόβλημα:Δεδομένου του μοντέλου ενός συστήματος, να ελεγχθεί με αυτόματο τρόπο αν αυτό το μοντέλο συμφωνεί με δεδομένες προδιαγραφές. Τα συστήματα τα οποία εξετάζονται συνήθως είναι συστήματα λογισμικού ή υλικού, και οι προδιαγραφές αφορούν απαιτήσεις ασφάλειας όπως η απουσία αδιεξόδων (deadlocks) και άλλων παρόμοιων επικίνδυνων καταστάσεων που μπορεί να προκαλέσουν την αποτυχία της λειτουργίας του συστήματος.
rdf:langString
La verificación de modelos (o Model checking) es un método automático de verificación de un sistema formal, en la mayoría de las ocasiones derivado del hardware o del software de un sistema informático. El sistema es descrito mediante un modelo, que debe satisfacer una especificación formal descrita mediante una fórmula, a menudo escrita en alguna variedad de lógica temporal. Formalmente, el problema se representa de la siguiente manera: Dada una propiedad deseada, expresada como una fórmula en lógica temporal p, y un modelo M con un estado inicial s; decidir si .
rdf:langString
In computer science, model checking or property checking is a method for checking whether a finite-state model of a system meets a given specification (also known as correctness). This is typically associated with hardware or software systems, where the specification contains liveness requirements (such as avoidance of livelock) as well as safety requirements (such as avoidance of states representing a system crash).
rdf:langString
Il model checking è un metodo per verificare algoritmicamente i sistemi formali. Viene realizzato mediante la verifica del modello, spesso derivato dal modello hardware o software, soddisfacendo una .La specifica è spesso scritta come formule logiche temporali. Formalmente il problema è posto così: scelta una proprietà da verificare, espressa come una formula logica temporale p, e un modello M avente stato iniziale s, decidere se .
rdf:langString
Проверка моделей (проверка на модели, англ. model checking) — метод автоматической формальной верификации параллельных систем с конечным числом состояний, позволяет проверить, удовлетворяет ли заданная модель системы формальным спецификациям. В качестве модели обычно используется так называемая модель Крипке, которая формально задаётся следующим образом: , где — множество состояний, — множество начальных состояний, — отношение переходов, — функция разметки.
rdf:langString
No campo da ciência da computação, verificação de modelos (do inglês, Model Checking) refere-se ao problema de testar automaticamente se um modelo que representa um sistema atende a uma dada especificação. Tipicamente estes são sistemas de hardware, software e protocolos de comunicação e suas especificações contém requisitos de segurança como a ausência de deadlocks e comportamentos similares que podem levar o sistema a travar. Esse deadlock é uma situação onde duas ou mais ações simultaneamente esperam a finalização da outra para sua continuação, e assim nenhuma delas pode ser concluída.
rdf:langString
Перевірка моделі або перевірка властивості полягає у вичерпній і автоматичній перевірці чи задана модель певної системи відповідає заданій специфікації. Зазвичай, мається на увазі апаратна або програмна система, а специфікація містить вимоги безпеки як-от відсутність взаємних блокувань та інших подібних критичних станів, що можуть призвести до креша. Превірка моделі — це техніка для автоматичної перевірки правильності властивостей системи зі скінченною кількістю станів.
rdf:langString
rdf:langString
Model checking
rdf:langString
Model Checking
rdf:langString
Έλεγχος μοντέλων
rdf:langString
Verificación de modelos
rdf:langString
Vérification de modèles
rdf:langString
Model checking
rdf:langString
モデル検査
rdf:langString
Проверка моделей
rdf:langString
Verificação de modelos
rdf:langString
Перевірка моделі
xsd:integer
321157
xsd:integer
1114932147
rdf:langString
Στο πεδίο της , ο όρος έλεγχος μοντέλων (Αγγλικά: model checking) αναφέρεται στο εξής πρόβλημα:Δεδομένου του μοντέλου ενός συστήματος, να ελεγχθεί με αυτόματο τρόπο αν αυτό το μοντέλο συμφωνεί με δεδομένες προδιαγραφές. Τα συστήματα τα οποία εξετάζονται συνήθως είναι συστήματα λογισμικού ή υλικού, και οι προδιαγραφές αφορούν απαιτήσεις ασφάλειας όπως η απουσία αδιεξόδων (deadlocks) και άλλων παρόμοιων επικίνδυνων καταστάσεων που μπορεί να προκαλέσουν την αποτυχία της λειτουργίας του συστήματος. Για να λυθεί ένα τέτοιο πρόβλημα αλγοριθμικά, πρέπει το μοντέλο του συστήματος και οι προδιαγραφές να διατυπώνονται με κάποια ακριβή μαθηματική γλώσσα: για αυτόν το λόγο, η διατύπωση γίνεται σε κάποια λογική και ελέγχεται αν κάποια ικανοποιεί μια δεδομένη λογική έκφραση. Αυτή η ιδέα είναι γενικότερη και εφαρμόζεται σε πολλά είδη λογικής και δομές. Ένα απλό πρόβλημα ελέγχου μοντέλων είναι να επαληθευτεί αν μια δεδομένη έκφραση της προτασιακής λογικής ικανοποιείται από μια δεδομένη δομή.
rdf:langString
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.
rdf:langString
La verificación de modelos (o Model checking) es un método automático de verificación de un sistema formal, en la mayoría de las ocasiones derivado del hardware o del software de un sistema informático. El sistema es descrito mediante un modelo, que debe satisfacer una especificación formal descrita mediante una fórmula, a menudo escrita en alguna variedad de lógica temporal. El modelo suele estar expresado como un sistema de transiciones, es decir, un grafo dirigido, que consta de un conjunto de vértices y arcos. Un conjunto de proposiciones atómicas se asocia a cada nodo. Así 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ásicas que se satisfacen en cada punto de la ejecución. Formalmente, el problema se representa de la siguiente manera: Dada una propiedad deseada, expresada como una fórmula en lógica temporal p, y un modelo M con un estado inicial s; decidir si . Existen herramientas automáticas para realizar el Model checking, basadas en técnicas combinatorias, explorando el espacio de estados posibles; lo que conduce al problema de explosión de estados. Para evitarlo, diversos investigadores han desarrollado técnicas basadas en algoritmos simbólicos, abstracción, reducción de orden parcial y model checking al vuelo. Inicialmente, las herramientas se diseñaron para trabajar con sistemas discretos, pero han sido extendidas a sistemas de tiempo real, o sistemas híbridos. Los inventores del método, Edmund M. Clarke, E. Allen Emerson y Joseph Sifakis, recibieron el Premio Turing 2007 de la ACM, en reconocimiento de su fundamental contribución al campo de las ciencias de la computación.
rdf:langString
En informatique, la vérification de modèles, ou model checking en anglais, est le problème suivant : vérifier si le modèle d'un système (souvent informatique ou électronique) satisfait une propriété. Par exemple, on souhaite vérifier qu'un programme ne se bloque pas, qu'une variable n'est jamais nulle, etc. Généralement, la propriété est écrite dans un langage, souvent en logique temporelle. La vérification est généralement faite de manière automatique. Sur le plan pratique, la vérification de modèles est devenue, au niveau industriel, la méthode de vérification de code et de systèmes matériels la plus populaire et la plus utilisée aujourd'hui[réf. nécessaire].
rdf:langString
In computer science, model checking or property checking is a method for checking whether a finite-state model of a system meets a given specification (also known as correctness). This is typically associated with hardware or software systems, where the specification contains liveness requirements (such as avoidance of livelock) as well as safety requirements (such as avoidance of states representing a system crash). In order to solve such a problem algorithmically, both the model of the system and its specification are formulated in some precise mathematical language. To this end, the problem is formulated as a task in logic, namely to check whether a structure satisfies a given logical formula. This general concept applies to many kinds of logic and many kinds of structures. A simple model-checking problem consists of verifying whether a formula in the propositional logic is satisfied by a given structure.
rdf:langString
Il model checking è un metodo per verificare algoritmicamente i sistemi formali. Viene realizzato mediante la verifica del modello, spesso derivato dal modello hardware o software, soddisfacendo una .La specifica è spesso scritta come formule logiche temporali. Il modello solitamente viene espresso come un sistema di transizioni, cioè grafo orientato formato da nodi (o vertici) e archi. Un insieme di è 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à fondamentali che caratterizzano un punto di esecuzione. Formalmente il problema è posto così: scelta una proprietà da verificare, espressa come una formula logica temporale p, e un modello M avente stato iniziale s, decidere se . 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, e 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 sistema real-time e forme limitate di sistemi ibridi.
rdf:langString
モデル検査（モデルけんさ、Model Checking）とは、形式システムをアルゴリズム的に検証する手法である。ハードウェアやソフトウェアの設計から導出されたモデルが形式仕様を満足するかどうか検証する。仕様は時相論理の論理式の形式で記述することが多い。
rdf:langString
No campo da ciência da computação, verificação de modelos (do inglês, Model Checking) refere-se ao problema de testar automaticamente se um modelo que representa um sistema atende a uma dada especificação. Tipicamente estes são sistemas de hardware, software e protocolos de comunicação e suas especificações contém requisitos de segurança como a ausência de deadlocks e comportamentos similares que podem levar o sistema a travar. Esse deadlock é uma situação onde duas ou mais ações simultaneamente esperam a finalização da outra para sua continuação, e assim nenhuma delas pode ser concluída. Para resolver tal problema de maneira algorítmica, tanto o modelo do sistema quanto a especificação são formulados em alguma linguagem matematicamente precisa. Para esta finalidade, ela deve ser formulada como uma tarefa de lógica, de forma a verificar se uma dada estrutura satisfaz uma dada fórmula lógica. O conceito é geral e se aplica a todos os tipos de lógicas e estruturas apropriadas. Um problema simples de verificação de modelo é verificar se uma dada fórmula na lógica proposicional é satisfeita por uma dada estrutura.
rdf:langString
Проверка моделей (проверка на модели, англ. model checking) — метод автоматической формальной верификации параллельных систем с конечным числом состояний, позволяет проверить, удовлетворяет ли заданная модель системы формальным спецификациям. В качестве модели обычно используется так называемая модель Крипке, которая формально задаётся следующим образом: , где — множество состояний, — множество начальных состояний, — отношение переходов, — функция разметки. Обычно спецификации задаются на языке формальной логики. Для спецификации аппаратного и программного обеспечения, как правило, применяют темпоральную логику — специальный язык, позволяющий описывать поведение системы во времени. Важным вопросом спецификации является полнота. Метод проверки на модели позволяет убедиться, что модель проектируемой системы соответствует заданной спецификации, однако определить, охватывает ли заданная спецификация все свойства, которым должна удовлетворять система, невозможно. Основная трудность, которую приходится преодолевать в ходе проверки на модели, связана с эффектом комбинаторного взрыва в пространстве состояний. Эта проблема возникает в системах, состоящих из многих компонентов, взаимодействующих друг с другом, а также в системах, обладающих структурами данных, способных принимать большое число значений.
rdf:langString
Перевірка моделі або перевірка властивості полягає у вичерпній і автоматичній перевірці чи задана модель певної системи відповідає заданій специфікації. Зазвичай, мається на увазі апаратна або програмна система, а специфікація містить вимоги безпеки як-от відсутність взаємних блокувань та інших подібних критичних станів, що можуть призвести до креша. Превірка моделі — це техніка для автоматичної перевірки правильності властивостей системи зі скінченною кількістю станів. Для того, що розв'язати таку задачу алгоритмічно, модель системи і специфікація формулюються якоюсь точною математичною мовою. Для цього проблему записують як задачу в логіці, — перевірити чи задана структура задовольняє заданій логічній формулі. Ця загальна концепція застосовна для багатьох видів логік і підхожих структур. Простим прикладом може бути перевірка чи задана формула в численні висловлень задовільнена заданою структурою.
xsd:nonNegativeInteger
24508
