Natural language (NL) requirements are usually human-centric and therefore error-prone and inaccurate. In order to improve the 3Cs of natural language requirements, namely Consistency, Correctness and Completeness, in this paper we propose a systematic pattern matching approach supporting both NL requirements modeling and inconsistency, incorrectness and incompleteness analysis among requirements. We first use business process modeling language to model NL requirements and then develop a formal language — Workflow Patterns-based Process Language (WPPL) — to formalize NL requirements. We leverage workflow patterns to perform two-level 3Cs checking on the formal representation based on a coherent set of checking rules. Our approach is illustrated through a real world financial service example — Global Equity Trading System (GETS).

In this paper, we discuss a fundamental theory of incremental verification for workflows. Incremental verification is a method to help multiple designers share and collaborate on huge workflows while maintaining their consistency. To this end, we introduce passbacks in workflows and their consistency property in the control flow perspective. passbacks indicate redoing of works. Workflows with passbacks are useful to naturally represent human works. To define the consistency property above, we define normality of workflows with passbacks and total correctness of normal workflows based on transition system-based semantics of normal workflows. We further extend workflows to sorted workflows and define their vertical division and composition. We also extend total correctness to normal sorted workflows, for the sake of incremental verification of a large-scale workflow with passbacks via vertical division and composition.

Online and realtime traffic summarization is a challenge as, except for the routine cases, aggregation parameters or, the flows that need to be observed are not known a priori. Dynamic adaptive aggregation algorithms adapt to the network traffic to detect the important flows. But present day algorithms are inadequate as they often produce inaccurate or meaningless aggregates. In this work we propose a Dynamic Constrained Adaptive Aggregation algorithm that does not produce the meaningless aggregates by using information about the network's configuration. We compare the performance of this algorithm with the erstwhile Dynamic (Unconstrained) Adaptive Aggregation algorithm and show its efficacy. Further we use the network map context that shows the network flows in an intuitive manner. Several applications of the algorithm and network map based visualization are discussed.

In this paper, we present a first step for developing a method of verifying both safety and correctness of object-oriented design specification. At first, we analyze the discrepancies, which can occur between requirements specification and design specification, to make clear target faults. Then, we propose a new design review method which aims at detecting faults in the design specification by using three kinds of information tables. Here, we assume that component library, standards for safety and design specification obtained from the Booch's object-oriented design method are given. At the beginning, the designers construct a design table based on a design specification, and the verifiers construct a correctness table and a safety table from component library and standards for safety. Then, by comparing the items on three tables, the verifiers review a given design specification and detect faults in it. Finally, using a small example of object-oriented design specification, we show that faults concerning safety or correctness can be detected by the new design review method.

This paper describes the results obtained of a prototype system, VeriProc/1, based on an algorithm we first presented in [13] which can prove the correctness of pipelined processors automatically without pipeline invariant, human interaction, or additional information. No timing relations such as an abstract function or β-relation is required. The only information required is to specify the location of the selectors in the design. The performance is independent of not only data width but also memory size. Detailed analysis of CPU time is presented. Further, don't-care forcing using additional data easily prepared by the user can improve performance.

We describe a formal verification algorithm for pipelined processors. This algorithm proves the equivalence between a processor's design and its specifications by using rewriting of recursive functions and a new type of mathematical induction: extended recursive induction. After the user indicates only selectors in the design, this algorithm can automatically prove processors having more than 10(1010) states. The algorithm is manuary applied to benchmark processors with pipelined control, and we discuss how data width, memory size, and the numbers of pipeline stages and instructions influence the computation cost of proving the correctness of the processors. Further, this algorithm can be used to generate a pipeline invariant.

In LOTOS, requirements for a distributed system are described as a service definition. On the protocol level, each node (protocol entity) must exchange some data values and synchronization messages to provide a service described in a service definition. The tuple of the specifications of all nodes in the system which provide the service is called as a protocol specification. In order to develop the communication programs satisfying a given service definition, it is very important to develop the correct protocol specification. For this purpose, the simulation of protocol specifications is useful and it is desirable that the designer can observe how a protocol specification is executed in parallel and how synchronization messages are exchanged among the nodes. Therefore, we have developed a new tool named PROSPEX. For a given pair of a service definition and a protocol specification, it executes the protocol specification in parallel and shows its execution process graphically on X Window System. If the protocol specification executes an event sequence which does not satisfy the service definition, then PROSPEX informs it to the designer. In this paper, the design and usefulness of PROSPEX are described.

The semantics of a language for communicating processes is investigated, and three full abstractness results for are established. The language contains atomic actions, termination, inaction, sequential composition, alternative composition, parallel composition, action restriction, and a form of guarded recursion. (The guardedness restriction on recursion is needed to establish one of the full abstractness results.) Three Plotkin-style operational semantics WL, CWL, and IWL of the language are defined. These semantics are linear in that the meaning of each program in any of these semantics is a set of action sequences the program may perform, and are weak in that the action sequences are obtained by ignoring (finte sequences of) internal moves. All the three semantics distinguish divergence (an infinite sequence of internal moves) from deadlock. The semantics IWL differs from the other two in that IWL is a so-called interal action semantics taking into account only internal moves under the assumption that the environment allows no (external) communication actions, and hence, the only possible actions for processes are internal moves, whereas the other two semantics take into account communication actions in addition to internal moves. The two semantics WL and CWL differ each other in that CWL is a so- called completed trace semantics, whereas WL is not. Then, two compositional models RF and IRF for the language are proposed, and the full a bstractness of RF (resp. of IRF) w. r. t. WL and CWL (resp. w. r. t. IWL), as expressed in the following, is established:s1s2(*) S[][S[]is a context of ⇒S[s1]S[s2]],where ,RF,WL, RF,CWL, IRF,IWL. A similar full abstractness result has been established by Bergstra, Klop, and Olderog for a language without recursion or internal moves. Moreover, Rutten investigated the semantics of a language similar to , in the framework of complete metric spaces, and showed that the failures model is fully abstract w. r. t. a strong linear semantics L, where L is strong in that it does not abstract from internal moves. The full abstractness of RF w. r. t. CWL, expressed in (*) with ,RF,CWL, is an extension of the result of Bergstra et al. to a language with recursion and internal moves. Also, the full abstractness of IRF w. r. t. IWL, expressed in (*) with ,IRF,IWL, is an extension of the Rutten's result, to the case of weak linear semantics with divergence.