| http://dbpedia.org/ontology/abstract
|
V oblasti počítačových systémů formální verifikace dokazuje nebo vyvrací správnost systému vzhledem k dané formální specifikaci nebo vlastnosti, použitím matematických formálních metod.
, La verificación formal, en ingeniería y en … La verificación formal, en ingeniería y en computación, es un método de validación estática (se valida a través del propio código del programa, a partir de una abstracción o de una representación simbólica) en el que, partiendo de un conjunto axiomático, reglas de inferencia y algún lenguaje lógico (como la lógica de primer orden), se puede encontrar una demostración o prueba de corrección de un programa, algoritmo, etc, aunque también se puede encontrar su refutación.Es un método necesario para probar cualquier programa o teoría pero, aunque sea satisfactoria, no asegura que la solución sea del todo correcta. Dentro de la computación, la verificación es usada para estudiar los distintos sistemas software (en código fuente), sistemas combinacionales, circuitos digitales, etc. Uno de los precursores de la verificación fue Edsger Dijkstra que, mostrando mucho interés en ella durante los 70, publicó el libro "A Discipline of Programming", en el cual, presentó su método de desarrollo sistemático de programas junto con sus pruebas de corrección, todos ellos basados en la verificación formal.s ellos basados en la verificación formal.
, Στα συστήματα υλικού και λογισμικού, η τυπική επαλήθευση (formal verification) είναι η απόδειξη της των αλγορίθμων ενός συστήματος σύμφωνα με κάποια ή ιδιότητα, με τη χρήση των μαθηματικών.
, Верифіка́ція форма́льна — в інформаційних технологіях, доказ, або заперечення відповідності системи у відношенні до певної формальної специфікації або характеристики, із використанням формальних методів математики.
, Формальная верификация или формальное дока … Формальная верификация или формальное доказательство — формальное доказательство соответствия или несоответствия предмета верификации его формальному описанию. Предметом выступают алгоритмы, программы и другие доказательства. Из-за рутинности даже простой формальной верификации и теоретической возможности их полной автоматизации под формальной верификацией обычно подразумевают автоматическую верификацию с помощью программы.атическую верификацию с помощью программы.
, Egiaztapen formala (hardware eta softwaree … Egiaztapen formala (hardware eta softwareen sistemei dagokionez), algoritmo jakin bat espezifikazio formal batekiko zuzena dela frogatzean datza, horretarako matematikak eskaintzen dituen metodo formalak medio direlarik. Algoritmo hauen egiaztapena gauzatzako, dagokion sistemaren (hardware edo softwarea, kasuak kasu) eredu matematiko abstraktu batean oinarritzen den bat eman behar da. Hauek dira sistemen eredutzat erabiltzen diren eredu matematiko batzuk: egoera makina finituak, , , , , , , eta . egoera makina finituak, , , , , , , eta .
, Formell verifiering innefattar att bevisa eller motbevisa korrektheten för avsedda algoritmer som ligger till grund för ett system med avseende på en viss formell specifikation eller egenskap, med hjälp av formella matematiska metoder.
, Verificação formal é a prova matemática da conformidade de um algoritmo a certa especificação formal ou propriedade, usando métodos formais.
, 在计算机硬件（特别是集成电路）和软件系统的设计过程中，形式验证的含义是根据某个或某些形式规范或属性，使用数学的方法证明其正确性或非正确性。
, Nell'ambito dei sistemi software e hardwar … Nell'ambito dei sistemi software e hardware la verifica formale è l'azione di provare o smentire matematicamente la correttezza degli algoritmi di un sistema controllando che rispettino specifiche formali o proprietà, usando metodi formali matematici. Risulta utile per fornire la correttezza di sistemi come: protocolli crittografici, circuiti combinatori, circuiti digitali con memoria interna e software espressi in codice sorgente. La verifica di questi sistemi è fatta fornendo una prova formale di un modello matematico astratto del sistema, la corrispondenza tra il modello matematico e la natura del sistema è conosciuta sin dalla costruzione dello stesso.Nei modelli si usano di solito: macchina a stati finiti, sistema a transizione di stati, rete di Petri, Sistema addizionale di vettori, teoria degli automi temporizzata, teoria degli automi ibrida, calcolo algebrico, semantica formale dei linguaggi di programmazione come la semantica operazionale, la semantica denotazionale, la semantica assiomatica e la logica di Hoare.emantica assiomatica e la logica di Hoare.
, On parle de vérification formelle quand on … On parle de vérification formelle quand on utilise les techniques des méthodes formelles. Dans le monde industriel, la vérification formelle est utilisée aussi bien pour vérifier du code informatique (bon fonctionnement des programmes avant la livraison du logiciel), que du code de circuits électroniques.
* Portail de l’informatique
* Portail de l'informatique théoriqueque
* Portail de l'informatique théorique
, In the context of hardware and software sy … In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal methods of mathematics. Formal verification can be helpful in proving the correctness of systems such as: cryptographic protocols, combinational circuits, digital circuits with internal memory, and software expressed as source code. The verification of these systems is done by providing a formal proof on an abstract mathematical model of the system, the correspondence between the mathematical model and the nature of the system being otherwise known by construction. Examples of mathematical objects often used to model systems are: finite-state machines, labelled transition systems, Petri nets, vector addition systems, timed automata, hybrid automata, process algebra, formal semantics of programming languages such as operational semantics, denotational semantics, axiomatic semantics and Hoare logic.tics, axiomatic semantics and Hoare logic.
, Weryfikacja formalna – stwierdzenie poprawności algorytmu w oparciu o formalne metody matematyczne.
, 形式的検証（けいしきてきけんしょう）とは、ハードウェアおよびソフトウェアのシステムにおいて形式手法や数学を利用し、何らかの形式仕様記述やプロパティに照らしてシステムが正しいことを証明したり、逆に正しくないことを証明することである。 完全な形式的検証は、システムにプログラミングの誤りがないことを保証する既知の唯一の方法である。“”ACMシンポジウムで発表された論文の要約から
|
| http://dbpedia.org/ontology/wikiPageID
|
270054
|
| http://dbpedia.org/ontology/wikiPageLength
|
15914
|
| http://dbpedia.org/ontology/wikiPageRevisionID
|
1119112027
|
| http://dbpedia.org/ontology/wikiPageWikiLink
|
http://dbpedia.org/resource/Finite-state_machine +
, http://dbpedia.org/resource/Software_industry +
, http://dbpedia.org/resource/Oracle_%28computability%29 +
, http://dbpedia.org/resource/Correctness_%28computer_science%29 +
, http://dbpedia.org/resource/Vector_addition_system +
, http://dbpedia.org/resource/Software_system +
, http://dbpedia.org/resource/Verification_and_validation +
, http://dbpedia.org/resource/L4_microkernel_family +
, http://dbpedia.org/resource/ACL2 +
, http://dbpedia.org/resource/Symbolic_simulation +
, http://dbpedia.org/resource/SPARK_%28programming_language%29 +
, http://dbpedia.org/resource/Mathematical_model +
, http://dbpedia.org/resource/Dependent_types +
, http://dbpedia.org/resource/Operational_semantics +
, http://dbpedia.org/resource/Algorithm +
, http://dbpedia.org/resource/Automated_theorem_proving +
, http://dbpedia.org/resource/Labelled_transition_system +
, http://dbpedia.org/resource/Coq +
, http://dbpedia.org/resource/Correct_by_construction +
, http://dbpedia.org/resource/Temporal_logic_in_finite-state_verification +
, http://dbpedia.org/resource/Hybrid_automata +
, http://dbpedia.org/resource/Denotational_semantics +
, http://dbpedia.org/resource/Temporal_logic +
, http://dbpedia.org/resource/Type_system +
, http://dbpedia.org/resource/Static_code_analysis +
, http://dbpedia.org/resource/Process_algebra +
, http://dbpedia.org/resource/Functional_programming +
, http://dbpedia.org/resource/Formal_specification +
, http://dbpedia.org/resource/Formal_proof +
, http://dbpedia.org/resource/Formal_methods +
, http://dbpedia.org/resource/Category:Theoretical_computer_science +
, http://dbpedia.org/resource/Hardware_industry +
, http://dbpedia.org/resource/Category:Formal_methods +
, http://dbpedia.org/resource/Proof_assistant +
, http://dbpedia.org/resource/Combinational_logic +
, http://dbpedia.org/resource/CompCert +
, http://dbpedia.org/resource/Runtime_verification +
, http://dbpedia.org/resource/Termination_analysis +
, http://dbpedia.org/resource/Property_Specification_Language +
, http://dbpedia.org/resource/Satisfiability_modulo_theories +
, http://dbpedia.org/resource/East_China_Normal_University +
, http://dbpedia.org/resource/Computational_tree_logic +
, http://dbpedia.org/resource/Intelligent_verification +
, http://dbpedia.org/resource/Proof_checker +
, http://dbpedia.org/resource/SystemVerilog +
, http://dbpedia.org/resource/Cryptographic_protocol +
, http://dbpedia.org/resource/Post-silicon_validation +
, http://dbpedia.org/resource/Category:Electronic_circuit_verification +
, http://dbpedia.org/resource/Decidability_%28logic%29 +
, http://dbpedia.org/resource/Mathematics +
, http://dbpedia.org/resource/Formal_equivalence_checking +
, http://dbpedia.org/resource/Axiomatic_semantics +
, http://dbpedia.org/resource/State_space_enumeration +
, http://dbpedia.org/resource/Model_checking +
, http://dbpedia.org/resource/Prototype_Verification_System +
, http://dbpedia.org/resource/List_of_model_checking_tools +
, http://dbpedia.org/resource/Digital_circuit +
, http://dbpedia.org/resource/Finite_model_theory +
, http://dbpedia.org/resource/Hoare_logic +
, http://dbpedia.org/resource/Genetic_programming +
, http://dbpedia.org/resource/Linear_temporal_logic +
, http://dbpedia.org/resource/Soundness +
, http://dbpedia.org/resource/Petri_net +
, http://dbpedia.org/resource/Cisco +
, http://dbpedia.org/resource/List_of_important_publications_in_theoretical_computer_science +
, http://dbpedia.org/resource/Abstract_interpretation +
, http://dbpedia.org/resource/Mathematical_proof +
, http://dbpedia.org/resource/Bird%E2%80%93Meertens_formalism +
, http://dbpedia.org/resource/Program_synthesis +
, http://dbpedia.org/resource/Program_derivation +
, http://dbpedia.org/resource/Category:Logic_in_computer_science +
, http://dbpedia.org/resource/SYSGO +
, http://dbpedia.org/resource/Source_code +
, http://dbpedia.org/resource/Use_case +
, http://dbpedia.org/resource/Isabelle_%28theorem_prover%29 +
, http://dbpedia.org/resource/SeL4 +
, http://dbpedia.org/resource/HOL_theorem_prover +
, http://dbpedia.org/resource/Integrity_%28operating_system%29 +
, http://dbpedia.org/resource/Timed_automaton +
, http://dbpedia.org/resource/PikeOS +
|
| http://dbpedia.org/property/wikiPageUsesTemplate
|
http://dbpedia.org/resource/Template:Main +
, http://dbpedia.org/resource/Template:Hatnote_group +
, http://dbpedia.org/resource/Template:Cn +
, http://dbpedia.org/resource/Template:Use_mdy_dates +
, http://dbpedia.org/resource/Template:More_citations_needed +
, http://dbpedia.org/resource/Template:Citation_needed +
, http://dbpedia.org/resource/Template:Distinguish +
, http://dbpedia.org/resource/Template:As_of +
, http://dbpedia.org/resource/Template:Reflist +
, http://dbpedia.org/resource/Template:Short_description +
, http://dbpedia.org/resource/Template:Cleanup +
, http://dbpedia.org/resource/Template:Wiktionary +
, http://dbpedia.org/resource/Template:For +
|
| http://purl.org/dc/terms/subject
|
http://dbpedia.org/resource/Category:Theoretical_computer_science +
, http://dbpedia.org/resource/Category:Logic_in_computer_science +
, http://dbpedia.org/resource/Category:Electronic_circuit_verification +
, http://dbpedia.org/resource/Category:Formal_methods +
|
| http://purl.org/linguistics/gold/hypernym
|
http://dbpedia.org/resource/Act +
|
| http://www.w3.org/ns/prov#wasDerivedFrom
|
http://en.wikipedia.org/wiki/Formal_verification?oldid=1119112027&ns=0 +
|
| http://xmlns.com/foaf/0.1/isPrimaryTopicOf
|
http://en.wikipedia.org/wiki/Formal_verification +
|
| owl:differentFrom |
http://dbpedia.org/resource/Verificationism +
|
| owl:sameAs |
http://zh.dbpedia.org/resource/%E5%BD%A2%E5%BC%8F%E9%AA%8C%E8%AF%81 +
, http://pl.dbpedia.org/resource/Weryfikacja_formalna +
, http://pt.dbpedia.org/resource/Verifica%C3%A7%C3%A3o_formal +
, http://uk.dbpedia.org/resource/%D0%A4%D0%BE%D1%80%D0%BC%D0%B0%D0%BB%D1%8C%D0%BD%D0%B0_%D0%B2%D0%B5%D1%80%D0%B8%D1%84%D1%96%D0%BA%D0%B0%D1%86%D1%96%D1%8F +
, http://rdf.freebase.com/ns/m.01nswj +
, http://ja.dbpedia.org/resource/%E5%BD%A2%E5%BC%8F%E7%9A%84%E6%A4%9C%E8%A8%BC +
, http://tr.dbpedia.org/resource/Program_do%C4%9Frulama +
, http://dbpedia.org/resource/Formal_verification +
, http://it.dbpedia.org/resource/Verifica_formale +
, http://he.dbpedia.org/resource/%D7%90%D7%99%D7%9E%D7%95%D7%AA_%D7%AA%D7%95%D7%9B%D7%A0%D7%94 +
, https://global.dbpedia.org/id/hcnQ +
, http://cs.dbpedia.org/resource/Form%C3%A1ln%C3%AD_verifikace +
, http://sv.dbpedia.org/resource/Formell_verifiering +
, http://el.dbpedia.org/resource/%CE%A4%CF%85%CF%80%CE%B9%CE%BA%CE%AE_%CE%B5%CF%80%CE%B1%CE%BB%CE%AE%CE%B8%CE%B5%CF%85%CF%83%CE%B7 +
, http://fa.dbpedia.org/resource/%D8%AF%D8%B1%D8%B3%D8%AA%DB%8C%E2%80%8C%DB%8C%D8%A7%D8%A8%DB%8C_%D8%B5%D9%88%D8%B1%DB%8C +
, http://yago-knowledge.org/resource/Formal_verification +
, http://www.wikidata.org/entity/Q173326 +
, http://fr.dbpedia.org/resource/V%C3%A9rification_formelle +
, http://ru.dbpedia.org/resource/%D0%A4%D0%BE%D1%80%D0%BC%D0%B0%D0%BB%D1%8C%D0%BD%D0%B0%D1%8F_%D0%B2%D0%B5%D1%80%D0%B8%D1%84%D0%B8%D0%BA%D0%B0%D1%86%D0%B8%D1%8F +
, http://eu.dbpedia.org/resource/Egiaztapen_formala_%28informatika%29 +
, http://es.dbpedia.org/resource/Verificaci%C3%B3n_formal +
, http://simple.dbpedia.org/resource/Formal_verification +
|
| rdf:type |
http://dbpedia.org/ontology/MusicGenre +
, http://dbpedia.org/class/yago/Know-how105616786 +
, http://dbpedia.org/class/yago/Method105660268 +
, http://dbpedia.org/class/yago/Abstraction100002137 +
, http://dbpedia.org/ontology/Band +
, http://dbpedia.org/class/yago/Ability105616246 +
, http://dbpedia.org/class/yago/PsychologicalFeature100023100 +
, http://dbpedia.org/class/yago/WikicatFormalMethods +
, http://dbpedia.org/class/yago/Cognition100023271 +
|
| rdfs:comment |
V oblasti počítačových systémů formální verifikace dokazuje nebo vyvrací správnost systému vzhledem k dané formální specifikaci nebo vlastnosti, použitím matematických formálních metod.
, Верифіка́ція форма́льна — в інформаційних технологіях, доказ, або заперечення відповідності системи у відношенні до певної формальної специфікації або характеристики, із використанням формальних методів математики.
, Nell'ambito dei sistemi software e hardwar … Nell'ambito dei sistemi software e hardware la verifica formale è l'azione di provare o smentire matematicamente la correttezza degli algoritmi di un sistema controllando che rispettino specifiche formali o proprietà, usando metodi formali matematici. Risulta utile per fornire la correttezza di sistemi come: protocolli crittografici, circuiti combinatori, circuiti digitali con memoria interna e software espressi in codice sorgente.na e software espressi in codice sorgente.
, 在计算机硬件（特别是集成电路）和软件系统的设计过程中，形式验证的含义是根据某个或某些形式规范或属性，使用数学的方法证明其正确性或非正确性。
, Формальная верификация или формальное дока … Формальная верификация или формальное доказательство — формальное доказательство соответствия или несоответствия предмета верификации его формальному описанию. Предметом выступают алгоритмы, программы и другие доказательства. Из-за рутинности даже простой формальной верификации и теоретической возможности их полной автоматизации под формальной верификацией обычно подразумевают автоматическую верификацию с помощью программы.атическую верификацию с помощью программы.
, La verificación formal, en ingeniería y en … La verificación formal, en ingeniería y en computación, es un método de validación estática (se valida a través del propio código del programa, a partir de una abstracción o de una representación simbólica) en el que, partiendo de un conjunto axiomático, reglas de inferencia y algún lenguaje lógico (como la lógica de primer orden), se puede encontrar una demostración o prueba de corrección de un programa, algoritmo, etc, aunque también se puede encontrar su refutación.Es un método necesario para probar cualquier programa o teoría pero, aunque sea satisfactoria, no asegura que la solución sea del todo correcta.ura que la solución sea del todo correcta.
, Στα συστήματα υλικού και λογισμικού, η τυπική επαλήθευση (formal verification) είναι η απόδειξη της των αλγορίθμων ενός συστήματος σύμφωνα με κάποια ή ιδιότητα, με τη χρήση των μαθηματικών.
, In the context of hardware and software sy … In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal methods of mathematics. Formal verification can be helpful in proving the correctness of systems such as: cryptographic protocols, combinational circuits, digital circuits with internal memory, and software expressed as source code.ry, and software expressed as source code.
, Verificação formal é a prova matemática da conformidade de um algoritmo a certa especificação formal ou propriedade, usando métodos formais.
, Egiaztapen formala (hardware eta softwaree … Egiaztapen formala (hardware eta softwareen sistemei dagokionez), algoritmo jakin bat espezifikazio formal batekiko zuzena dela frogatzean datza, horretarako matematikak eskaintzen dituen metodo formalak medio direlarik. Algoritmo hauen egiaztapena gauzatzako, dagokion sistemaren (hardware edo softwarea, kasuak kasu) eredu matematiko abstraktu batean oinarritzen den bat eman behar da. Hauek dira sistemen eredutzat erabiltzen diren eredu matematiko batzuk: egoera makina finituak, , , , , , , eta . egoera makina finituak, , , , , , , eta .
, On parle de vérification formelle quand on … On parle de vérification formelle quand on utilise les techniques des méthodes formelles. Dans le monde industriel, la vérification formelle est utilisée aussi bien pour vérifier du code informatique (bon fonctionnement des programmes avant la livraison du logiciel), que du code de circuits électroniques.
* Portail de l’informatique
* Portail de l'informatique théoriqueque
* Portail de l'informatique théorique
, Formell verifiering innefattar att bevisa eller motbevisa korrektheten för avsedda algoritmer som ligger till grund för ett system med avseende på en viss formell specifikation eller egenskap, med hjälp av formella matematiska metoder.
, Weryfikacja formalna – stwierdzenie poprawności algorytmu w oparciu o formalne metody matematyczne.
, 形式的検証（けいしきてきけんしょう）とは、ハードウェアおよびソフトウェアのシステムにおいて形式手法や数学を利用し、何らかの形式仕様記述やプロパティに照らしてシステムが正しいことを証明したり、逆に正しくないことを証明することである。 完全な形式的検証は、システムにプログラミングの誤りがないことを保証する既知の唯一の方法である。“”ACMシンポジウムで発表された論文の要約から
|
| rdfs:label |
形式验证
, Formal verification
, Verificación formal
, Egiaztapen formala (informatika)
, Weryfikacja formalna
, Verifica formale
, Formální verifikace
, Формальная верификация
, Формальна верифікація
, Verificação formal
, 形式的検証
, Formell verifiering
, Vérification formelle
, Τυπική επαλήθευση
|
