期刊文献+
共找到49篇文章
< 1 2 3 >
每页显示 20 50 100
Real-time embedded software testing method based on extended finite state machine 被引量:6
1
作者 Yongfeng Yin Bin Liu Hongying Ni 《Journal of Systems Engineering and Electronics》 SCIE EI CSCD 2012年第2期276-285,共10页
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 reliab... 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. 展开更多
关键词 real-time system real-time embedded software for- mal method extended finite state machine (EFSM) testing se- quence test case.
下载PDF
Intrusion Detection for Wireless Mesh Networks using Finite State Machine 被引量:5
2
作者 Yi Ping Wu Yue +1 位作者 Liu Ning Wang Zhiyang 《China Communications》 SCIE CSCD 2010年第5期40-48,共9页
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 protec... 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. 展开更多
关键词 wireless mesh networks SECURITY intrusion detection finite state machine
下载PDF
Artificial emotional model based on finite state machine 被引量:4
3
作者 孟庆梅 吴伟国 《Journal of Central South University of Technology》 EI 2008年第5期694-699,共6页
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 emotiona... 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. 展开更多
关键词 finite state machine artificial emotion model Markov chain SIMULATION
下载PDF
POWER OPTIMIZATION OF FINITE STATE MACHINE BASED ON GENETIC ALGORITHM 被引量:1
4
作者 XiaYinshui A.E.A.Almaini WuXunwei 《Journal of Electronics(China)》 2003年第3期194-201,共8页
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. ... 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. 展开更多
关键词 Finite state machine state assignment Power dissipation Area Genetic algorithm OPTIMIZATION
下载PDF
Verifying the accuracy of interlocking tables for railway signalling systems using abstract state machines 被引量:1
5
作者 Basri Tugcan Celebi Ozgur Turay Kaymakci 《Journal of Modern Transportation》 2016年第4期277-283,共7页
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 re... 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. 展开更多
关键词 Model checking - Abstract state machines Interlocking
下载PDF
EDSM-Based Binary Protocol State Machine Reversing
6
作者 Shen Wang Fanghui Sun +3 位作者 Hongli Zhang Dongyang Zhan Shuang Li Jun Wang 《Computers, Materials & Continua》 SCIE EI 2021年第12期3711-3725,共15页
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 ... 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. 展开更多
关键词 Network security protocol state machine EDSM algorithm protocol reverse engineering protocol analyzing
下载PDF
Global Control Simulation of Electric Vehicle Based on Finite State Machine Theory
7
作者 邹渊 孙逢春 何洪文 《Journal of Beijing Institute of Technology》 EI CAS 2004年第S1期68-72,共5页
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 par... 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. 展开更多
关键词 electric vehicle: finite state machine control algorithm
下载PDF
Balancing four-state continuous-variable quantum key distribution with linear optics cloning machine
8
作者 吴晓东 廖骎 +2 位作者 黄端 吴湘华 郭迎 《Chinese Physics B》 SCIE EI CAS CSCD 2017年第11期97-103,共7页
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). Ben... 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. 展开更多
关键词 four states linear optics cloning machine quantum key distribution
下载PDF
Intelligent decision-making method for vehicles in emergency conditions based on artificial potential fields and finite state machines
9
作者 Xunjia Zheng Huilan Li +6 位作者 Qiang Zhang Yonggang Liu Xing Chen Hui Liu Tianhong Luo Jianjie Gao Lihong Xia 《Journal of Intelligent and Connected Vehicles》 EI 2024年第1期19-29,共11页
This study aims to propose a decision-making method based on artificial potential fields(APFs)and finite state machines(FSMs)in emergency conditions.This study presents a decision-making method based on APFs and FSMs ... This study aims to propose a decision-making method based on artificial potential fields(APFs)and finite state machines(FSMs)in emergency conditions.This study presents a decision-making method based on APFs and FSMs for emergency conditions.By modeling the longitudinal and lateral potential energy fields of the vehicle,the driving state is identified,and the trigger conditions are provided for path planning during lane changing.In addition,this study also designed the state transition rules based on the longitudinal and lateral virtual forces.It established the vehicle decision-making model based on the finite state machine to ensure driving safety in emergency situations.To illustrate the performance of the decision-making model by considering APFs and finite state machines.The version of the model in the co-simulation platform of MATLAB and CarSim shows that the developed decision model in this study accurately generates driving behaviors of the vehicle at different time intervals.The contributions of this study are two-fold.A hierarchical vehicle state machine decision model is proposed to enhance driving safety in emergency scenarios.Mathematical models for determining the transition thresholds of lateral and longitudinal vehicle states are established based on the vehicle potential field model,leading to the formulation of transition rules between different states of autonomous vehicles(AVs). 展开更多
关键词 DECISION-MAKING artificial potential field finite state machines emergency conditions autonomous driving
原文传递
SF^2HDL: A Computational Tool of State Transition Diagram Translation
10
作者 Tiago da Silva Almeida Alexandre César Rodrigues da Silva 《Journal of Mechanics Engineering and Automation》 2013年第2期78-86,共9页
The lack of standard to electronic circuits modeling made possible the development of many tools and modeling languages for electronic circuits. In this way, several tools to be used on different descriptions stage of... The lack of standard to electronic circuits modeling made possible the development of many tools and modeling languages for electronic circuits. In this way, several tools to be used on different descriptions stage of the designs are necessary. This paper presents a tool called SF^2HDL (Stateflow to Hardware Description Language or State Transition Table) that translates a finite state machine on state transition diagram representation, described by Stateflow tool, into an input file standard for TABELA program or into a file behavioral VHDL (Very High Speed Integrated Circuits Hardware Description Language) directly. The TABELA program was used to optimization this finite state machine. After that, the TAB2VHDL program was used to generate the VHDL code on register transfer level, what permits comparisons with results obtained by synthesis. The finite state machine must be described by Mealy model and the user can describe the machine on high level abstraction using all Simulink supports. The tool was very efficient on computational cost and it made translation of several cases, for the two VHDL description models. Every state machine translated was simulated and implemented on device EP2C20F484C7 using Quartus II environment. 展开更多
关键词 Finite state machine VHDL (very high speed integrated circuits hardware description language) synthesis HDB3 (highdensity bipolar 3) computational tool.
下载PDF
基于EFSM的智能车间制造系统生产物流建模与仿真 被引量:1
11
作者 李柳臻 金超 +1 位作者 林廷宇 朱耀琴 《系统仿真学报》 CAS CSCD 北大核心 2023年第12期2655-2668,共14页
制造业的生产物流方式处于不断变革中,对其建模仿真可为制造系统规划设计、分析及改造提供决策支持。依“人-机-物-环-法”分类给出了智能车间制造系统中实体元素的描述,结合EFSM(extended finite state machine)和组件化建模思想,建立... 制造业的生产物流方式处于不断变革中,对其建模仿真可为制造系统规划设计、分析及改造提供决策支持。依“人-机-物-环-法”分类给出了智能车间制造系统中实体元素的描述,结合EFSM(extended finite state machine)和组件化建模思想,建立了生产和物流组件化EFSM模型;阐述了智能车间多作业生产的建模过程以及组件模型实例化方法;通过EFSM-DEVS(discrete event system specification)模型自动转换及DEVS引擎完成了仿真运行。仿真结果表明:该方法所建立的模型更符合车间实际状况,适用性更广;组件化建模思想能构造更具扩展性的软件;建模及仿真运行的3D可视化使软件直观性更好,其仿真结果与AnyLogic保持一致。 展开更多
关键词 生产物流建模与仿真 EFSM(extended finite state machine) 组件化建模 DEVS(discrete event system specification) 多作业建模
下载PDF
M-LSM:An Improved Multi-Liquid State Machine for Event-Based Vision Recognition
12
作者 王蕾 郭莎莎 +2 位作者 曲连华 田烁 徐炜遐 《Journal of Computer Science & Technology》 SCIE EI CSCD 2023年第6期1288-1299,共12页
Event-based computation has recently gained increasing research interest for applications of vision recogni-tion due to its intrinsic advantages on efficiency and speed.However,the existing event-based models for visi... Event-based computation has recently gained increasing research interest for applications of vision recogni-tion due to its intrinsic advantages on efficiency and speed.However,the existing event-based models for vision recogni-tion are faced with several issues,such as large network complexity and expensive training cost.In this paper,we propose an improved multi-liquid state machine(M-LSM)method for high-performance vision recognition.Specifically,we intro-duce two methods,namely multi-state fusion and multi-liquid search,to optimize the liquid state machine(LSM).Multi-state fusion by sampling the liquid state at multiple timesteps could reserve richer spatiotemporal information.We adapt network architecture search(NAS)to find the potential optimal architecture of the multi-liquid state machine.We also train the M-LSM through an unsupervised learning rule spike-timing dependent plasticity(STDP).Our M-LSM is evalu-ated on two event-based datasets and demonstrates state-of-the-art recognition performance with superior advantages on network complexity and training cost. 展开更多
关键词 liquid state machine bio-inspired learning classification event-based vision
原文传递
Modeling and TOPSIS-GRA Algorithm for Autonomous Driving Decision-Making Under 5G-V2X Infrastructure
13
作者 Shijun Fu Hongji Fu 《Computers, Materials & Continua》 SCIE EI 2023年第4期1051-1071,共21页
This paper is to explore the problems of intelligent connected vehicles(ICVs)autonomous driving decision-making under a 5G-V2X structured road environment.Through literature review and interviews with autonomous drivi... This paper is to explore the problems of intelligent connected vehicles(ICVs)autonomous driving decision-making under a 5G-V2X structured road environment.Through literature review and interviews with autonomous driving practitioners,this paper firstly puts forward a logical framework for designing a cerebrum-like autonomous driving system.Secondly,situated on this framework,it builds a hierarchical finite state machine(HFSM)model as well as a TOPSIS-GRA algorithm for making ICV autonomous driving decisions by employing a data fusion approach between the entropy weight method(EWM)and analytic hierarchy process method(AHP)and by employing a model fusion approach between the technique for order preference by similarity to an ideal solution(TOPSIS)and grey relational analysis(GRA).The HFSM model is composed of two layers:the global FSM model and the local FSM model.The decision of the former acts as partial input information of the latter and the result of the latter is sent forward to the local pathplanning module,meanwhile pulsating feedback to the former as real-time refresh data.To identify different traffic scenarios in a cerebrum-like way,the global FSM model is designed as 7 driving behavior states and 17 driving characteristic events,and the local FSM model is designed as 16 states and 8 characteristic events.In respect to designing a cerebrum-like algorithm for state transition,this paper firstly fuses AHP weight and EWM weight at their output layer to generate a synthetic weight coefficient for each characteristic event;then,it further fuses TOPSIS method and GRA method at the model building layer to obtain the implementable order of state transition.To verify the feasibility,reliability,and safety of theHFSMmodel aswell as its TOPSISGRA state transition algorithm,this paper elaborates on a series of simulative experiments conducted on the PreScan8.50 platform.The results display that the accuracy of obstacle detection gets 98%,lane line prediction is beyond 70 m,the speed of collision avoidance is higher than 45 km/h,the distance of collision avoidance is less than 5 m,path planning time for obstacle avoidance is averagely less than 50 ms,and brake deceleration is controlled under 6 m/s2.These technical indexes support that the driving states set and characteristic events set for the HFSM model as well as its TOPSIS-GRA algorithm may bring about cerebrum-like decision-making effectiveness for ICV autonomous driving under 5G-V2X intelligent road infrastructure. 展开更多
关键词 5G-V2X cerebrum-like autonomous driving driving behavior decision-making hierarchical finite state machines TOPSIS-GRA algorithm
下载PDF
DSML ProcGraph: Overview and a Mid-Size Industrial Application Example
14
作者 Giovanni Godena Miha Glavan 《Journal of Software Engineering and Applications》 2023年第8期315-347,共7页
This paper presents model-based approach to process-control software development. The presented approach enables modelling of control software in a straightforward manner and, at the same time, on a high level of abst... This paper presents model-based approach to process-control software development. The presented approach enables modelling of control software in a straightforward manner and, at the same time, on a high level of abstraction. The essence of the presented approach is a high-level, domain-specific modelling language ProcGraph, which is based on three types of diagrams that describe the modelled system using a domain-oriented hierarchical structure of interdependent procedural control entities and state-transition diagrams describing the behaviour of the procedural control entities. The presented concept is demonstrated by means of higher-level model segments of a real process-control application that deals with the micronisation process in the production of titanium dioxide. The presented industrial case shows that the application of ProcGraph provides adequate expressive power for an elegant preparation of graphic specifications in a transparent and easy way. 展开更多
关键词 Model-Driven Software Engineering Domain-Specific Modelling Languages Process-Control Software state machines Titanium Dioxide
下载PDF
Design of intelligent controller for mobile robot based on fuzzy logic 被引量:3
15
作者 高鸣 宋爱国 《Journal of Southeast University(English Edition)》 EI CAS 2010年第1期62-67,共6页
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 mob... 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. 展开更多
关键词 mobile robot path tracking obstacle avoidance fuzzy logic finite state machine
下载PDF
Problem of interoperability in semantic web service system
16
作者 满君丰 彭三城 +1 位作者 向剑伟 胡永祥 《Journal of Southeast University(English Edition)》 EI CAS 2006年第3期306-310,共5页
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 i... 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. 展开更多
关键词 semantic services-oriented architecture abstract state machine service interface INTEROPERABILITY
下载PDF
Research of NS dataflow mechanism and its analyzer implementation
17
作者 金烨 樊隽 《Journal of Southeast University(English Edition)》 EI CAS 2003年第1期44-48,共5页
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. Base... 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. 展开更多
关键词 network simulation NS simulator dataflow analysis state machine
下载PDF
Test Data Generation for Stateful Network Protocol Fuzzing Using a Rule-Based State Machine 被引量:13
18
作者 Rui Ma Daguang Wang +2 位作者 Changzhen Hu Wendong Ji Jingfeng Xue 《Tsinghua Science and Technology》 SCIE EI CAS CSCD 2016年第3期352-360,共9页
To improve the efficiency and coverage of stateful network protocol fuzzing, this paper proposes a new method, using a rule-based state machine and a stateful rule tree to guide the generation of fuzz testing data. Th... To improve the efficiency and coverage of stateful network protocol fuzzing, this paper proposes a new method, using a rule-based state machine and a stateful rule tree to guide the generation of fuzz testing data. The method first builds a rule-based state machine model as a formal description of the states of a network protocol. This removes safety paths, to cut down the scale of the state space. Then it uses a stateful rule tree to describe the relationship between states and messages, and then remove useless items from it. According to the message sequence obtained by the analysis of paths using the stateful rule tree and the protocol specification, an abstract data model of test case generation is defined. The fuzz testing data is produced by various generation algorithms through filling data in the fields of the data model. Using the rule-based state machine and the stateful rule tree, the quantity of test data can be reduced. Experimental results indicate that our method can discover the same vulnerabilities as traditional approaches, using less test data, while optimizing test data generation and improving test efficiency. 展开更多
关键词 FUZZING stateful network protocol test data generation rule-based state machine stateful rule tree
原文传递
Specifying Requirements of Real-Time System with Rules and Templates 被引量:8
19
作者 Wu Guo-qing Xiao Hai-feng +1 位作者 Zheng Pen Ying Shi 《Wuhan University Journal of Natural Sciences》 EI CAS 2000年第3期278-284,共7页
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 m... 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. 展开更多
关键词 requirements specification model requirements specification real-time system finite state machine
下载PDF
Towards a Formal Semantics for UML/MARTE State Machines Based on Hierarchical Timed Automata 被引量:7
20
作者 Yu Zhou Luciano Baresi Matteo Rossi 《Journal of Computer Science & Technology》 SCIE EI CSCD 2013年第1期188-202,共15页
UML is a widely-used, general purpose modeling language. But its lack of a rigorous semantics forbids the thorough analysis of designed solution, and thus precludes the discovery of significant problems at design time... UML is a widely-used, general purpose modeling language. But its lack of a rigorous semantics forbids the thorough analysis of designed solution, and thus precludes the discovery of significant problems at design time. To bridge the gap, the paper investigates the underlying semantics of UML state machine diagrams, along with the time-related modeling elements of MARTE, the profile for modeling and analysis of real-time embedded systems, and proposes a formal operational semantics based on extended hierarchical timed automata. The approach is exemplified on a simple example taken from the automotive domain. Verification is accomplished by translating designed models into the input language of the UPPAAL model checker. 展开更多
关键词 timed automata state machine diagram formal semantics
原文传递
上一页 1 2 3 下一页 到第
使用帮助 返回顶部