Last modifed: Friday, April 01, 2005

Overview

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.

Description

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 [4], 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.

Details

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.

Time plan

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.

Intellectual Property

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).

References

[1] Y.Bertot and L.Thery. A Generic Approach to Building User Interface for Theorem Provers. Journal of Symbolic Computation (1998) 25, pp 161-194.

[2] 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.

[3] R. A. Kemmer. Integrating Formal Methods into Development Process. IEEE Computer, September 1990, pp 37–51.

[4] P. G. Larsen, J. Fitzerald and T. Brookes. Applying Formal Specification in Industry.
IEEE Software, May 1996, pp. 48 – 56.

[5] F.Pfenning. The Practice of Logical Frameworks. In proceedings of the 21st International Colloquium, Linköping, Sweden, April 22-24, 1996.

[6] 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

[7] J.M.Wing. A Specifier’s Introduction to Formal Methods. IEEE Computer, September 1990, pp 8–24.