|
Journal of Computer Science and Technology ›› 2020, Vol. 35 ›› Issue (6): 1324-1342.doi: 10.1007/s11390-020-0537-8
Special Issue: Software Systems
Previous Articles Next Articles
Qian-Qian Lin1, Shu-Ling Wang1, Member, CCF, Bo-Hua Zhan1, Member, CCF, and Bin Gu2,*, Member, CCF
[1] Andrès F, Boulos J. DDS:The data delivery service. In Proc. the IFIP World Conference on IT Tools, September 1996, pp.487-494. [2] Hugues J, Pautet L, Kordon F. A framework for DRE middleware, an application to DDS. In Proc. the 9th IEEE International Symposium on Object and Component-Oriented Real-Time Distributed Computing, April 2006, pp.224-231. [3] Almadani B. RTPS middleware for real-time distributed industrial vision systems. In Proc. the 11th IEEE International Conference on Embedded and Real-Time Computing Systems and Applications, August 2005, pp.361-364. [4] Almadani B, Al-Saeedi M, Al-Roubaiey A. Scalable wireless video streaming over real-time publish subscribe protocol (RTPS). In Proc. the 17th IEEE/ACM International Symposium on Distributed Simulation and Real Time Applications, October 2013, pp.221-230. [5] Behrmann G, David A, Larsen K G. A tutorial on UPPAAL. In Proc. International School on Formal Methods for the Design of Computer, Communication and Software Systems, September 2004, pp.200-236. [6] David A, Larsen K G, Legay A, Mikucionis M, Poulsen D B. UPPAAL SMC tutorial. International Journal on Software Tools for Technology Transfer, 2015, 17(4):397-415. [7] Beckman K, Reininger J. Adaptation of the DDS security standard for resource-constrained sensor networks. In Proc. the 13th International Symposium on Industrial Embedded Systems, June 2018. [8] Youssef T A, Hariri M E, Elsayed A T, Mohammed O A. A DDS-based energy management framework for small microgrid operation and control. IEEE Trans. Industrial Informatics, 2018, 14(3):958-968. [9] Pérez H, Gutiérrez J J. Modelling the QoS parameters of DDS for event-driven real-time applications. Journal of Systems and Software, 2015, 104:126-140. [10] Alaerjan A, Kim D, Kafaf D A. Modeling functional behaviors of DDS. In Proc. the IEEE SmartWorld, Ubiquitous Intelligence & Computing, Advanced & Trusted Computed, Scalable Computing & Communications, Cloud & Big Data Computing, Internet of People and Smart City Innovation, August 2017. [11] Kleppe A. Object constraint language:Metamodeling semantics. In UML 2 Semantics and Applications, Lano K (ed.), Wiley, 2009, pp.163-178. [12] Liu Y, Guan Y, Li X, Wang R, Zhang J. Formal analysis and verification of DDS in ROS2. In Proc. the 16th ACM/IEEE International Conference on Formal Methods and Models for System Design, October 2018, pp.62-66. [13] Yin J, Zhu H, Fei W, Xu Q, Wu R. Formalization and verification of RTPS StatefulWriter module using CSP. In Proc. the 31st International Conference on Software Engineering and Knowledge Engineering, July 2019, pp.147-198. [14] Brookes S D, Hoare C A R, Roscoe A W. A theory of communicating sequential processes. Journal of the ACM, 1984, 31(3):560-599. [15] Hoare C A R. Communicating Sequential Processes. Prentice-Hall, 1985. [16] Yang Y, Jiang Y, Gu M, Sun J. Verifying Simulink Stateflow model:Timed automata approach. In Proc. the 31st IEEE/ACM International Conference on Automated Software Engineering, September 2016, pp.852-857. [17] Kang E, Ke L, Hua M, Wang Y. Verifying automotive systems in EAST-ADL/Stateflow using UPPAAL. In Proc. the 2015 Asia-Pacific Software Engineering Conference, December 2015, pp.143-150. [18] Hamon G, Rushby J. An operational semantics for Stateflow. International Journal on Software Tools for Technology Transfer, 2007, 9(5/6):447-456. [19] Tiwari A. Formal semantics and analysis methods for Simulink/Stateflow models. Technical Report, SRI International, 2002. http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.1.3492, Mar. 2020. [20] Zou L, Zhan N, Wang S, Fränzle M. Formal verification of Simulink/Stateflow diagrams. In Proc. the 13th International Symposium on Automated Technology for Verification and Analysis, October 2015, pp.464-481. [21] Chen C, Sun J, Liu Y et al. Formal modeling and validation of Stateflow diagrams. International Journal on Software Tools for Technology Transfer, 2012, 14(6):653-671. [22] Alur R, Dill D L. A theory of timed automata. Theoretical Computer Science, 1994, 126(2):183-235. [23] Berhmann G, David A, Larsen K G, Pettersson P, Yi W. Developing UPPAAL over 15 years. Software-Practice and Experience, 2011, 41(2):133-142. [24] Younes H L S, Kwiatkowska M, Normaln G, Parker D. Numerical vs. statistical probabilistic model checking. International Journal on Software Tools for Technology Transfer, 2007, 15(11):1427-1434. [25] Georgios E F, George J P. Robust sampling for MITL specifications. In Proc. the 5th International Conference on Formal Modeling and Analysis of Timed Systems, Oct. 2007, pp.147-162. [26] Grumberg O, Long D E. Model checking and modular verification. ACM Transactions on Programming Languages and Systems, 1994, 16(3):843-871. |
[1] | Zhi Ma, Lei Qiao, Meng-Fei Yang, Shao-Feng Li, Jin-Kun Zhang. Verification of Real Time Operating System Exception Management Based on SPARCv8 [J]. Journal of Computer Science and Technology, 2021, 36(6): 1367-1387. |
[2] | Jingwen Xu, Yanhong Huang, Jianqi Shi, Shengchao Qin. A Multi-Agent Spatial Logic for Scenario-Based Decision Modeling and Verification in Platoon Systems [J]. Journal of Computer Science and Technology, 2021, 36(6): 1231-1247. |
[3] | Zhao-Hui Li, Xin-Yu Feng. Verifying Contextual Refinement with Ownership Transfer [J]. Journal of Computer Science and Technology, 2021, 36(6): 1342-1366. |
[4] | Jia-Qi Yin, Hui-Biao Zhu, Yuan Fei. Specification and Verification of the Zab Protocol with TLA+ [J]. Journal of Computer Science and Technology, 2020, 35(6): 1312-1323. |
[5] | Jun-Peng Zha, Xin-Yu Feng, Lei Qiao. Modular Verification of SPARCv8 Code [J]. Journal of Computer Science and Technology, 2020, 35(6): 1382-1405. |
[6] | Hui-Na Chao, Hua-Wei Li, Xiaoyu Song, Tian-Cheng Wang, Xiao-Wei Li. Evaluating and Constraining Hardware Assertions with Absent Scenarios [J]. Journal of Computer Science and Technology, 2020, 35(5): 1198-1216. |
[7] | Zi-Peng Zhang, Ming Fu, Xin-Yu Feng. A Lightweight Dynamic Enforcement of Privacy Protection for Android [J]. Journal of Computer Science and Technology, 2019, 34(4): 901-923. |
[8] | Wen-Min Li, Xue-Lei Li, Qiao-Yan Wen, Shuo Zhang, Hua Zhang. Flexible CP-ABE Based Access Control on Encrypted Data for Mobile Users in Hybrid Cloud System [J]. , 2017, 32(5): 974-990. |
[9] | Mert Ozkaya. Visual Specification and Analysis of Contract-Based Software Architectures [J]. , 2017, 32(5): 1025-1043. |
[10] | Peng-Yi Hao, Yang Xia, Xiao-Xin Li, Sei-ichiro Kamata, Sheng-Yong Chen. Discriminative Histogram Intersection Metric Learning and Its Applications [J]. , 2017, 32(3): 507-519. |
[11] | Cinzia Bernardeschi, Luca Cassano, Andrea Domenici. SRAM-Based FPGA Systems for Safety-Critical Applications: A Survey on Design Standards and Proposed Methodologies [J]. , 2015, 30(2): 373-390. |
[12] | Wen-Gang Zhou, Hou-Qiang Li, Yijuan Lu, Qi Tian. Encoding Spatial Context for Large-Scale Partial-DuplicateWeb Image Retrieval [J]. , 2014, 29(5): 837-848. |
[13] | Tao Xie, Lu Zhang, Xusheng Xiao, Ying-Fei Xiong, and Dan Hao. Cooperative Software Testing and Analysis:Advances and Challenges [J]. , 2014, 29(4): 713-723. |
[14] | Zhao-Peng Li, Yu Zhang, and Yi-Yun Chen. A Shape Graph Logic and A Shape System [J]. , 2013, 28(6): 1063-1084. |
[15] | Jun-Wei Cao, (曹军威), Member, CCF, ACM, Senior Member, IEEE, Fan Zhang (张帆), Student Member, IEEE, Ke Xu (许可), Lian-Chen Liu (刘连臣) and Cheng Wu (吴澄). Formal Verification of Temporal Properties for Reduced Overhead in Grid Scientific Workflows [J]. , 2011, 26(6): 1017-1030. |
|
|