The MAYA system is a development graph manager that provides tool support for various administrative and management aspects of evolutionary formal software development. It is based on a uniform representation of structured theories, the so-called development graph (see [2,3]), and rules to reason about the structure of the specification. Those rules have been implemented in MAYA [5], which hence provides tool support for the verification in-the-large of structured specifications. Originally developed as an add-on to the INKA 5.0 system, it has been outsourced and is now developed as a system on its own. The vision motivating its development is that it serves as a uniform mediator between parsers for specifications and theorem provers. The latter, usually, provide tool support for verification in-the-small of specifications, and thus complement the in-the-large verification capabilities of MAYA [5].
To fulfill its mediator role, MAYA [5] provides a uniform interface to the parsers, in order to represent structured theories. For a detailed description of the integration of the CASL parser CATS see [1].
For the integration of theorem provers, there are several possible schemes (more to come soon). We have integrated the HOLCASL system into MAYA [4], in order to obtain strong tool support for verification in-the-small of CASL specification. We defined a uniform format of methodcalls by refining the XML-RPC protocol to the specific need of connecting MAYA to some theorem prover. The DTD of the methodcalls and the exchange format for HOL signatures and formulas can be found here.
The core of MAYA is implemented in Allegro Common Lisp, its user interface in MOZART OZ. The sources of MAYA together with the integrated CASL parser CATS and the HOL-CASL theorem proving system (see [4]) can be found here.
[1] Serge Autexier, Dieter Hutter, Heiko Mantel, Axel Schairer. Towards an Evolutionary Formal Software-Development Using CASL, In WADT99 Selected Papers volume, Springer, LNCS 1827, 2000.
Abstract: In practice, the formal development of software is an evolutionary process. Failed proof attempts give rise to changes in the specification and such changes invalidate proofs which have been previously performed. Clearly, it is very desirable to preserve much of the proof effort after such changes. In this paper, we propose development graphs as a general framework for modular specifications and define a structure preserving translation of CASL specifications into these graphs. The feature of development graphs, which is most important for an evolutionary process, is that they simplify the analysis of changes to the specification such that their negative effects can be kept to a minimum.
[2] Dieter Hutter. Management of change in structured verification, In Proceedings Automated Software Engineering (ASE-2000), IEEE, 2000.
Abstract: The use of formal methods in large complex applications implies the need for an evolutionary formal program development in which specification and verification phases are interleaved. But any change of a specification either by adding new parts or by changing erroneous parts affects existing verification work in a subtle way. In this paper we present a truth maintenance system for structured specification and verification. It is based on the simple but powerful notion of a development graph as an underlying datastructure to represent an actual consistent state of a formal development. Based on this notion we try to minimize the consequences of changes of existing verification work.
[3] Till Mossakowski, Serge Autexier, Dieter Hutter. Extending Development Graphs With Hiding, In H. Hußmann (Ed.), Proceedings of Fundamental Approaches to Software Engineering (FASE 2001), April 2-6 , 2001, Genova, Italy, accepted, forthcoming.
Abstract: Development graphs are a tool for dealing with structured specifications in a way easing management of change and reusing proofs. In this work, we extend development graphs with hiding. Hiding is a particularly difficult to realize operation, s ince it does not admit such a good decomposition of the involved specifications as other structuring operations do. We develop both a semantics and proof rules for development graphs with hiding. The rules are proven to be sound, and also complete relative to an oracle for conservative extensions. We also show that an absolute complete set of rules cannot exist. The whole framework is developed in a way independent of the underlying logical system.
[4] Serge Autexier, Till Mossakowski: Integrating HOL-CASL into the Development Graph Manager MAYA, In. A. Armando (Ed.) Proceedings of FROCOS'02, Springer, LNAI 2309, Santa Margherita Ligure, April, 2002.
Abstract: For the recently developed specification language CASL, there exist two different kinds of proof support: While HOL-CASL has its strength in proofs about specifications in-the-small, MAYA has been designed for management of proofs in (CASL) specifications in-the-large, within an evolutionary formal software development process involving changes of specifications. In this work, we discuss our integration of HOL-CASL and MAYA into a powerful system providing tool support for CASL, which will also serve as a basis for the integration of further proof tools.
[5] Serge Autexier, Dieter Hutter, Till Mossakowski, Axel Schairer, The Development Graph Manager MAYA (system description), In H. Kirchner (editor) Proceedings of 9th International Conference on Algebraic Methodology And Software Technology (AMAST'02), Springer, September 2002, accepted, forthcoming.
[6] Serge Autexier, Dieter Hutter, Maintenance of Formal Software Development by Stratified Verification, In M. Baaz, A. Voronkov (Eds.) Proceedings of the 9th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2002, Springer LNCS 2514, Tbilisi, Georgia, October 14-18, 2002.
Abstract: The development of industrial-size software is an evolutionary process based on structured specifications. In a formal setting, specification and verification are intertwined. Specifications are amended either to add new functionality or to fix bugs detected during the verification process. In this paper we propose a system to maintain the verification of formal developments. It exploits the structure of the specification to reveal and eliminate redundant proof obligations and therefore constitutes itself a verification system in-the-large. Proofs in this system are represented as explicit proof objects allowing the system to adjust or reuse them in case the specification is changed.
[7] Till Mossakowski, Piotr Hoffman, Serge Autexier, Dieter Hutter CASL Logic , Part IV of the CASL Reference Manual, P.D. Mosses (editor), pp. 281--363, Springer LNCS 2960, 2004