Name
Abstract | ||
|---|---|---|
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. |
Year | DOI | Venue |
|---|---|---|
2004 | 10.1016/j.entcs.2004.11.004 | Electr. Notes Theor. Comput. Sci. |
Keywords | Field | DocType |
compelling evidence,software tool,high-quality requirements specification,software error,high assurance software system,formal speciflcation,model checking,powerful software tool,software system artifact,scr.,software tools,software artifact,scr,software development,formal veriflcation,theorem proving,hardware design,formal methods,formal specification,formal verification,software system,formal method,software systems | Programming language,Software engineering,Computer science,Theoretical computer science,Software system,Computer-aided software engineering,Software construction,Software verification and validation,Software requirements specification,Software development,Software requirements,Software verification | Journal |
Volume | Issue | ISSN |
108 | C | 1571-0661 |
Citations | PageRank | References |
4 | 0.52 | 18 |
Authors | ||
1 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Constance Heitmeyer | 1 | 583 | 39.53 |