Tools for Formal Software Engineering
Zhiming Liu, R. Venkatesh · 2005
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. Transformations include those for model construction and those that invoke verification tools. 1 Formal Software Engineering and the Grand Challenge The goal of the Verifying Compiler Grand Challenge [14] 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