Tremendous progress has been made in automated and semi-automated verification since the seminal works on program verification. Automated deductive techniques like model checking have been highly successful for many v...
详细信息
ISBN:
(纸本)9783540691471
Tremendous progress has been made in automated and semi-automated verification since the seminal works on program verification. Automated deductive techniques like model checking have been highly successful for many verification tasks (e.g., [17, 18, 13]). Impressive advances continue to be made in static analysis, type systems, and static bug finding (e.g., [21, 12]). These approaches aim to verify code or find bugs in existing systems as automatically as possible, with as little developer help as possible. This has been the aim of the research community for many years, possibly due in part to the bad reputation that continues to plague full program verification. Theorem proving approaches to program verification have continued to make advances, but indeed, they still are generally applied only to the most critical applications (e.g., [7, 5, 16, 11]).
We propose a collaboration project to integrate the research effort and results obtained at UNU-IIST on formal techniques in component and object systems with research at TRDDC in modelling and development of tools th...
详细信息
ISBN:
(纸本)9783540691471
We propose a collaboration project to integrate the research effort and results obtained at UNU-IIST on formal techniques in component and object systems with research at TRDDC in modelling and development of tools that support object-oriented and component-based design. The main theme is an integration of verification techniques with engineering methods of modelling and design, and an integration of verification tools and transformation tools. This will result in a method in which a correct program can be developed through transformations that are either proven to be correct or by showing that the transformed model can be proven correct by a verification tool.
When considering the program verification challenge [8] one should not forget a lesson learned in the testing community: when it comes to industrial size programs, it is not realistic to expect programmers to formally...
详细信息
ISBN:
(纸本)9783540691471
When considering the program verification challenge [8] one should not forget a lesson learned in the testing community: when it comes to industrial size programs, it is not realistic to expect programmers to formally specify their program beyond simple assertions. It is well known that large parts of real code cannot be described naturally with high level invariants or temporal properties, and further that it is often the case that the process of describing what a code segment should do is as difficult and at least as complicated as the coding itself. Indeed, high-level temporal property-based testing, although by now supported by commercial tools such as Temporal-Rover[4], is in very limited use. The industry typically attempts to circumvent this problem with Regression Testing, which is probably the most popular testing method for general computer programs. It is based on the idea of reasoning by induction: check an initial version of the software when it is still very simple, and then check that a newer version of the software produces the same output as the earlier one, given the same inputs. If this process results with a counterexample, the user is asked to check whether it is an error or a legitimate change. In the latter case the testing database is updated with the new 217;correct217; output *** Testing does not require a formal specification of the investigated system nor a deep understanding of the code, which makes it highly suitable for accompanying the development process, especially if it involves more than one *** propose to learn from this experience and develop techniques for Regression Verification. The underlying proof engine is still a certifying compiler as envisioned by the grand challenge, so this proposal should be thought of as another application of this technology that makes the verification picture more complete.
暂无评论