Services that operate normally, independently, will behave differently when simultaneously initiated with another service. This behavior is called a feature interaction. A feature interaction, where the next state can not be determined uniquely for one event, is called a non-determinacy feature interaction. To detect the interaction, judgment has to be made as to whether the state, where the non-determinacy occurs, is reachable from the initial state or not. For the judgment, many methods have been proposed. But, still now, it is required huge computation time to judge the reachability. This paper proposes a new method to test the reachability using a little knowledge elicited beforehand. By using the proposed method computation time was reduced drastically. Besides, by applying the proposed method to a benchmark, the proposed method was confirmed to be effective and reasonable.

A protocol completion method is proposed to transform protocols synthesized from service specifications into error-free protocols. Communication service specifications described by message sequence charts can be synthesized into protocols. The synthesized protocols may include latent exceptional behaviors that are beyond the given service specifications. Therefore, even if the service specifications themselves are verified, these exceptional behaviors may produce protocol errors such as deadlock states or unspecified reception. Error-free protocols can be obtained from error-free service specifications by synthesizing and then completing the synthesized protocols. By taking account of each service specification through protocol completion, every exceptional behavior can be detected in the protocol entities including erroneous exceptional behaviors. This function can also be applied to resolution of feature interactions. The proposed method is applied to the synthesis of the X.227 protocol from its partial service specifications.

A stepwise refinement method of communications service specifications is proposed to generate communications software that can conform to any network architecture. This method uses a two-layered language; one layer is a service specification description language (STR), and the other layer is a supplementary specification description language for implementing STR description on a communications system (STR/D). STR specifies terminal behaviors that can be recognized from a perspective outside of the communications systems. With STR, a communications service is defined by a set of rules that can be described without detailed knowledge of communications systems or communications network architectures. Each STR rule describes a global state transition of terminals. Supplementary specifications, such as terminal control and network control, are needed to implement communications services specified by STR rules. These supplementary specifications are described by STR/D rules. Communications services, such as UPT (Universal Personal Telecommunication), are standardized so that they can be provided on a given functional model consisting of functional entities. Specifications for each functional entity in a network are obtained from the two kinds of initially described specifications mentioned above. The obtained specifications are described by STR(L) and STR/D(L) rules, which specify local specifications of a functional entity. These specifications for functional entities are then transformed into software specifications, and finally communications software is generated from these software specifications. This stepwise refinement method makes it possible to generate communications software that can conform to any functional model from service specifications.