Net-Oriented Analysis and Design (NOAD) is defined as three items: (1) Various nets are utilized as an effective modeling method. (2) Inter-relationships among verious nets are determined. (3) Verification or analysis methods for nets are provided and they are implemented based on the mathematical theory, that is Net theory. Very few methods have been presented to satisfy these three items. For example, the Real-Time SA method covers item (1) only. The Object-Oriented Analysis and Design method (OOA/OOD) covers items (1) and (2). NOAD can be regarded as an extension to OOA/OOD. This paper discusses how effectively various nets have been used in actual software development support metnods and tools and evaluates such several methods and tools from the NOAD viewpoint.

This paper describes a modeling of the cryptography based on a concept of Petri nets. Movement of tokens in the net model shows a dynamic behavior of systems. On the other hand, the cryptography is considered as a bit operation, so that we can point out a common property between the net structure and the cryptography, which provides our idea that movement of tokens of the net model corresponds to a bitoperation of the cryptography. Some effective keys in the net model are considered by means of the net elements, which are based on T-invariant and net structures. It is shown that the keys of the net structured cryptography provide reasonable strength comparing with the data encryption standard (DES).

The subject of the paper is to propose two approximation algorithms FM_SPLA, FM_DPLA for priority-list scheduling in timed Petri nets. Their capability is compared with that of existing algorithms SPLA, DPLA through experimental results, where SPLA and DPLA have previously been proposed by the authors.

An integrated platform INTEGRAL has been developed for developing large complex communication software systems. At the heart of INTEGRAL, a pair of graphical and textual specification languages, DISCOL (DIStributed Communication-Oriented Language), has been developed based on Petri nets. Around DISCOL, a wide variety of design and analysis tools have been integrated in coherent manner so that a seamless support from design to verification and testing are made available along with software life-cycle. The platform has been applied to the development of a PBX simulator named UICPBX. In the development, some real communication services have been fully specified with DISCOL. Such experiences have revealed the effectiveness of the proposed techniques.

Stochastic Petri Nets and Generalized Stochastic Petri Nets as well as other extensions to Stochastic Petri Nets have been widely applied as a model of asynchronous concurrent process, or as an aid to analyze or design concurrent systems. This paper presents an Extended Stochastic Petri Net model for a shift processing system in which three kinds of sink may occur and an arbitrary time distribution is incorporated, provides an analytical method based on a Markov renewal process with some non-regeneration points to clarify the probabilistic behavior of the system, and finally evaluates the performance of the system with numerical values.

The subject of the paper is to analyze time complexity of the minimum modification problem in the Horn clause propositional logic. Given a set H of Horn clauses and a query Q in propositional logic, we say that Q is provable over H if and only if Q can be shown to be true by repeating Modus Ponens among clauses of H. Suppose that Q is not provable over H, and we are going to modify H and Q into H and Q , respectively, such that Q is provable over H . The problem of making such modification by minimum variable deletion (MVD), by minimum clause addition (MCA) or by their combination (MVDCA) is considered. Each problem is shown to be NP-complete, and some approximation algorithms with their experimental evaluation are given.

The subject of the paper is to analyze time complexity of the minimum axiom set problem (MASHC) in the Horn clause propositional logic. MASHC is defined by "Given a set H of Horn clauses and a query Q, all in propositional logic, such that Q is provable over H, find an axiom set of minimum cardinality, HH, with respect to Q, where Q is provable over H if and only if Q can be shown to be true by repeating Modus Ponens starting from clauses of H under the assumption that all of them are originally assumed to be true". If Q is provable over H then H is called an axiom set (with respect to Q). As stated in the definition of MASHC, detecting if Q is provable over H is required. This leads us to a problem, called the provability detecting problem (PDPHC), defined by "Given a set H of Horn clauses and a query Q in propositional logic, determine if Q is provable over H". First an O(σ) algorithm BFSHC for PDPHC is given based on the breadth-first search, where σ is the formula size of a given set of Horn clauses. For MASHC, it is shown that the problem is NP-complete, and an O(σ) approximation algorithm FMAS is given. Its experimental evaluation is also presented.