| comment
| - 形式的検証（けいしきてきけんしょう）とは、ハードウェアおよびソフトウェアのシステムにおいて形式手法や数学を利用し、何らかの形式仕様記述やプロパティに照らしてシステムが正しいことを証明したり、逆に正しくないことを証明することである。 完全な形式的検証は、システムにプログラミングの誤りがないことを保証する既知の唯一の方法である。“”ACMシンポジウムで発表された論文の要約から
- Weryfikacja formalna – stwierdzenie poprawności algorytmu w oparciu o formalne metody matematyczne.
- Verificação formal é a prova matemática da conformidade de um algoritmo a certa especificação formal ou propriedade, usando métodos formais.
- 在计算机硬件（特别是集成电路）和软件系统的设计过程中，形式验证的含义是根据某个或某些形式规范或属性，使用数学的方法证明其正确性或非正确性。
- 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.
- 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 .
- 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.
- Верифіка́ція форма́льна — в інформаційних технологіях, доказ, або заперечення відповідності системи у відношенні до певної формальної специфікації або характеристики, із використанням формальних методів математики.
- 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.
- 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é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.
- 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.
- Στα συστήματα υλικού και λογισμικού, η τυπική επαλήθευση (formal verification) είναι η απόδειξη της των αλγορίθμων ενός συστήματος σύμφωνα με κάποια ή ιδιότητα, με τη χρήση των μαθηματικών.
|
![[RDF Data]](/fct/images/sw-rdf-blue.png)
