Loading...
Please wait, while we are loading the content...
Similar Documents
Methods and tools for formal software engineering.
| Content Provider | CiteSeerX |
|---|---|
| Author | Venkatesh, R. Liu, Zhiming |
| Abstract | Abstract. 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. 1 Formal Software Engineering and the Grand Challenge The goal of the Verifying Compiler Grand Challenge [7, 6] is to build a verifying compiler that “uses mathematical and logical reasoning to check the programs that it compiles.” This implies that “a program should be allowed to run only if it is both syntactically and semantically correct ” [20]. To achieve this goal, the whole computing community have to deal with a wide range of issues, among which are [2] 1. arriving at automated procedures of abstraction that enables a compiler to work in combination with different program verification tools including testing tools, 2. studying what, where, when and how the correctness properties, i.e. assertions and annotations, are identified and specified, 3. identifying properties that can be verified compositionally, and designing specification notations and models to support more compositional specification, analysis and verification. 4. making tools that are scalable even with specified correctness criteria, In our view, theories and techniques are a long way from being able to solve the first three problems, and solutions to these problems is obviously vital for dealing with the fourth problem. |
| File Format | |
| Access Restriction | Open |
| Subject Keyword | Making Tool Correctness Property Transformation Tool Formal Technique Research Effort Component-based Design Verification Tool Transformed Model Specification Notation Correct Program Object System Testing Tool Long Way Verification Technique Logical Reasoning Main Theme Formal Software Engineering Automated Procedure Collaboration Project Fourth Problem Grand Challenge Compositional Specification Correctness Criterion Wide Range Engineering Method Verifying Compiler Whole Computing Community Different Program Verification Tool Verifying Compiler Grand Challenge |
| Content Type | Text |
