This paper presents a new level of description between behavioral and state descriptions of a finite-state machine (FSM). The description is termed behavioral phase clustering description. New concepts of behavioral p...This paper presents a new level of description between behavioral and state descriptions of a finite-state machine (FSM). The description is termed behavioral phase clustering description. New concepts of behavioral phase and clustering of behavioral phases in an FSM are introduced. The new description simplifies functional analysis, verification and test of FSM designs. If an FSM is described at low level, some states can be clustered into behavioral phases directly. If it is described at behavioral level, behavioral phases can be extracted from the behavioral description, and clustering of behavioral phases can be performed through easy functional analysis. As one application of behavioral phase clustering descriptions, a new technique employed in a test generation system, ATCLUB, at Register Transfer (RT)-level based on a behavioral phase transition fault model is introduced in this paper. In ATCLUB, test generation process is accelerated through clustering of behavioral phases. Experimental results show that ATCLUB generates test sequence efficiently, with a sharp decrease in vector count at the penalty of a slightly decrease in fault coverage comparing to other ATPC tools.展开更多
We present a method of generating test cases from the software specifications which are modeled by nondeterministic finite state machines. It is applicable to both nondeterministic and deterministic finite state mach...We present a method of generating test cases from the software specifications which are modeled by nondeterministic finite state machines. It is applicable to both nondeterministic and deterministic finite state machines. When applied to deterministic machines, this method yields usually smaller test suites with full fault coverage than the existing methods that also assure full fault coverage. In particular, the proposed mehod can be used to test the control portion of software specified in the formalspecification languages SDL or ESTELLE.展开更多
A formal methodology is proposed to reduce the amount of information displayed to remote human operators at interfaces to large-scale process control plants of a certain type. The reduction proceeds in two stages. In ...A formal methodology is proposed to reduce the amount of information displayed to remote human operators at interfaces to large-scale process control plants of a certain type. The reduction proceeds in two stages. In the first stage, minimal reduced subsets of components, which give full information about the state of the whole system, are generated by determining functional dependencies between components. This is achieved by using a temporal logic proof obligation to check whether the state of all components can be inferred from the state of components in a subset in specified situations that the human operator needs to detect, with respect to a finite state machine model of the system and other human operator behavior. Generation of reduced subsets is automated with the help of a temporal logic model checker. The second stage determines the interconnections between components to be displayed in the reduced system so that the natural overall graphical structure of the system is maintained. A formal definition of an aesthetic for the required subgraph of a graph representation of the full system, containing the reduced subset of components, is given for this purpose. The methodology is demonstrated by a case study.展开更多
Aspect-oriented programming modularizes crosscutting concerns into aspects with the advice invoked at the specified points of program execution. Aspects can be used in a harmful way that invalidates desired properties...Aspect-oriented programming modularizes crosscutting concerns into aspects with the advice invoked at the specified points of program execution. Aspects can be used in a harmful way that invalidates desired properties and even destroys the conceptual integrity of programs. To assure the quality of an aspect-oriented system, rigorous analysis and design of aspects are highly desirable. In this paper, we present an approach to aspect-oriented modeling and verification with finite state machines. Our approach provides explicit notations （e.g., pointcut, advice and aspect） for capturing crosscutting concerns and incremental modification requirements with respect to class state models. For verification purposes, we compose the aspect models and class models in an aspect-oriented model through a weaving mechanism. Then we transform the woven models and the class models not affected by the aspects into FSP （Finite State Processes）, which are to be checked by the LTSA （Labeled Transition System Analyzer） model checker against the desired system properties. We have applied our approach to the modeling and verification of three aspect-oriented systems. To further evaluate the effectiveness of verification, we created a large number of flawed aspect models and verified them against the system requirements. The results show that the verification has revealed all flawed models. This indicates that our approach is effective in quality assurance of aspect-oriented state models. As such, our approach can be used for model-checking state-based specification of aspect-oriented design and can uncover some system design problems before the system is implemented.展开更多
视频内容自动分析领域中,关键的挑战在于如何识别重要对象和如何建模对象之间的时空关系.本文基于感知概念(Perception Concepts,简称PCs)和有限状态机(Finite State Machines,简称FSMs)提出一种语义内容分析模型自动描述和探测体育视...视频内容自动分析领域中,关键的挑战在于如何识别重要对象和如何建模对象之间的时空关系.本文基于感知概念(Perception Concepts,简称PCs)和有限状态机(Finite State Machines,简称FSMs)提出一种语义内容分析模型自动描述和探测体育视频中有意义的语义内容.根据体育视频中可识别的特征元素,定义PCs来表示视频中重要的语义模式;设计PC-FSM模型来描述PCs间的时空关系;采用一个图匹配方法自动探测视频中的高层语义.本文提出的方法使用户能够根据其自身的兴趣和知识设计体育视频的查询描述,并将语义内容探测问题转换为图匹配问题.实验结果验证了本文提出的方法的有效性.展开更多
基金This work was supported by the National Natural Science Foundation of China (Grant No. 69733010)the Youth Science Foundation of Institute of Computing Technology (Grant No. 20016280-18).
文摘This paper presents a new level of description between behavioral and state descriptions of a finite-state machine (FSM). The description is termed behavioral phase clustering description. New concepts of behavioral phase and clustering of behavioral phases in an FSM are introduced. The new description simplifies functional analysis, verification and test of FSM designs. If an FSM is described at low level, some states can be clustered into behavioral phases directly. If it is described at behavioral level, behavioral phases can be extracted from the behavioral description, and clustering of behavioral phases can be performed through easy functional analysis. As one application of behavioral phase clustering descriptions, a new technique employed in a test generation system, ATCLUB, at Register Transfer (RT)-level based on a behavioral phase transition fault model is introduced in this paper. In ATCLUB, test generation process is accelerated through clustering of behavioral phases. Experimental results show that ATCLUB generates test sequence efficiently, with a sharp decrease in vector count at the penalty of a slightly decrease in fault coverage comparing to other ATPC tools.
文摘We present a method of generating test cases from the software specifications which are modeled by nondeterministic finite state machines. It is applicable to both nondeterministic and deterministic finite state machines. When applied to deterministic machines, this method yields usually smaller test suites with full fault coverage than the existing methods that also assure full fault coverage. In particular, the proposed mehod can be used to test the control portion of software specified in the formalspecification languages SDL or ESTELLE.
基金This work was supported by the Royal Society in the UK (No.2004R1)An initial study appeared in Proceedings of IEEE International Conference on Systems,Man and Cybernetics,the Hague,Netherlands,pp.124-129,2004.
文摘A formal methodology is proposed to reduce the amount of information displayed to remote human operators at interfaces to large-scale process control plants of a certain type. The reduction proceeds in two stages. In the first stage, minimal reduced subsets of components, which give full information about the state of the whole system, are generated by determining functional dependencies between components. This is achieved by using a temporal logic proof obligation to check whether the state of all components can be inferred from the state of components in a subset in specified situations that the human operator needs to detect, with respect to a finite state machine model of the system and other human operator behavior. Generation of reduced subsets is automated with the help of a temporal logic model checker. The second stage determines the interconnections between components to be displayed in the reduced system so that the natural overall graphical structure of the system is maintained. A formal definition of an aesthetic for the required subgraph of a graph representation of the full system, containing the reduced subset of components, is given for this purpose. The methodology is demonstrated by a case study.
基金supported in part by the ND EPSCoR IIP-SG via NSF of USA under Grant No.EPS-047679The fourth author was supported in part by the National Natural Science Foundation of China under Grant No.60603036+1 种基金the National Basic Research 973 Program of China under Grant No.2009CB320702the National High-Tech Research and Development 863 Program of China under Grant No.2009AA01Z148
文摘Aspect-oriented programming modularizes crosscutting concerns into aspects with the advice invoked at the specified points of program execution. Aspects can be used in a harmful way that invalidates desired properties and even destroys the conceptual integrity of programs. To assure the quality of an aspect-oriented system, rigorous analysis and design of aspects are highly desirable. In this paper, we present an approach to aspect-oriented modeling and verification with finite state machines. Our approach provides explicit notations （e.g., pointcut, advice and aspect） for capturing crosscutting concerns and incremental modification requirements with respect to class state models. For verification purposes, we compose the aspect models and class models in an aspect-oriented model through a weaving mechanism. Then we transform the woven models and the class models not affected by the aspects into FSP （Finite State Processes）, which are to be checked by the LTSA （Labeled Transition System Analyzer） model checker against the desired system properties. We have applied our approach to the modeling and verification of three aspect-oriented systems. To further evaluate the effectiveness of verification, we created a large number of flawed aspect models and verified them against the system requirements. The results show that the verification has revealed all flawed models. This indicates that our approach is effective in quality assurance of aspect-oriented state models. As such, our approach can be used for model-checking state-based specification of aspect-oriented design and can uncover some system design problems before the system is implemented.
文摘视频内容自动分析领域中,关键的挑战在于如何识别重要对象和如何建模对象之间的时空关系.本文基于感知概念(Perception Concepts,简称PCs)和有限状态机(Finite State Machines,简称FSMs)提出一种语义内容分析模型自动描述和探测体育视频中有意义的语义内容.根据体育视频中可识别的特征元素,定义PCs来表示视频中重要的语义模式;设计PC-FSM模型来描述PCs间的时空关系;采用一个图匹配方法自动探测视频中的高层语义.本文提出的方法使用户能够根据其自身的兴趣和知识设计体育视频的查询描述,并将语义内容探测问题转换为图匹配问题.实验结果验证了本文提出的方法的有效性.
