This paper presents an analytical model that yields the unavailability of a network function when each backup server can protect two functions and can recover one of them. Previous work describes a model to deal with the case that each function can be protected only by one server. In our model, we allow each function to be protected by multiple servers to ensure function availability. This requires us to know the feasible states of a connected component and its state transitions. By adopting the divide-and-conquer method, we enumerate the feasible states of a connected component. We then classify its state transitions. Based on the obtained feasible states and the classification of the state transitions, we enumerate the feasible states incoming to and outgoing from a general state, the transfer rates, and the conditions. With those informations, we generate multiple equations about the state transitions. Finally, by solving them, we obtain the probabilities that a connected component is in each state and calculate the unavailability of a function. Numerical results show that the average unavailability of a function is reduced by 18% and 5.7% in our two examined cases by allowing each function to be protected by multiple servers.

Software engineering education at universities plays an increasingly important role as software quality is becoming essential in realizing a safe and dependable society. This paper proposes a practical state transition model (Practical-STM) based on the Organizational Expectancy Model for the improvement of software process education based on the Personal Software Process (PSP) from a motivation point of view. The Practical-STM treats an individual trainee of the PSP course as a state machine, and formalizes a motivation process of a trainee using a set of states represented by factors regarding motivation and a set of operations carried out by course instructors. The state transition function of this model represents the features or characteristics of a trainee in terms of motivation. The model allows a formal description of the states of a trainee in terms of motivation and the educational actions of the instructors in the PSP course. The instructors are able to decide effective and efficient actions to take toward the trainees objectively by presuming a state and a state transition function of the trainees formally. Typical patterns of state transitions from an initial state to a final state, which is called a scenario, are useful for inferring possible transitions of a trainee and taking proactive operations from a motivation point of view. Therefore, the model is useful not only for improving the educational effect of the PSP course, but also for the standardization of the course management and the quality management of the instructors.

We proposes a method for determining the frequency for monitoring the activities of a malware download site used for malware attacks on websites. In recent years, there has been an increase in attacks exploiting vulnerabilities in web applications for infecting websites with malware and maliciously using those websites as attack platforms. One scheme for countering such attacks is to blacklist malware download sites and filter out access to them from user websites. However, a malware download site is often constructed through the use of an ordinary website that has been maliciously manipulated by an attacker. Once the malware has been deleted from the malware download site, this scheme must be able to unblacklist that site to prevent normal user websites from being falsely detected as malware download sites. However, if a malware download site is frequently monitored for the presence of malware, the attacker may sense this monitoring and relocate that malware on a different site. This means that an attack will not be detected until the newly generated malware download site is discovered. In response to these problems, we clarify the change in attack-detection accuracy caused by attacker behavior. This is done by modeling attacker behavior, specifying a state-transition model with respect to the blacklisting of a malware download site, and analyzing these models with synthetically generated attack patterns and measured attack patterns in an operation network. From this analysis, we derive the optimal monitoring frequency that maximizes the true detection rate while minimizing the false detection rate.

Nonvolatile flip-flop enables leakage power reduction in logic circuits and quick return from standby mode. However, it has limited write endurance, and its power consumption for writing is larger than that of conventional D flip-flop (DFF). For this reason, it is important to reduce the number of write operations. The write operations can be reduced by stopping the clock signal to synchronous flip-flops because write operations are executed only when the clock is applied to the flip-flops. In such clock gating, a method using Exclusive OR (XOR) of the current value and the new value as the control signal is well known. The XOR based method is effective, but there are several cases where the write operations can be reduced even if the current value and the new value are different. The paper proposes a method to detect such unnecessary write operations based on state transition analysis, and proposes a write control method to save power consumption of nonvolatile flip-flops. In the method, redundant bits are detected to reduce the number of write operations. If the next state and the outputs do not depend on some current bit, the bit is redundant and not necessary to write. The method is based on Binary Decision Diagram (BDD) calculation. We construct write control circuits to stop the clock signal by converting BDDs representing a set of states where write operations are unnecessary. Proposed method can be combined with the XOR based method and reduce the total write operations. We apply combined method to some benchmark circuits and estimate the power consumption with Synopsys NanoSim. On average, 15.0% power consumption can be reduced compared with only the XOR based method.

State Transition Matrix (STM) is a table-based modeling language that has been frequently used in industry for specifying behaviors of systems. Functional correctness of a STM design (i.e., a design developed with STM) could often be expressed as invariant properties. In this paper, we first present a formalization of the static and dynamic aspects of STM designs. Consequentially, based on this formalization, we investigate a symbolic encoding approach, through which a STM design could be bounded model checked w.r.t. invariant properties by using Satisfiability Modulo Theories (SMT) solving technique. We have built a prototype implementation of the proposed encoding and the state-of-the-art SMT solver - Yices, is used in our experiments to evaluate the effectiveness of our approach. Two attempts for accelerating SMT solving are also reported.

Those host-based intrusion detection models like VPStatic first construct a model of acceptable behaviors for each monitored program via static analysis, and then perform intrusion detection by comparing them with programs' runtime behaviors. These models usually share the highly desirable feature that they do not produce false alarms but face the conflicts between accuracy and efficiency. For instance, the high accuracy of the VPStatic model is at the cost of high space complexity. In this paper, we use a statically-constructed state transition table (STT), which records expected transitions among system calls as well as their stack states (return address lists), as a behavior model to perform context-sensitive intrusion detection. According to our analysis, our STT model improves the space efficiency of the VPStatic model without decreasing its high precision and time efficiency. Experiments show that for three test programs, memory uses of our STT models are all much less than half of the VPStatic models'. Thereby, we alleviate the conflicts between the accuracy and the efficiency.

In a periodic spectrum sensing framework where each frame consists of a sensing block and a data transmitting block, increasing sensing duration decreases the probabilities of both missed opportunity and interference with primary users, but increasing sensing duration also decreases the energy efficiency and the transmitting efficiency of the cognitive network. Therefore, the sensing duration to use is a trade-off between sensing performance and system efficiencies. The relationships between sensing duration and state transition probability are analyzed firstly, when the licensed channel stays in the idle and busy states respectively. Then a state transition probability based sensing duration optimization algorithm is proposed, which can dynamically optimize the sensing duration of each frame in the current idle/busy state by predicting each frame's state transition probability at the beginning of the current state. Analysis and simulation results reveal that the time-varying optimal sensing duration increases as the state transition probability increases and compared to the existing method, the proposed algorithm can use as little sensing duration in each frame as possible to satisfy the sensing performance constraints so as to maximize the energy and transmitting efficiencies of the cognitive networks.

In this letter, we propose a novel approach to human activity recognition. We present a class of features that are robust to the tilt of the attached sensor module and a state transition model suitable for HMM-based activity recognition. In addition, postprocessing techniques are applied to stabilize the recognition results. The proposed approach shows significant improvements in recognition experiments over a variety of human activity DB.

Particle filter has attracted increasing attention from researchers of object tracking due to its promising property of handling nonlinear and non-Gaussian systems. In this paper, we mainly explore the problem of precisely estimating observation likelihoods of particles in the joint feature-spatial space. For this purpose, a mixture Gaussian kernel function based similarity is presented to evaluate the discrepancy between the target region and the particle region. Such a similarity can be interpreted as the expectation of the spatial weighted feature distribution over the target region. To adapt outburst of object motion, we also present a method to appropriately adjust state transition model by utilizing the priors of motion speed and object size. In comparison with the standard particle filter tracker, our tracking algorithm shows the better performance on challenging video sequences.

A typical feature of MANETs is that network topology is dynamically changed by node movement. When we execute state transition testing for such protocols, first we draw the Finite State Machine (FSM) with respect to each number of neighbor nodes. Next, we create the state transition matrix from the FSMs. Then, we generate test cases from the state transition matrix. However, the state transition matrix is getting much large because the number of states and the number of transitions increase explosively with increase of the number of neighbor nodes. As a result, the number of test cases increases, too. In this paper, we propose a new method to reduce the number of test cases by using equivalent division method. In this method, we decide a representative input to each state, which is selected from equivalent inputs to the states. By using our proposed method, we can generate state transition matrix which is hard to affect increasing the number of neighbor nodes. As a consequence, the number of test cases can be reduced.

In digital transmission and storage systems, sequences must have attributes that comply with the physical characteristics of the channel. These channel constraints can often be satisfied through constrained sequence coding techniques which avoid use of sequences that violate the given channel constraints. In the design of a constrained code, it is usually helpful to consider the PSD of the encoded sequence in order to ensure that PSD requirements are met, and to obtain an indication of bandwidth, response at dc, average power peaks, and other spectral characteristics of interest. In this paper, we introduce an approach for the construction of finite-state sequential machine (FSSM) modeled encoders to satisfy spectral requirements. This approach involves construction of either a Mealy or a Moore FSSM to represent the encoder, and evaluation of the state transition probabilities and codeword values such that the PSD of the designed code meets a predefined spectral shape. Examples in this paper demonstrate the usefulness of this approach.

This paper presents a formal verification method based on logic simulation. In our method, some restricted class of circuits which include data paths can be verified without abstraction of data paths by using symbolic values. Our verifier extracts a transition relation from the state graph (given as a specification) which is expressed using symbolic values, and verifies based on simulation using those symbolic values if the circuit behaves correctly with respect to each transition of the specification. If the verifier terminates with "correct," then it can be guaranteed that for any applicable input vector sequence, the circuit and the specification behaves identically. We have implemented the proposed method on a Unix workstation and verified some FIFO and LIFO circuits by using it.

Message Sequence Chart (MSC) standardized by International Telecommunication Union is a graphical and textual language for specification of concurrent systems. It has been used formally as well as informally to specify behavior of real-time systems, in particular telecommunication switching systems. Formal verification of a system specification is crucial to ensure that implementation of the system works correctly. In particular, verification methods based on finite states have been widely used in telecommunication systems design. The methods determine global system states and transitions between them (i. e. , build a global state transition graph (GSTG)), and verify the system's desired properties, such as safety and liveness, on the GSTG. In this paper, we focus on construction of GSTGs from MSC specifications. We propose action dependency graph as an intuitive description of semantics of MSC specifications and present an algorithm to translate MSC specifications to action dependency graphs as well as an algorithm to construct a global state transition graph from an action dependency graph.

This paper proposes a method of automatically eliciting knowledge which is used to detect feature interactions in telecommunication services. With conventional methods, the knowledge is provided manually. With the proposed method, the knowledge is automatically elicited as service constraints. In telecommunication systems, when a new service is added, new state transitions are created. In case of new service, the new state should be reached in the state transitions. On the other hand, some states of existing services should not be reached. These constraints can be considered as knowledge for detecting feature interactions. This paper also proposes a scenario for detecting feature interactions using elicited knowledge. This scenario was confirmed as effective.

This paper describes an efficient simulator for state transition analysis of multivalued continuous-time neural networks, where the multivalued transfer function of neuron is regarded as a stepwise constant one. Use of stepwise constant method enables to analyse the state transition of the network without solving explicitly the differential equations. This method also enables to select the optimal timestep in numerical integration. The proposed method is implemented on the simulator and applied to the general neural network analysis. Furthermore, this is compared with the conventional simulators. Finally, it is shown that our simulator is drastically faster and more practical than the conventional simulators.

Due to the large and complex information processing systems, formal description methods are needed for specification of systems and their efficient and reliable designs. During the early stage of system design, it is often necessary to modify or change system requirements which may influence the whole system design. We have proposed a new flexible description methodology, which copes with the modifications or changes in the system requirements, in order to obtain the formal specification of the system. We have also shown that function requirements can be modeled by a Logical Petri Net (LPN), which is a kind of extended Petri Nets, in order to derive the formal specification. In this paper, we propose a verification method of system requirements that contain some kinds of logical errors. Further, we show a method to decompose and refine a requirement description hierarchically, and discuss how to derive a formal specification from a requirement description flexibly along our refinement method against the changes of the requirement description in the system.

This paper proposed a practical method of program validation for state-based reactive concurrent systems. The proposed method is of particular relevance to plant control systems. Plant control systems can be represented by extended state transition systems (e.g., communicating asynchronous transition systems). Our validation method is based on state space analysis. Since naive state space analysis causes the state explosion problem, techniques to ease state explosion are necessary. One of the most promising techniques is the partial order method. However, these techniques usually require some structural assumptions and they are not always effective for actual control systems. Therefore, we claim integration and harmonization of verification (i.e., state space analysis based on the partial order method) and simulation (i.e., conventional validation technique). In the proposed method, verification is modeled as exhaustive simulation over the state space, and two types of simulation management techniques are introduced. One is logical selection (pruning) based on the partial order method. The other is heuristic selection based on priority (a priori precedence) specified by the user. In order to harmonize verification (logical selection) and conventional simulation (heuristic selection), we propose a new logical selection mechanism (the default priority method). The default priority method which prunes redundant state generation based on default priority is in harmony with heuristic selection based on the user's priority. We have implemented a practical validation tool, Simulation And Verification Environment for Reactive Concurrent Systems (SAVE/RCS), and applied it to chemical plant control systems.

Until now, in a communication system which deals with multiple processes, system behavior has been described by a fixed number of processes. The state reachability problem for specified processes was generally deliberated within a pre-defined number of processes, and was analyzed by essentially searching for all possible behaviors. However, in a system whose number of processes is arbitrary, a given state which is not reachable in some situations which consists of a small number of processes might be reachable in another situation which consists of a larger number of processes. This article discusses the above problem, assuming that the behavior of a system is described by an arbitrary number of processes. After discussing the relationship between our model and the Petri net model, we clarify the properties between the set of reachable states and the number of processes involved in the system, and show an algorithm to obtain a sufficient number of processes for resolving the reachability problem.

Recently, a flexible image database retrieval system where image keywords can be captured automatically is strongly required, in order to manage a practical number of image data successfully. However, image recognition/understanding technology level is not generally sufficient enough to achieve this requirement. In order to overcome this problem, a new type of image database framework is proposed in this paper. In the proposed system, image keywords are extracted in fully-automated fashion by the flexible and generalized image recognition system. Image keywords employed in this system are a collection of recognized objects in the image, where achieved recognition levels are allowed to be intermediate or imperfect. The concept of recognition thesaurus" has been introduced to manage these various abstraction level of kerwords successfully. As an embodiment of this concept, an experimental image database with various types of sports scenes has been implemented and various retrieval evaluations have been performed. Experimental results reveal the effectiveness of the proposed method.

A conflict detection support method for combining additional telecommunication services with existing services is proposed. In this method, telecommunication services are described by the STR (State Transition Rule) method which specifies a set of state transition rules. Though conflict detection in the past depended on manual analysis by the designer, with this method, conflict candidates are mechanically narrowed down and indicated to the designer. All conflicts between five actual telecommunication service descriptions are detected in an experiment using a system developed in line with the proposed method.