Design and implementation of embedded formal verification assistants in the .NET framework
Last modifed: Friday, April 01, 2005
The proposed project focuses on development of a .NET library that will enable to utilize structures and algorithms appearing in the tools supporting formal specification and verification. It aims at both, model checking and theorem proving to enable their combination in specialized tools based on the designed library. This approach supports the idea for considering .NET infrastructure as a common application framework equipped with a rich collection of wide spectrum classes. The conception of involving imperative languages, such as C#, VB, or C++, together with their functional relatives, such as SML, Mondrian, in the common framework opens interesting possibilities for mixing different style of programming at the granularity of class level which can make the task easier to complete, better manageable and the library wider usable. The primary goal is to provide a uniform library for development of specialized verification tools or their embedding into the tools for specification and design of computer systems.
Many formal methods for specification, verification, or development of computer-based systems have been proposed in the recent several decades. Happier ones were accepted by practitioners and are used in the industry for assisting with development mostly of critical systems , while others can be found only in academic area demonstrating their capability on synthetic examples. The crucial aspect adjudicating whether a method becomes popular, even only for academics, is accessibility of appropriate computer powered tools aiding with checking specifications, maintenance of development process or carrying out verification procedures. Unfortunately, development of such tools can consume a lot of time when it is done from scratch and, although some existing components are reused, it requires significant amount of effort exerted on their adaptation. Moreover development techniques are still changing, thus methods today available may become outdated quite soon.
Other point of view considers a broader utilizing of formal methods in the development. The idea of complete formal development of software seems to be utopia from several practical reasons, but broad accepted conviction considering selective embedding of formal methods in a development process represents a feasible way [3, 7]. It calls for an implementation of specialized tools or utilities that can translate or generate appropriate information for the current tools. The former, to be meaningful, requires existence of a suitable software infrastructure boosting implementation of the tools.
The proposed project considers to design and to implement a prototype of a class library containing structures and algorithms of selected specification and verification methods and theories packed into the .NET classes. Members of the project team have adequate knowledge of formal verification to consider both the model checking and the theorem proving approaches, which will divide the library onto two sub packages. The model checking package will include algorithms for state exploring possible extended with optimization techniques, abstract representations for state machines, state-transition graphs, binary decision diagrams and other relevant formal representations. The field of theorem proving will support language definitions, such as induction principle, general and dependent data type declarations, function definitions, and basic proof procedures including, for instance, decision algorithms, simplification methods, and lambda computation.
The purpose of the project is not to create a new verification tool but rather to extract fundamental concepts from either existing tools or theoretical results in order to design a general purpose library. The list of most significant algorithm and structure representations will be derived in a systematic way from the survey of currently available tools and research papers on formal methods, e.g. [1,2,5,6]. The architecture of library will be designed with respect to providing general, extensible and compact class hierarchy, using modern techniques for development of object-oriented software. An implementation realized exclusively in the .NET programming languages considers maximal utilization of standard framework classes. In the particular cases of model-checking algorithms, an open source code of third-party authors could be adapted if available.
The planned concrete output of the project consists of
· the library of structures and algorithms in the form of class hierarchy implemented in the .NET framework,
· full programmer and user documentation of the library, possibly extended with a bug list, prepared for further development and maintaining, and
· collection of technical reports and research papers delivering mainly surveys, comparative studies, and invented approaches.
Moreover to declared outputs of the project, all PhD. students involved in the project are encouraged to support ideas of their dissertations by designing appropriate tools utilizing the developed library.
March 2004 Start of the project
May 2004 Preliminary survey on specification structures and algorithms
June 2004 Done selection of formalisms and final version of the survey
September 2004 Library architecture proposal - first version
November 2004 Library architecture specification - final version
April 2005 Beta version of the library implementation
August 2005 Library documentation and bug-fixing
September 2005 Final workshop, Redmond, Seattle.
We will primarily use web pages of our project to share source codes, and technical reports. Research papers written during the project will be published in the usual way either at conference proceedings or in journals. The software produced in the frame of this project will be available under the MIT License (http://opensource.org/licenses/mit-license.php).
 Y.Bertot and L.Thery. A Generic Approach to Building User Interface for Theorem Provers. Journal of Symbolic Computation (1998) 25, pp 161-194.
 K. Fisler, S. Krishnamurthi and K. E. Gray. Implementing Extensible Theorem Provers. In proceedings of the 12th International Conference on Theorem Proving in Higher Order Logics, 1999.
 R. A. Kemmer. Integrating Formal Methods into Development Process. IEEE Computer, September 1990, pp 37–51.
 P. G. Larsen, J. Fitzerald and T. Brookes. Applying Formal Specification in Industry.
 F.Pfenning. The Practice of Logical Frameworks. In proceedings of the 21st International Colloquium, Linköping, Sweden, April 22-24, 1996.
 M. Stehr, J. Meseguer. Pure Type Systems in Rewriting Logic. In proceedings of LFM'99: Workshop on Logical Frameworks and Meta-languages, Paris, France, September 28, 1999
 J.M.Wing. A Specifier’s Introduction to Formal Methods. IEEE Computer, September 1990, pp 8–24.