Model checking (original) (raw)
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].
.jpg?width=300)
| Property | Value |
|---|---|
| dbo:abstract | Στο πεδίο της , ο όρος έλεγχος μοντέλων (Αγγλικά: model checking) αναφέρεται στο εξής πρόβλημα:Δεδομένου του μοντέλου ενός συστήματος, να ελεγχθεί με αυτόματο τρόπο αν αυτό το μοντέλο συμφωνεί με δεδομένες προδιαγραφές. Τα συστήματα τα οποία εξετάζονται συνήθως είναι συστήματα λογισμικού ή υλικού, και οι προδιαγραφές αφορούν απαιτήσεις ασφάλειας όπως η απουσία αδιεξόδων (deadlocks) και άλλων παρόμοιων επικίνδυνων καταστάσεων που μπορεί να προκαλέσουν την αποτυχία της λειτουργίας του συστήματος. Για να λυθεί ένα τέτοιο πρόβλημα αλγοριθμικά, πρέπει το μοντέλο του συστήματος και οι προδιαγραφές να διατυπώνονται με κάποια ακριβή μαθηματική γλώσσα: για αυτόν το λόγο, η διατύπωση γίνεται σε κάποια λογική και ελέγχεται αν κάποια ικανοποιεί μια δεδομένη λογική έκφραση. Αυτή η ιδέα είναι γενικότερη και εφαρμόζεται σε πολλά είδη λογικής και δομές. Ένα απλό πρόβλημα ελέγχου μοντέλων είναι να επαληθευτεί αν μια δεδομένη έκφραση της προτασιακής λογικής ικανοποιείται από μια δεδομένη δομή. (el) 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) 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. (es) 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]. (fr) 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. (en) 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. (it) モデル検査（モデルけんさ、Model Checking）とは、形式システムをアルゴリズム的に検証する手法である。ハードウェアやソフトウェアの設計から導出されたモデルが形式仕様を満足するかどうか検証する。仕様は時相論理の論理式の形式で記述することが多い。 (ja) 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. (pt) Проверка моделей (проверка на модели, англ. model checking) — метод автоматической формальной верификации параллельных систем с конечным числом состояний, позволяет проверить, удовлетворяет ли заданная модель системы формальным спецификациям. В качестве модели обычно используется так называемая модель Крипке, которая формально задаётся следующим образом: , где — множество состояний, — множество начальных состояний, — отношение переходов, — функция разметки. Обычно спецификации задаются на языке формальной логики. Для спецификации аппаратного и программного обеспечения, как правило, применяют темпоральную логику — специальный язык, позволяющий описывать поведение системы во времени. Важным вопросом спецификации является полнота. Метод проверки на модели позволяет убедиться, что модель проектируемой системы соответствует заданной спецификации, однако определить, охватывает ли заданная спецификация все свойства, которым должна удовлетворять система, невозможно. Основная трудность, которую приходится преодолевать в ходе проверки на модели, связана с эффектом комбинаторного взрыва в пространстве состояний. Эта проблема возникает в системах, состоящих из многих компонентов, взаимодействующих друг с другом, а также в системах, обладающих структурами данных, способных принимать большое число значений. (ru) Перевірка моделі або перевірка властивості полягає у вичерпній і автоматичній перевірці чи задана модель певної системи відповідає заданій специфікації. Зазвичай, мається на увазі апаратна або програмна система, а специфікація містить вимоги безпеки як-от відсутність взаємних блокувань та інших подібних критичних станів, що можуть призвести до креша. Превірка моделі — це техніка для автоматичної перевірки правильності властивостей системи зі скінченною кількістю станів. Для того, що розв'язати таку задачу алгоритмічно, модель системи і специфікація формулюються якоюсь точною математичною мовою. Для цього проблему записують як задачу в логіці, — перевірити чи задана структура задовольняє заданій логічній формулі. Ця загальна концепція застосовна для багатьох видів логік і підхожих структур. Простим прикладом може бути перевірка чи задана формула в численні висловлень задовільнена заданою структурою. (uk) |
| dbo:thumbnail | wiki-commons:Special:FilePath/Two_One_G_(cropped).jpg?width=300 |
| dbo:wikiPageExternalLink | http://spinroot.com/spin/Doc/Book_extras/ http://patterns.projects.cis.ksu.edu/documentation/patterns.shtml https://onlinelibrary.wiley.com/doi/10.1002/9780470050118.ecse247 http://cadp.inria.fr/resources/evaluator/rafmc.html http://vasy.inria.fr/ftp/publications/cadp/Mateescu-Sighireanu-03.pdf https://link.springer.com/chapter/10.1007/978-3-540-69850-0_2 https://web.archive.org/web/20110719222236/http:/patterns.projects.cis.ksu.edu/documentation/patterns.shtml http://homepages.inf.ed.ac.uk/jcb/Research/bradfield-stirling-HPA-mu-intro.ps.gz |
| dbo:wikiPageID | 321157 (xsd:integer) |
| dbo:wikiPageLength | 24508 (xsd:nonNegativeInteger) |
| dbo:wikiPageRevisionID | 1114932147 (xsd:integer) |
| dbo:wikiPageWikiLink | dbr:Cambridge_University_Press dbr:Program_analysis_(computer_science) dbr:Propositional_calculus dbr:Romeo_Model_Checker dbr:Enumeration_algorithm dbr:FDR2 dbr:MCRL2 dbr:CADP dbr:Boost_Software_License dbr:Algorithm dbr:Alloy_(specification_language) dbr:Uppaal_Model_Checker dbr:Decision_problem dbr:Degree_(graph_theory) dbr:Interpretation_(logic) dbr:Libdmc dbr:List_of_model_checking_tools dbr:Computability_theory_(computer_science) dbr:SPIN_model_checker dbr:Node_(computer_science) dbr:Bounded_expansion dbr:Correctness_(computer_science) dbr:Leslie_Lamport dbr:Livelock dbr:Logic dbr:MIT_Press dbr:State_explosion_problem dbr:Communicating_sequential_processes dbr:Computation_tree_logic dbr:Computational_complexity_theory dbr:Computer_hardware dbr:Computer_science dbr:Embedded_system dbr:Petri_net dbr:Structure_(mathematical_logic) dbr:Mutual_exclusion dbr:Automated_theorem_proving dbr:BLAST_model_checker dbr:Büchi_automaton dbr:Treewidth dbr:Turing_Award dbr:Linear_temporal_logic dbr:Graph_search dbr:Algebra_of_Communicating_Processes dbr:Amir_Pnueli dbr:ECLAIR dbr:Edge_(graph_theory) dbr:First-order_logic dbr:Formal_verification dbr:NuSMV dbr:PAT_(model_checker) dbr:Binary_decision_diagrams dbr:Directed_graph dbr:Discrete_system dbr:Formal_specification dbr:Free_variable dbr:Partial_order_reduction dbr:Refinement_(computing) dbr:Relational_database dbr:Hardware_description_language dbr:Iterative_deepening_depth-first_search dbr:Java_Pathfinder dbr:Counterexample dbr:Crash_(computing) dbr:Temporal_logic dbr:Hybrid_system dbr:Artificial_intelligence dbc:Logic_in_computer_science dbr:Abstract_interpretation dbc:Model_checking dbr:Binary_decision_diagram dbr:TAPAAL_Model_Checker dbr:TLA+ dbr:Zing_(model-checker) dbr:Don't-care_term dbr:Automated_planning_and_scheduling dbr:Boolean_satisfiability_problem dbr:CPAchecker dbr:Microsoft dbr:Message_Passing_Interface dbr:Monadic_second-order_logic dbr:Static_code_analysis dbr:Software dbr:Software_verification dbr:Vertex_(graph_theory) dbr:Satplan dbr:Software_system dbr:ISP_Formal_Verification_Tool dbr:Finite-state_machine dbr:TAPAs_model_checker dbr:J._Sifakis dbr:Petri_Nets dbr:Propositional_satisfiability dbr:UML_activity_diagram dbr:E._A._Emerson dbr:PRISM_(model_checker) dbr:Finite_state_machine dbr:Circuit_class dbr:AC0_(complexity) dbr:E._M._Clarke dbr:File:Two_One_G_(cropped).jpg |
| dbp:wikiPageUsesTemplate | dbt:About dbt:Cite_book dbt:Cite_journal dbt:Cite_web dbt:Cmn dbt:Cn dbt:Expand_section dbt:Main dbt:Refbegin dbt:Refend dbt:Refimprove dbt:Reflist dbt:Short_description dbt:Harvid dbt:Harvnb |
| dcterms:subject | dbc:Logic_in_computer_science dbc:Model_checking |
| rdf:type | yago:Ability105616246 yago:Abstraction100002137 yago:Cognition100023271 yago:Know-how105616786 yago:Method105660268 yago:PsychologicalFeature100023100 dbo:MusicGenre yago:WikicatFormalMethods |
| rdfs:comment | 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]. (fr) モデル検査（モデルけんさ、Model Checking）とは、形式システムをアルゴリズム的に検証する手法である。ハードウェアやソフトウェアの設計から導出されたモデルが形式仕様を満足するかどうか検証する。仕様は時相論理の論理式の形式で記述することが多い。 (ja) 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) αναφέρεται στο εξής πρόβλημα:Δεδομένου του μοντέλου ενός συστήματος, να ελεγχθεί με αυτόματο τρόπο αν αυτό το μοντέλο συμφωνεί με δεδομένες προδιαγραφές. Τα συστήματα τα οποία εξετάζονται συνήθως είναι συστήματα λογισμικού ή υλικού, και οι προδιαγραφές αφορούν απαιτήσεις ασφάλειας όπως η απουσία αδιεξόδων (deadlocks) και άλλων παρόμοιων επικίνδυνων καταστάσεων που μπορεί να προκαλέσουν την αποτυχία της λειτουργίας του συστήματος. (el) 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 . (es) 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). (en) 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 . (it) Проверка моделей (проверка на модели, англ. model checking) — метод автоматической формальной верификации параллельных систем с конечным числом состояний, позволяет проверить, удовлетворяет ли заданная модель системы формальным спецификациям. В качестве модели обычно используется так называемая модель Крипке, которая формально задаётся следующим образом: , где — множество состояний, — множество начальных состояний, — отношение переходов, — функция разметки. (ru) 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. (pt) Перевірка моделі або перевірка властивості полягає у вичерпній і автоматичній перевірці чи задана модель певної системи відповідає заданій специфікації. Зазвичай, мається на увазі апаратна або програмна система, а специфікація містить вимоги безпеки як-от відсутність взаємних блокувань та інших подібних критичних станів, що можуть призвести до креша. Превірка моделі — це техніка для автоматичної перевірки правильності властивостей системи зі скінченною кількістю станів. (uk) |
| rdfs:label | Model checking (en) Model Checking (de) Έλεγχος μοντέλων (el) Verificación de modelos (es) Vérification de modèles (fr) Model checking (it) モデル検査 (ja) Проверка моделей (ru) Verificação de modelos (pt) Перевірка моделі (uk) |
| owl:sameAs | freebase:Model checking wikidata:Model checking dbpedia-de:Model checking dbpedia-el:Model checking dbpedia-es:Model checking dbpedia-fa:Model checking dbpedia-fr:Model checking dbpedia-it:Model checking dbpedia-ja:Model checking dbpedia-pt:Model checking dbpedia-ru:Model checking dbpedia-sk:Model checking dbpedia-tr:Model checking dbpedia-uk:Model checking dbpedia-vi:Model checking https://global.dbpedia.org/id/YkpJ yago-res:Model checking |
| prov:wasDerivedFrom | wikipedia-en:Model_checking?oldid=1114932147&ns=0 |
| foaf:depiction | wiki-commons:Special:FilePath/Two_One_G_(cropped).jpg |
| foaf:isPrimaryTopicOf | wikipedia-en:Model_checking |
| is dbo:academicDiscipline of | dbr:Doron_A._Peled dbr:Gerard_J._Holzmann dbr:Joost-Pieter_Katoen dbr:Marta_Kwiatkowska |
| is dbo:genre of | dbr:Romeo_Model_Checker dbr:Uppaal_Model_Checker dbr:Libdmc dbr:SPIN_model_checker dbr:Murφ dbr:NuSMV dbr:PAT_(model_checker) dbr:TAPAAL_Model_Checker |
| is dbo:knownFor of | dbr:Joseph_Sifakis dbr:E._Allen_Emerson dbr:Edmund_M._Clarke |
| is dbo:nonFictionSubject of | dbr:Principles_of_Model_Checking |
| is dbo:wikiPageRedirects of | dbr:Symbolic_model_checking dbr:Temporal_Logic_in_Finite-State_Verification dbr:Symbolic_model_verification dbr:Symbolic_Model_Verification dbr:Temporal_logic_in_finite-state_verification dbr:Model_checker dbr:Model-checker dbr:Model-checking dbr:Model_checkers dbr:Modelchecking |
| is dbo:wikiPageWikiLink of | dbr:Behavior_tree dbr:Belief_revision dbr:BMC dbr:Property_Specification_Language dbr:Romeo_Model_Checker dbr:Electronic_design_automation dbr:List_of_University_of_Texas_at_Austin_faculty dbr:List_of_computer_scientists dbr:Principles_of_Model_Checking dbr:David_L._Dill dbr:David_May_(computer_scientist) dbr:Denotational_semantics dbr:Alloy_(specification_language) dbr:Joseph_Sifakis dbr:List_of_pioneers_in_computer_science dbr:Patricia_Bouyer-Decitre dbr:Culture_of_Greece dbr:DPLL_algorithm dbr:Uppaal_Model_Checker dbr:Descriptive_Complexity dbr:Doron_A._Peled dbr:Dynamic_epistemic_logic dbr:Infer_Static_Analyzer dbr:International_Conference_on_Reachability_Problems dbr:Rajeev_Alur dbr:Libdmc dbr:List_of_mathematical_logic_topics dbr:List_of_model_checking_tools dbr:Protocol_engineering dbr:Computer-assisted_proof dbr:Construction_and_Analysis_of_Distributed_Processes dbr:Craig_interpolation dbr:Anca_Muscholl dbr:And-inverter_graph dbr:Mathematical_logic dbr:SPIN_model_checker dbr:Generalized_Büchi_automaton dbr:Omega_language dbr:Orna_Grumberg dbr:Mihaela_Sighireanu dbr:Reachability_problem dbr:Timed_propositional_temporal_logic dbr:Timed_word dbr:Gerard_J._Holzmann dbr:Glossary_of_artificial_intelligence dbr:Bounded_expansion dbr:Moshe_Vardi dbr:Murφ dbr:Concolic_testing dbr:Concurrency_(computer_science) dbr:Conference_on_Implementation_and_Application_of_Automata dbr:Consistency_model dbr:Constraint_automaton dbr:Correctness_(computer_science) dbr:Thomas_W._Reps dbr:Symbolic_model_checking dbr:Logic_of_graphs dbr:Simulink dbr:Cleanroom_software_engineering dbr:Clock_(model_checking) dbr:Computation_tree_logic dbr:Computer_Aided_Verification dbr:Embedded_system dbr:Kristin_Yvonne_Rozier dbr:Static_program_analysis dbr:Automated_theorem_proving dbr:BLAST_model_checker dbr:Büchi_automaton dbr:Turing_Award dbr:Distributed_computing dbr:Game_semantics dbr:Harvard_John_A._Paulson_School_of_Engineering_and_Applied_Sciences dbr:Joost-Pieter_Katoen dbr:Linear_temporal_logic_to_Büchi_automaton dbr:Linear_time_property dbr:List_of_Carnegie_Mellon_University_people dbr:Test_design dbr:Amir_Pnueli dbr:E._Allen_Emerson dbr:ECLAIR dbr:Edmund_M._Clarke dbr:First-order_logic dbr:Formal_verification dbr:NuSMV dbr:PAT_(model_checker) dbr:Difference_bound_matrix dbr:Fair_computational_tree_logic dbr:Formal_methods dbr:Fragment_(logic) dbr:Graph_rewriting dbr:List_of_Duke_University_people dbr:PRISM_model_checker dbr:Partial_order_reduction dbr:Region_(model_checking) dbr:Helmut_Veith dbr:Java_Pathfinder dbr:Courcelle's_theorem dbr:Temporal_Logic_in_Finite-State_Verification dbr:Hybrid_automaton dbr:Abstract_interpretation dbr:Abstraction_(computer_science) dbr:Binary_decision_diagram dbr:Symbolic_artificial_intelligence dbr:TAPAAL_Model_Checker dbr:TLA+ dbr:Javier_Esparza dbr:Transition_system dbr:Widening_(computer_science) dbr:Zing dbr:Reachability_analysis dbr:Reactive_synthesis dbr:Automated_planning_and_scheduling dbr:Marta_Kwiatkowska dbr:Boolean_satisfiability_problem dbr:CPAchecker dbr:CPN-AMI dbr:CTL* dbr:Greg_Morrisett dbr:IAR_Systems dbr:Illinois_Security_Lab dbr:Kripke_structure_(model_checking) dbr:National_Technical_University_of_Athens dbr:Ofer_Strichman dbr:OpenComRTOS dbr:Rebeca_(programming_language) dbr:Red_Lizard_Software dbr:Christel_Baier dbr:Modal_μ-calculus dbr:Loop_unrolling dbr:Model-based_testing dbr:SMV dbr:Static_timing_analysis dbr:Symbolic_model_verification dbr:SIGNAL_(programming_language) dbr:SLAM_project dbr:Semantics_(computer_science) dbr:Runtime_verification dbr:Nested_word dbr:Nets_within_Nets dbr:Extended_static_checking dbr:ISP_Formal_Verification_Tool dbr:List_of_terms_relating_to_algorithms_and_data_structures dbr:List_of_tools_for_static_code_analysis dbr:Runtime_predictive_analysis dbr:Treiber_stack dbr:Symbolic_trajectory_evaluation dbr:Signal_(model_checking) dbr:Quotient_filter dbr:Semi-deterministic_Büchi_automaton dbr:Paris_Kanellakis_Award dbr:True_quantified_Boolean_formula dbr:Metric_interval_temporal_logic dbr:State_space_enumeration dbr:Symbolic_Model_Verification dbr:Temporal_logic_in_finite-state_verification dbr:Model_checker dbr:Model-checker dbr:Model-checking dbr:Model_checkers dbr:Modelchecking |
| is dbp:field of | dbr:Doron_A._Peled |
| is dbp:fields of | dbr:Gerard_J._Holzmann |
| is dbp:genre of | dbr:Romeo_Model_Checker dbr:Uppaal_Model_Checker dbr:Libdmc dbr:SPIN_model_checker dbr:Murφ dbr:NuSMV dbr:PAT_(model_checker) dbr:TAPAAL_Model_Checker |
| is dbp:knownFor of | dbr:Joseph_Sifakis dbr:Edmund_M._Clarke |
| is dbp:subject of | dbr:Principles_of_Model_Checking |
| is foaf:primaryTopic of | wikipedia-en:Model_checking |
