¹Department of Computer Science and Information Engineering, Shanghai Institute of Technology, Shanghai, China
²Department of Computer Science and Engineering, East China University of Science and Technology, Shanghai, China
³Shanghai Key Laboratory of Computer Software Evaluating and Testing, Shanghai, China

---

Abstract—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.

Index Terms—Distributed real-time and embedded system; Petri net; Time Reachability Graph; modeling; verifying.

[PDF]

Cite: Liqiong Chen, Guisheng Fan, Yunxiang Liu, "An Approach to Formally Modeling and Verifying Distributed Real-time Embedded Software," Journal of Software vol. 5, no. 9, pp. 990-997, 2010.