MENDELS ZONE A Concurrent Program Development System ABSTRACT MENDELS ZONE is a software development system for concurrent pro- grams. The system takes as input several kinds of specifications for MENDEL objects, verifies their correctness using automated theorem proving techniques, and generates correct KL1 programs semi-automatically. KEY FEATURES (I%(B object generation: Specifications, based on equational logic, for MENDEL objects are verified in parallel using term rewriting techniques and trans- formed into MENDEL objects automatically. (I%(B object composition: MENDEL objects are represented by a high-level Petri net (MENDEL net). Users compose these objects with the aid of a graphical MENDEL net editor. (I%(B object adjustment: Composed objects are automatically adjusted to satisfy supplied temporal logic specifications, which specify only timing con- straints of composed objects. The object adjustment is carried out by parallel automated reasoning techniques with Petri nets and temporal logic. - 97 - ABSTRACT In the future, an increasing number of application programs will be dis- tributed systems or concurrent systems. Debugging and testing of concurrent systems are very difficult, hence it is necessary to establish a methodology for the development of reliable programs. MENDELS ZONE is a system whose aim is the realization of such a methodology, and supports the development of correct concurrent programs through the combined use of several formal methods. APPROACH MENDEL is a concurrent programming language based on Petri net seman- tics, which can be compiled into KL1 and executed. A MENDEL program is composed of several objects which behave concurrently. MENDELS ZONE is a concurrent program development system for MENDEL, that adopts formal methods based on mathematics. Formal methods are recognized as useful in developing reliable programs, but the following problems need to be solved before putting them into practical use: 1. It is difficult to describe a whole system with only one formal method. 2. Specifications become less comprehensible as their sizes grow larger. 3. Formal methods are not suitable for large scale systems. 4. The verification of specifications and the generation of programs are com- putationally costly. In MENDELS ZONE, the above problems are dealt with as follows. Objects behaviors are described by an algebraic specification based on equational logic, and timing constraints among objects are described using temporal logic. Vi- sual specifications such as Petri nets are used to make formal specifications more understandable and lessen the burden of describing the specifications. Objects can be regarded as reusable parts because of their increased com- prehensibility and modularity, which makes it possible to develop large scale systems. Theorem proving methods for both the equational logic and the tem- poral logic are used in order to verify specifications and transform them into programs. Parallel implementations of these methods contribute in shortening the time necessary for verification and transformation. - 98 - MENDELS ZONE has put formal methods into practical use as described above, and it becomes possible to verify the correctness of specifications and transform them into programs. As a result, reliable programs can be gener- ated. OUTLINE OF SYSTEM The development of programs using MENDELS ZONE has two phases, namely, the "Algebraic Specification Phase" in which objects are generated and the "Petri Net Phase" in which Objects are composed. Figure 1 is a snapshot taken during the "Algebraic Specification Phase". FIGURE 1 Users denote algebraic specifications for behavior Method of objects 1. In order to describe specifications correctly, MENDELS ZONE provides several support functions: syntactical check, direct execution as a term rewriting system and verification with inductionless induction. When equations that the specifications should satisfy are given in 2, the system verifies automatically whether they are true or not. Progress of the verification procedure can be observed in 3. After verification, the specifications are transformed into MENDEL objects automatically. Figure 2 is a snapshot taken during the "Petri Net Phase". Objects gener- ated by automated transformation are registered in a Parts-Library 4. Com- position of objects is represented in terms of a high-level Petri net (MENDEL net), and is created using only mouse operations in the graphical MENDEL net editor 5. In general, there are some timing constraints among methods in - 99 - a object or among objects. In such a case, users denote the timing constraints using temporal logic 6. MENDELS ZONE adjusts Petri nets automatically in order to satisfy the constraints. This program adjustment means synthesizing an arbiter that is attached to the original programs. A completed MENDEL program is compiled into a KL1 program, whose execution can be monitored within the environment provided by MENDELS ZONE. FIGURE 2 RESULT We have developed an control system of a power station in order to exam- ine the effectiveness of MENDELS ZONE for the development of a concurrent system. This control system was originally implemented directly in KL1, and we developed an almost identical system using MENDELS ZONE. Based on this experience, we feel confident in saying that a real system can be developed using MENDELS ZONE. A comparison between two development efforts re- veals that MENDELS ZONE reduces debugging time although more time is needed for specifying and coding. This fact is an indication of effectiveness of verification based on formal methods. OUTLINE OF DEMONSTRATION We demonstrate the capabilities of MENDELS ZONE using the develop- ment example of the control system, and show the result of this development. - 100 -