Real-time embedded software testing method based on extended finite state machine

The reliability of real-time embedded software directly determines the reliability of the whole real-time embedded sys- tem, and the effective software testing is an important way to ensure software quality and reliability. Based on the analysis of the characteristics of real-time embedded software, the formal method is introduced into the real-time embedded software testing field and the real-time extended finite state machine （RT-EFSM） model is studied firstly. Then, the time zone division method of real-time embedded system is presented and the definition and description methods of time-constrained transition equivalence class （timeCTEC） are presented. Furthermore, the approaches of the testing sequence and test case generation are put forward. Finally, the proposed method is applied to a typical avionics real- time embedded software testing practice and the examples of the timeCTEC, testing sequences and test cases are given. With the analysis of the testing result, the application verification shows that the proposed method can effectively describe the real-time embedded software state transition characteristics and real-time requirements and play the advantages of the formal methods in accuracy, effectiveness and the automation supporting. Combined with the testing platform, the real-time, closed loop and automated simulation testing for real-time embedded software can be realized effectively.

Intrusion Detection for Wireless Mesh Networks using Finite State Machine

Wireless Mesh Networks is vulnerable to attacks due to the open medium, dynamically changing network topology, cooperative algorithms, Lack of centralized monitoring and management point. The traditional way of protecting networks with firewalls and encryption software is no longer suffi- cient and effective for those features. In this paper, we propose a distributed intrusion detection ap- proach based on timed automata. A cluster-based detection scheme is presented, where periodically a node is elected as the monitor node for a cluster. These monitor nodes can not only make local intrusion detection decisions, but also cooperatively take part in global intrusion detection. And then we con- struct the Finite State Machine （FSM） by the way of manually abstracting the correct behaviors of the node according to the routing protocol of Dynamic Source Routing （DSR）. The monitor nodes can verify every node＇s behavior by the Finite State Ma- chine （FSM）, and validly detect real-time attacks without signatures of intrusion or trained data.Compared with the architecture where each node is its own IDS agent, our approach is much more efficient while maintaining the same level of effectiveness. Finally, we evaluate the intrusion detection method through simulation experiments.

Artificial emotional model based on finite state machine

According to the basic emotional theory, the artificial emotional model based on the finite state machine（FSM） was presented. In finite state machine model of emotion, the emotional space included the basic emotional space and the multiple emotional spaces. The emotion-switching diagram was defined and transition fimction was developed using Markov chain and linear interpolation algorithm. The simulation model was built using Stateflow toolbox and Simulink toolbox based on the Matlab platform. And the model included three subsystems： the input one, the emotion one and the behavior one. In the emotional subsystem, the responses of different personalities to the external stimuli were described by defining personal space. This model takes states from an emotional space and updates its state depending on its current state and a state of its input （also a state-emotion）. The simulation model realizes the process of switching the emotion from the neutral state to other basic emotions. The simulation result is proved to correspond to emotion-switching law of human beings.

POWER OPTIMIZATION OF FINITE STATE MACHINE BASED ON GENETIC ALGORITHM

Using state assignment to minimize power dissipation and area for finite state ma-chines is computationally hard. Most of published results show that the reduction of switchingactivity often trades with area penalty. In this paper, a new approach is proposed. Experimentalresults show a significant reduction of switching activity without area penalty compared withprevious publications.

Verifying the accuracy of interlocking tables for railway signalling systems using abstract state machines

Railway transportation system is a critical sector where design methods and techniques are defined by international standards in order to reduce possible risks to an acceptable minimum level. CENELEC 50128 strongly recommends the utilization of finite state machines during system modelling stage and formal proof methods during the verifi- cation and testing stages of control algorithms. Due to the high importance of interlocking table at the design state of a sig- nalization system, the modelling and verification of inter- locking tables are examined in this work. For this purpose, abstract state machines are used as a modelling tool. The developed models have been performed in a generalized structure such that the model control can be done automatically for the interlocking systems. In this study, NuSMV is used at the verification state. Also, the consistency of the developed models has been supervised through fault injection. The developed models and software components are applied on a real railway station operated by Metro Istanbul Co.

EDSM-Based Binary Protocol State Machine Reversing

Internet communication protocols define the behavior rules of network components when they communicate with each other.With the continuous development of network technologies,many private or unknown network protocols are emerging in endlessly various network environments.Herein,relevant protocol specifications become difficult or unavailable to translate in many situations such as network security management and intrusion detection.Although protocol reverse engineering is being investigated in recent years to perform reverse analysis on the specifications of unknown protocols,most existing methods have proven to be time-consuming with limited efficiency,especially when applied on unknown protocol state machines.This paper proposes a state merging algorithm based on EDSM(Evidence-Driven State Merging)to infer the transition rules of unknown protocols in form of state machines with high efficiency.Compared with another classical state machine inferring method based on Exbar algorithm,the experiment results demonstrate that our proposed method could run faster,especially when dealing with massive training data sets.In addition,this method can also make the state machines have higher similarities with the reference state machines constructed from public specifications.

Global Control Simulation of Electric Vehicle Based on Finite State Machine Theory

Finite state machine theory (FSM) is introduced and applied to global control of electric vehicle. Theoretical adaptation for application of FSM in control of electric vehicle is analyzed. Global control logic for parts of electric vehicle is analyzed and built based on FSM. Using Matlab/Simulink, BJD6100-HEV global control algorithm is modeled and prove validity by simulation.

Balancing four-state continuous-variable quantum key distribution with linear optics cloning machine

We show that the secret key generation rate can be balanced with the maximum secure distance of four-state continuous-variable quantum key distribution（CV-QKD） by using the linear optics cloning machine（LOCM）. Benefiting from the LOCM operation, the LOCM-tuned noise can be employed by the reference partner of reconciliation to achieve higher secret key generation rates over a long distance. Simulation results show that the LOCM operation can flexibly regulate the secret key generation rate and the maximum secure distance and improve the performance of four-state CV-QKD protocol by dynamically tuning parameters in an appropriate range.

Design of intelligent controller for mobile robot based on fuzzy logic

In order to improve a mobile robot＇s autonomy in unknown environments, a novel intelligent controller is designed. The proposed controller is based on fuzzy logic with the aim of assisting a multi-sensor equipped mobile robot to safely navigate in an indoor environment. First, the designs of two behaviors for a robot＇s autonomous navigation are described, including path tracking and obstacle avoidance, which emulate human driving behaviors and reduce the complexity of the robot＇s navigation problems in unknown environments. Secondly, the two behaviors are combined by using a finite state machine （FSM）, which ensures that the robot can safely track a predefined path in an unknown indoor environment. The inputs to this controller are the readings from the sensors. The corresponding output is the desired direction of the robot. Finally, both the simulation and experimental results verify the effectiveness of the proposed method.

Problem of interoperability in semantic web service system

In order to fully realize semantic interoperability among distributed and heterogeneous applications on the web, a set of effective interoperability mechanisms is presented. This mechanism adopts service interactive interfaces （SII） and service aggregative interfaces （SAI） modeled with abstract state machine （ASM） to abstractly describe the behavior of the invoked web service instances, which makes business processing accurately specify tasks and effectively solves the problems of communication and collaboration between service providers and service requesters. The mechanism also uses appropriate mediators to solve the problems of information and coinmunication incompatibility during the course of service interaction, which is convenient for service interoperability, sharing and integration. The mechanism＇ s working principle and interoperability implementation are illustrated by a use case in detail.

Research of NS dataflow mechanism and its analyzer implementation

This paper analyzes the main elements in NS network simulator, makes adetailed view of dataflow management in a link, a node, and an agent, respectively, and introducesthe information described by its trace file. Based on the analysis of transportation and treatmentof different packets in NS, a dataflow state machine is proposed with its states exchange triggeringevents and a dataflow analyzer is designed and implemented according to it. As the machine statefunctions, the analyzer can make statistic of total transportation flux of a specified dataflow andoffer a general fluctuation diagram. Finally, a concrete example is used to test its performance.

基于EFSM的智能车间制造系统生产物流建模与仿真

制造业的生产物流方式处于不断变革中,对其建模仿真可为制造系统规划设计、分析及改造提供决策支持。依“人-机-物-环-法”分类给出了智能车间制造系统中实体元素的描述,结合EFSM(extended finite state machine)和组件化建模思想,建立了生产和物流组件化EFSM模型;阐述了智能车间多作业生产的建模过程以及组件模型实例化方法;通过EFSM-DEVS(discrete event system specification)模型自动转换及DEVS引擎完成了仿真运行。仿真结果表明:该方法所建立的模型更符合车间实际状况,适用性更广;组件化建模思想能构造更具扩展性的软件;建模及仿真运行的3D可视化使软件直观性更好,其仿真结果与AnyLogic保持一致。

Specifying Requirements of Real-Time System with Rules and Templates

This paper presents a model specifying requirements of real-time systems. Different from existing researches, this model mainly uses rules and templates to represent hierarchical FSMs (Finite State Machine). In this model, one rule corresponds to one state transition of FSM and one template corresponds to one FSM. Rules and information with respect to a FSM can be written in a template. So templates include not only state diagrams, but also information that can not be described by FSM, such as performance requirements. The specification using this model consists of a collection of templates and it is easy for users to understand and to review. After introduced the related researches and principles of the model, this paper specifies requirements of a real-time system with this model, and discusses characters of this model in the end.

Multiple UIO-based test sequence generation for distributed systems

In developing distributed systems, conformance testing is required to determine whether an implementation under test （IUT） conforms to its specification. With distributed test architectures involving multiple remote testers, testing approaches may become more complicated because of issues known as controllability and observability problems. Based on a finite state machine （FSM） representation of the system＇s specification, this paper proposes a new method to generate a test sequence utilizing multiple UIO sequences. The method is essentially guided by the way of minimizing the use of external coordination messages and input/output operations. Experiments are given to evaluate the proposed method.

An EFSM-Based Test Data Generation Approach in Model-Based Testing

Testing is an integral part of software development.Current fastpaced system developments have rendered traditional testing techniques obsolete.Therefore,automated testing techniques are needed to adapt to such system developments speed.Model-based testing(MBT)is a technique that uses system models to generate and execute test cases automatically.It was identified that the test data generation(TDG)in many existing model-based test case generation(MB-TCG)approaches were still manual.An automatic and effective TDG can further reduce testing cost while detecting more faults.This study proposes an automated TDG approach in MB-TCG using the extended finite state machine model(EFSM).The proposed approach integrates MBT with combinatorial testing.The information available in an EFSM model and the boundary value analysis strategy are used to automate the domain input classifications which were done manually by the existing approach.The results showed that the proposed approach was able to detect 6.62 percent more faults than the conventionalMB-TCG but at the same time generated 43 more tests.The proposed approach effectively detects faults,but a further treatment to the generated tests such as test case prioritization should be done to increase the effectiveness and efficiency of testing.

OPEN ARCHITECTURE CNC SYSTEM HITCNC AND KEY TECHNOLOGY

Aiming at the characteristics of modularity and reconfigurable in open architecture computer numerical control （CNC） system, the open architecture CNC system, Harbin Institute of Tech- nology computer numerical control （HITCNC）, is researched and manufactured based on the interface standards. The system＇s external interfaces are coincident with the corresponding international standards, and the internal interfaces follow the open modular architecture controller （OMAC） agreement. In the research and manufacturing process, object-oriented technology is used to ensure the openness of the HITCNC, and static programming is applied in the CNC system according to the idea of modularization disassembly. The HITCNC also actualizes real-time and unreal-time modules adopting real-time dynamical linked library （RTDLL） and component object model （COM）. Finite state ma- chine （FSM） is adopted to do dynamically modeling of HITCNC. The complete separation between the software and the hardware is achieved in the HITCNC by applying the SoftSERCANS technique. The application of the above key techniques decreases the programming workload greatly, and uses software programs replacing hardware functions, which offers plenty technique ensures for the openness of HITCNC. Finally, based on the HITCNC, a three-dimensional milling system is established. On the system, series experiments are done to validate the expandability and interchangeability of HITCNC. The results of the experiments show that the established open architecture CNC system HITCNC is correct and feasible, and has good openness.

Formal Verification of TASM Models by Translating into UPPAAL

Timed abstract state machine(TASM) is a formal specification language used to specify and simulate the behavior of real-time systems. Formal verification of TASM model can be fulfilled through model checking activities by translating into UPPAAL. Firstly, the translational semantics from TASM to UPPAAL is presented through atlas transformation language(ATL). Secondly, the implementation of the proposed model transformation tool TASM2UPPAAL is provided. Finally, a case study is given to illustrate the automatic transformation from TASM model to UPPAAL model.

A Joint Model of Device Load and User Intention in Load Monitoring

In this paper, a concept for the joint modeling of the device load and user intention is presented. It consists of two coupled models, a device load model to characterize the power consumption of an electric device of interest, and a user intention model for describing the user intentions which cause the energy consumption. The advantage of this joint model is the ability to predict the device load from the user intention and to reconstruct the user intention from the measured device load. This opens a new way for load monitoring, simulation and prediction from the perspective of users instead of devices.

Formal Reduction of Interfaces to Large-scale Process Control Systems

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.

Remolding Diversified Objects in Ada95: Toward A Object Pattern

Ada provides full capacities of supporting object orientation, but the diversified objects patterned in Ada are so intricate that Ada95's aim would be demolished. In order to complement the disfigurement that Ada does lack for a pristine notion of class, this paper presents a remolded object pattern known as A object, an Ada based class description language A ObjAda aiming at support for A object pattern and the related approach for key algorithms and implementation. In consequent, A ObjAda hereby promotes Ada with highlighted object orientation, which not only effectively exploits the capacities in Ada95, but also rationally hides befuddling concepts from Ada95.