We have already proposed a process algebra µLOTOS as a mathematical framework to synthesize a process from a number of (incomplete) specifications, in which requirements for the process do not have to be completely determined. It is guaranteed that the synthesized process satisfies all the given specifications, if they are consistent. For example, µLOTOS is useful for incremental design. The advantage of µLOTOS is that liveness properties can be expressed by least fixpoints and disjunctions . In this paper, we present µLOTOSR, which is a refined µLOTOS. The improvement is that µLOTOSR has a conjunction operator . Therefore, the consistency between a number of specifications S1,,S2 can be checked by the satisfiability of the conjunction specification S1 S2. µLOTOSR does not need the complex consistency check used in µLOTOS.

We have implemented a program editor for Modula-2 at ETH Zurich, named Macpeth. Macpeth is running on Lilith, Macintosh and other machines. We show the data structure for translation from the internal parse tree to the external textual representation. The data structure keeps the information for efficient scrolling and partial refreshing operations on the window.

We often use data flow diagrams or state transition diagrams to design software systems with concurrency. We call those diagrams as nets in this paper. Semantics of any methods to describe such software systems should be defined in some formal ways. There would be no doubts that any nets should be supported by appropriate theoretical frameworks. In this paper, we use CCS as a typical algebraic approach of using formulas to express concurrent behaviors and point out the different features of CCS from Petri nets. Any approaches should be not only theoretically beautiful but also practically useful. We use a specification language LOTOS as such example which has two features, CCS and ADT, and is designed to specify practical communication protocols. Algebraic approaches of using formulas, like LOTOS, can be considered as a compact way to express concurrent behaviors. We explore our discussions of net-oriented approaches into UIMS research fields. After mentioning state transition models of UIMS, we exemplify a practically used example, VIA-UIMS, which has been developed by one of authors. VIA-UIMS employs a net-oriented architecture. It has been designed to reconstuct tools which have already been widely used in many sites.

The purpose of this research is to analyze production rules with coupling modes in active databases and to exploit an assistant system for rule programming. Each production rule is a specification including an event, a condition, and an action. The action is automatically executed whenever the event occurs and the condition is satisfied. Coupling modes are useful to control execution order of transactions. For example, a transaction for consistency check should be executed after transactions for update. An active database, which is a database with production rules, can spontaneously update database states and check their consistency. Production rules provide a powerful mechanism for knowledge-bases. However it is very difficult in general to predict how a set of production rules will behave because of cascading rule triggers, concurrency, and so on. We are attempting to adopt a process algebra as a basic tool to analyze production rules. In order to describe and analyze concurrent and communicating systems, process algebras such as CCS, CSP, ACP, and π-calculus, are well known. However there are some difficulties to apply existing process algebras to analysis of production rules in growing process trees by process creation. In this paper we propose a process algebra named CCSPR (a Calculus of Communicating Systems with Production Rules), Which is an extension of CCS. An advantage of CCSPR is to syntactically describe growing process trees. Therefore, production rules can be appropriately analyzed in CCSPR. After giving definitions and properties of CCSPR, we show an example of analysis of production rules in CCSPR.