Managing Complexity in Software Development with Formally Based Tools

Autor: Constance L. Heitmeyer
Rok vydání: 2004
Předmět:
Model checking
formal methods
Correctness
General Computer Science
Computer science
media_common.quotation_subject
Software requirements specification
Software walkthrough
computer.software_genre
Theoretical Computer Science
theorem proving
Software
Formal specification
Software quality analyst
Software verification and validation
Software requirements
Software system
formal verification
Computer-aided software engineering
Formal verification
Software design description
media_common
software tools
formal specification
Social software engineering
business.industry
Programming language
Software development
Formal methods
model checking
Software metric
Software framework
Test case
Debugging
Software security assurance
Software deployment
Software construction
Goal-Driven Software Development Process
Package development process
Software design
business
Software engineering
SCR
computer
Software verification
Computer Science(all)
Zdroj: Electronic Notes in Theoretical Computer Science. 108:11-19
ISSN: 1571-0661
DOI: 10.1016/j.entcs.2004.11.004
Popis: Over the past two decades, formal methods researchers have produced a number of powerful software tools designed to detect errors in, and to verify properties of, hardware designs, software systems, and software system artifacts. Mostly used in the past to debug hardware designs, in future years, these tools should help developers improve the quality of software systems. They should be especially useful in developing high assurance software systems, where compelling evidence is required that the system satisfies critical properties, such as safety and security. This paper describes the different roles that formally based software tools can play in improving the correctness of software and software artifacts. Such tools can help developers manage complexity by automatically exposing certain classes of software errors and by producing evidence (e.g., mechanically checked proofs, results of executing automatically generated test cases, etc.) that a software system satisfies its requirements. In addition, the tools allow practitioners to focus on development tasks best performed by people—e.g., obtaining and validating requirements and constructing a high-quality requirements specification.
Databáze: OpenAIRE
Externí odkaz: