An approach to formally modeling and verifying distributed real-time embedded software

作者：Chen Liqiong^*; Fan Guisheng; Liu Yunxiang

来源：Journal of Software, 2010, 5(9): 990-997.

DOI：10.4304/jsw.5.9.990-997

• Analysis process
• Basic properties
• Communication process
• Distributed real-time and embedded systems
• Distributed real-time embedded
• Distributed real-time embedded systems
• Function module
• Internetworked
• Modeling
• Operational conditions
• Reachability graphs
• Software analysis
• Verifying

As computer systems become increasingly internetworked, Distributed Real-time Embedded (DRE) systems has became increasingly common and important, a challenging problem faced by researchers and developers of DRE software is devising and implementing an method that can effectively analyze requirements in varying operational conditions. In this paper, a Hierarchical Distributed Realtime Embedded net (HDRE-net) is proposed as software analysis tool. The basic task, function module and communication process are modeled by using HDRE-net, thus forming the whole application through the synthesis operation of Petri net. Time Reachability Graph is adopted to analyze the correctness of HDRE-net, the basic properties of DRE software are also considered. Finally, a specific example is given to simulate the analysis process, and the results show that the method can be a good solution to analyze DRE software.

• 出版日期2010
• 单位华东理工大学