| dbpprop:abstract
|
- In computer science and software engineering, formal methods are particular kind of mathematically-based techniques for the specification, development and verification of software and hardware systems. The use of formal methods for software and hardware design is motivated by the expectation that, as in other engineering disciplines, performing appropriate mathematical analyses can contribute to the reliability and robustness of a design. However, the high cost of using formal methods means that they are usually only used in the development of high-integrity systems, where safety or security is important. Formal methods are best described as the application of a fairly broad variety of theoretical computer science fundamentals, in particular logic calculi, formal languages, automata theory, and program semantics, but also type systems and algebraic data types to problems in software and hardware specification and verification.
- In der Informatik bezeichnet der Begriff der Formalen Methoden eine Vielzahl von natur- und ingenieurswissenschaftlichen Techniken zum Modellieren und zur rigorosen Überprüfung von Computersystemen. Formale Methoden basieren in der Regel auf der Verwendung von mathematischer Logik. Die Rolle von Formalen Methoden in der Softwaretechnik und in der industriellen Praxis ist zur Zeit umstritten.
- En informatique, les méthodes formelles sont des techniques permettant de raisonner rigoureusement, à l'aide de logique mathématique, sur des programmes informatiques ou des matériels électroniques, afin de démontrer leur validité par rapport à une certaine spécification. Ces méthodes permettent d'obtenir une très forte assurance de l'absence de bogue dans les logiciels, c'est-à-dire d'acquérir des niveaux d'évaluation d'assurance élevés, elles sont basées sur les sémantiques des programmes, c'est-à-dire sur des descriptions mathématiques formelles du sens d'un programme donné par son code source (ou parfois, son code objet). Cependant, elles sont généralement coûteuses en ressources (humaines et matérielles) et actuellement réservées aux logiciels les plus critiques. Leur amélioration et l'élargissement de leurs champs d'application pratique sont la motivation de nombreuses recherches scientifiques en informatique.
- 形式手法（けいしきしゅほう、英: formal methods）は、計算機科学における数学を基盤としたソフトウェアおよびハードウェアシステムの仕様記述、開発、検証の技術である。そのアプローチは高度な信頼性（安全性やセキュリティなど）を求められるシステムでは特に重要であり、開発工程でエラーが入り込まないことを保証する。形式手法は要求仕様レベルや機能仕様レベルでは特に効果的であるが、実装レベル（例えばプログラム作成）でも完全な形式主義的開発は可能である。
- Metody formalne - w informatyce tym terminem określa się oparte na matematyce podejścia do specyfikacji, projektowania i weryfikacji oprogramowania lub systemów informatycznych. Użycie notacji i języków ze zdefiniowanym matematycznym znaczeniem pozwala precyzyjnie określić, co system informatyczny powinien robić, jakie mają być jego właściwości oraz zweryfikować poprawność działania systemu.
- Métodos formais, na ciência da computação e engenharia de software, são técnicas matemáticas para o desenvolvimento e especificação dos sistemas de software e hardware. Para realizar tal tarefa no desenvolvimento, deve-se primeiro construir um modelo de solução especificada formalmente, utilizando uma linguagem formal. Tendo este modelo formal como base, pode-se ter os seguintes benefícios: Permitir que dúvidas sobre o projeto possam ser respondidas por avaliações matemáticas. Estas avaliações puramente simbólicas e precisas podem ser usadas para “debugging” e inspeção do projeto, bem como para verificação do software; Uso de linguagens técnicas e ferramentas baseadas na lógica e matemática discreta, para especificação de software e verificação de sistemas, criando um sistema compreensivel, robusto e de desempenho aceitável; A redução da dependência da intuição e julgamento humanos; Grande poder de abstração; Provar que o código está correto ao se realizar a implementação do software, Validar o modelo através de simulações e assim detectar inconsistências e ambiguidades na especificação decorrentes da "linguagem informal". Encontramos as seguintes desvantagens nos métodos formais: Esse objetivo torna-se ainda mais imperativo quando software é empregado em sistemas cuja falha operacional pode ocasionar perdas humanas, econômicas ou causar degradação na prestação de serviços. Em ambientes críticos envolvendo sistemas de controle de tráfego aéreo ou de comando e controle de aeronaves, há uma necessidade preeminente de que os requisitos do sistema sejam precisamente especificados, objetivando implementar corretamente o projeto. Situação similar ocorre em sistemas sujeitos a sofrer degradação no nível de prestação de serviços quando operando em situação de falha. Exemplos de tais sistemas compreendem os sistemas de telecomunicações e sistemas de bancos com caixa de auto-atendimento. Em geral, o alto custo do uso de métodos formais, durante o desenvolvimento, levam-os a serem aplicados apenas em sistemas de alta-integridade, nos quais há alta probabilidade de falhas conduzirem a prejuízo e/ou morte.
- Формальні методи — в комп'ютерних науках, основані на математиці методи написання специфікацій, розробки та перевірки програмного забезпечення та комп'ютерного обладнання. Цей підхід особливо важливий для вбудованих систем, для яких важливими є надійність або безпека, для захисту від появи помилок в процесі розробки. Застосування формальних методів особливо ефективно на ранніх етапах написання вимог та специфікацій, але, також, можуть використовуватись для повністю формальної розробки реалізації (наприклад, програми).
- 在计算机科学和软件工程领域，形式化方法是基于数学的特种技术，适合于软件和硬件系统的描述、开发和验证。将形式化方法用于软件和硬件设计，是期望能够像其它工程学科一样，使用适当的数学分析以提高设计的可靠性和鲁棒性。但是，由于采用形式化方法的成本高意味着它们通常只用于开发注重安全性的高度整合的系统。
|
| rdfs:comment
|
- In computer science and software engineering, formal methods are particular kind of mathematically-based techniques for the specification, development and verification of software and hardware systems. The use of formal methods for software and hardware design is motivated by the expectation that, as in other engineering disciplines, performing appropriate mathematical analyses can contribute to the reliability and robustness of a design.
- In der Informatik bezeichnet der Begriff der Formalen Methoden eine Vielzahl von natur- und ingenieurswissenschaftlichen Techniken zum Modellieren und zur rigorosen Überprüfung von Computersystemen. Formale Methoden basieren in der Regel auf der Verwendung von mathematischer Logik. Die Rolle von Formalen Methoden in der Softwaretechnik und in der industriellen Praxis ist zur Zeit umstritten.
- En informatique, les méthodes formelles sont des techniques permettant de raisonner rigoureusement, à l'aide de logique mathématique, sur des programmes informatiques ou des matériels électroniques, afin de démontrer leur validité par rapport à une certaine spécification.
- Metody formalne - w informatyce tym terminem określa się oparte na matematyce podejścia do specyfikacji, projektowania i weryfikacji oprogramowania lub systemów informatycznych. Użycie notacji i języków ze zdefiniowanym matematycznym znaczeniem pozwala precyzyjnie określić, co system informatyczny powinien robić, jakie mają być jego właściwości oraz zweryfikować poprawność działania systemu.
- Métodos formais, na ciência da computação e engenharia de software, são técnicas matemáticas para o desenvolvimento e especificação dos sistemas de software e hardware. Para realizar tal tarefa no desenvolvimento, deve-se primeiro construir um modelo de solução especificada formalmente, utilizando uma linguagem formal. Tendo este modelo formal como base, pode-se ter os seguintes benefícios: Permitir que dúvidas sobre o projeto possam ser respondidas por avaliações matemáticas.
- Формальні методи — в комп'ютерних науках, основані на математиці методи написання специфікацій, розробки та перевірки програмного забезпечення та комп'ютерного обладнання.
- 在计算机科学和软件工程领域，形式化方法是基于数学的特种技术，适合于软件和硬件系统的描述、开发和验证。将形式化方法用于软件和硬件设计，是期望能够像其它工程学科一样，使用适当的数学分析以提高设计的可靠性和鲁棒性。但是，由于采用形式化方法的成本高意味着它们通常只用于开发注重安全性的高度整合的系统。
|
![[RDF Data]](/statics/sw-cube.png)
