Automated verification of responsive protocols modeled by extended finite state machines

Along with advancement of communication systems, the demand for fault-tolerance and real-time performance for communication protocols continues to increase. Communication protocols which perform recovery from any abnormal state to a normal state are called self-stabilizing protocols. However, in these protocols, real-time recovery is not taken into consideration. This paper discusses verification of communication protocols which have self-stabilizing and timeliness properties, which are called responsive protocols.Gouda et al. proposed a mathematical method to prove whether a given protocol specification satisfies the self-stabilizing property. However, this method is not automated and does not verify the timeliness property. This paper thus proposes an automated method for verification of responsive protocols. In this method, communication protocols are modeled by extended finite state machines and their states are represented by predicates. The self-stabilizing property is proven by verifying that sequences of such states which start from an arbitrary abnormal state converge in a normal state. Also, the timeliness property is proven by verifying that the convergence is done within a priori given time.     

Analysis of a class of communicating finite state machines

Thereachability, deadlok detection andunboundedness detection problems are considered for the class ofcyclic one-type message networks of communicating finite state machines. We show that all the three problems are effectively solvable by (a) constructing canonical execution event sequences which belong to a context-free language, and (b) showing that the reachability sets are semilinear. Our algorithms have polynomial complexity in terms of size of a global structure of a network, called theshuffle-product. The relationships between general Petri nets and the class of communicating finite state machines considered here are also explored.Supported in part by NSF CCR-9004121     

Formalization of UML state machines using temporal logic

The main purpose of this paper is to approach the use of formal methods in computing. In more specific terms, we use a temporal logic to formalize the most fundamental aspects of the semantics of UML state machines. We pay special attention to the dynamic aspects of the different operations associated with states and transitions, as well as the behaviour of transitions related with composite states. This, to the best of our knowledge, has not been done heretofore using temporal logic.Our formalization is based on a temporal logic that combines points, intervals, and dates. Moreover this new temporal logic is built over an innovative and simple topological semantics, which simplifies the metatheory development.     

Minimization of mealy finite-state machines by using the values of the output variables for state assignment

Structural models of finite-state machines (FSMs) that make it possible to use the values of the output variables for encoding the internal states are studied. To minimize the area (the parameter area is used to denote cost in the context of this paper) of FSM implementation, it is proposed to use the structural model of the class D FSM. A method for the design of the class D FSM in FPGA is proposed. This method involves two phases—splitting the internal states of the FSM (to satisfy the necessary conditions for the construction of the class D FSM) and encoding the internal states (to ensure that the codes are mutually orthogonal). It is shown that the proposed method reduces the area of FSM implementation for all families of FPGAs of various manufacturers by a factor of 1.41–1.72 on average and by a factor of two for certain families. Practical issues concerning the method and the specific features of its use are discussed, and possible directions of the elaboration of this approach are proposed.     

On the structure of free finite state machines

The finite state machine U_{m, n}(M) freely generated by a set consisting of m states and n inputs subjects to the relations holding in the finite state machine M was considered by Birkhoff and Lipson in [1, 2]. In this paper, necessary and sufficient conditions for U_{m, n}(M) to consist of m disjoint copies of U_{1, n}(M) are established. The relationship between U_{1, n}(M) and the transition monoid of M, and a representation of U_{1, n}(M) as a transition monoid machine are described. The characterization of machines of type U_{1, n}(M) is in this way reduced to the characterization of finite monoids possessing a ‘universal presentation’. Some general results concerning finite semigroups and groups with a universal presentation, and precise characterizations of finite semilattices and Abelian groups admitting a universal presentation are described.     

Spiking neurons and the induction of finite state machines

We discuss in this short survey article some current mathematical models from neurophysiology for the computational units of biological neural systems: neurons and synapses. These models are contrasted with the computational units of common artificial neural network models, which reflect the state of knowledge in neurophysiology 50 years ago. We discuss the problem of carrying out computations in circuits consisting of biologically realistic computational units, focusing on the biologically particularly relevant case of computations on time series. Finite state machines are frequently used in computer science as models for computations on time series. One may argue that these models provide a reasonable common conceptual basis for analyzing computations in computers and biological neural systems, although the emphasis in biological neural systems is shifted more towards asynchronous computation on analog time series. In the second half of this article some new computer experiments and theoretical results are discussed, which address the question whether a biological neural system can, in principle, learn to behave like a given simple finite state machine.     

Automated metamorphic testing on the analyses of feature models

Context

A feature model (FM) represents the valid combinations of features in a domain. The automated extraction of information from FMs is a complex task that involves numerous analysis operations, techniques and tools. Current testing methods in this context are manual and rely on the ability of the tester to decide whether the output of an analysis is correct. However, this is acknowledged to be time-consuming, error-prone and in most cases infeasible due to the combinatorial complexity of the analyses, this is known as the oracle problem.

Objective

In this paper, we propose using metamorphic testing to automate the generation of test data for feature model analysis tools overcoming the oracle problem. An automated test data generator is presented and evaluated to show the feasibility of our approach.

Method

We present a set of relations (so-called metamorphic relations) between input FMs and the set of products they represent. Based on these relations and given a FM and its known set of products, a set of neighbouring FMs together with their corresponding set of products are automatically generated and used for testing multiple analyses. Complex FMs representing millions of products can be efficiently created by applying this process iteratively.

Results

Our evaluation results using mutation testing and real faults reveal that most faults can be automatically detected within a few seconds. Two defects were found in FaMa and another two in SPLOT, two real tools for the automated analysis of feature models. Also, we show how our generator outperforms a related manual suite for the automated analysis of feature models and how this suite can be used to guide the automated generation of test cases obtaining important gains in efficiency.

Conclusion

Our results show that the application of metamorphic testing in the domain of automated analysis of feature models is efficient and effective in detecting most faults in a few seconds without the need for a human oracle.     

Use of a lightweight formal method to model the static aspects of state machines

In this paper the author uses Alloy as a modeling language to model the elements that form a state machine and the rules that govern how they can be connected. In particular, the model proposed in this paper focuses in the static aspects of state machines. To analyze and detect design errors in the model, the Alloy analyzer was used. With the use of this tool, design errors can be detected very quickly. This tool can also generate instances of the model without making a line of code. The paper presents two models based on the formal approach: a graphical model and a textual model. The graphical model is used as an overview of the system while the textual model is used to establish further constraints on the graphical model.     

Post-evolution of variable-length class prototypes to unlock decision making within support vector machines

Although neural networks and support vector machines (SVMs) are the traditional predictors for the classification of complex problems, these opaque paradigms cannot explain the logic behind the discrimination process. Therefore, within the quite unexplored area of evolutionary algorithms opening the SVM decision black box, the paper appoints a cooperative coevolutionary (CC) technique to extract discriminative and compact class prototypes following a SVM model. Various interactions between the SVM and CC are considered, while many experiments test three decisive hypotheses: fidelity to the SVM prediction, superior accuracy to the CC classifier alone and a compact and comprehensive resulting output, achieved through a class-oriented form of feature selection. Results support the hybridization by statistically and visually demonstrating its advantages.     

Fault trees—Problems and the modern state of investigations

Published in Kibernetika i Sistemnyi Analiz, No. 3, pp. 128–150, May–June, 1994.     

Unification of the models for types, classes and state machines

The static model, specified formally, and the dynamic model, represented by hierarchical state machines, are intimately related. By defining a mapping between the two, we are able to provide a definition of inheritance, multiple inheritance and behavioral subtyping for state machines based on that for formally specified types and classes, and provide a graphical representation for formal specifications in terms of state machines. The state machine notation is based on statecharts. It, however, supports both a declarative style, appropriate for types, and an imperative style, appropriate for classes. State machines may be parameterized and may be viewed from different perspectives, based on an arbitrary choice of state predicates. And states are interpreted not as an expression of concurrency, but result from a choice of independent state predicates.     

On the synthesis of adaptive tests for nondeterministic finite state machines

The paper suggests a method for synthesis of adaptive tests with guaranteed coverage for checking functioning of discrete systems whose behavior is described by nondeterministic finite state machines. In contrast to other known methods, we do not represent the complete test as a tree but list test cases one by one and check functioning of the finite state machine on each test case. The complete test detects all defective systems that are r-distinguishable from the reference system. Besides, the test detects other defective systems containing traces that are not present in the specification; but detection of all such systems that are r-compatible with the specification is not guaranteed.     

A necessary and sufficient condition for fundamental periods of cascade machines to be products of the fundamental periods of their constituent finite state machines

Suppose that a finite state machine α produces a periodic sequence (whose fundamental period is A) of nonnegative integer outputs which are used to drive another finite state machine β through a subsequence of its sequence of internal states in the following way. At the jth clock tick of α's clock its integer output a(j) tells β's clock to tick a(j) times (quickly) to drive β numerous steps down its sequence of internal states to the next internal state in this subsequence of its internal states. Suppose that the sequence of outputs of β is periodic with fundamental period B. Suppose that the sum (over any list of A successive entries of the output sequence of α) of α's outputs is S. Then the subsequence of outputs of the cascade machine β ← α consisting of β, driven by α's outputs as described above, is periodic. The fundamental period of the sequence of outputs of the cascade machine β ←a consisting of β driven by α's outputs is no larger than AB. If every output of α is smaller than B, and if S is relatively prime to B, then the fundamental period of the output sequence of this cascade machine is exactly AB. Moreover, every internal state of B occurs exactly A times in each block of AB successive internal states of the cascade machine β ← α. If, on the other hand, S is not relatively prime to B, then the fundamental period of the output sequence of β ← α is less than AB.     

On the complexity of existence of homing sequences for nondeterministic finite state machines

The paper discusses complexity of the problem of checking existence of a homing sequence for an observable complete finite state machines (FSMs). The minimum length of such a sequence for FSMs of certain class is known to be exponential in the number of the FSM states. It is shown that the problem of checking the existence of such a sequence belongs to class PSPACE.     

On the capability of fuzzy set theory to represent concepts

The aim of this paper is to examine the conclusions drawn by Osherson and Smith ["On the adequacy of prototype theory as a theory of concepts", Cognition 9 (1981), pp. 35-58] concerning the inadequacy of the apparatus of fuzzy set theory to represent concepts. Since Osherson and Smith derive their conclusions from specific examples, we show for each of these examples that the respective conclusion they arrive at is not warranted. That is, we demonstrate that fuzzy set theory is sufficiently expressive to represent the various strong intuitions and experimental evidence regarding the relation between simple and combined concepts that are described by Osherson and Smith. To pursue our arguments, we introduce a few relevant notions of fuzzy set theory.     

On the class of L*-language formulas that specify finite-memory finite-state machines

The class of L*-language specifications that specify finite-memory finite-state machines is characterized. The transformation of an L*-language specification into an equivalent specification that specifies a finite-memory finite-state machine is substantiated.     

Modeling and control of discrete event systems using finite state machines with variables and their applications in power grids

Control theories for discrete event systems modeled as finite state machines have been well developed to address various fundamental control issues. However, finite state machine model has long suffered from the problem of state explosion that renders it unsuitable for some practical applications. In an attempt to mitigate the state explosion problem, we propose an efficient representation that appends finite sets of variables to finite state machines in modeling discrete event systems. We also present the control synthesis techniques for such finite state machines with variables (FSMwV). We first present our notion and means of control under this representation. We next present our algorithms for both offline and online synthesis of safety control policies. We then apply these results to the control of electric power grids.     

利用HyperChem获取反应过渡态的方法

利用HyperChem的动态数据交换DDE(Dynamic Data Exchange)功能,通过Excel中的Visual BasicA编程来控制HyperChem的运行,从而控制反应过程中的反应坐标和反应步长,计算得到反应系统沿反应坐标的能量变化曲线,从而可获取反应的过渡态和活化能△E。利用该计算方法搜寻了喹啉分子在S-Mo-Ni催化剂晶体表面催化加氢反应的过渡态,取得较好的效果。利用该方法可以确定复杂反应过渡态,从而为实验研究起理论指导作用。     

Approximation algorithms for the bandwidth minimization problem for a large class of trees

We present approximation algorithms for the bandwidth minimization problem (BMP) for a large class of trees. The BMP is NP-hard, even for trees of maximum node degree 3. The problem finds applications in many areas, including VLSI layout, multiprocessor scheduling, and matrix processing, and has been studied for both graphs and matrices. We study the problem on trees having the following property: given any tree nodev, the depth difference of any two nonempty subtrees rooted atv is bounded by a constantk. We call such treesh(k)trees orgeneralized height-balanced (GHB)trees. The above definition extends the class of balanced trees to trees with depthd=Θ(\N\). For any tree in the above defined class, anO (logd) times optimal algorithm is presented. Furthermore, we extend the application of the algorithm to trees that simulate theh(k) property, which we callh(k)-like trees, and also provide intuitive ideas for an approximation algorithm for general trees. This work has been supported in part by the Computer Learning Research (CLEAR) Center at the University of Texas at Dallas.