A novel requirement analysis approach for periodic control systems

详细信息    查看全文

• 作者：Zheng Wang (12008) (22008)
  Geguang Pu (12008)
  Jiangwen Li (12008)
  Yuxiang Chen (12008)
  Yongxin Zhao (12008) (32008)
  Mingsong Chen (12008)
  Bin Gu (22008)
  Mengfei Yang (42008)
  Jifeng He (12008)
  
• 关键词：SPARDL ; simulation ; dataflow analysis ; code generation
• 刊名：Frontiers of Computer Science in China
• 出版年：2013
• 出版时间：April 2013
• 年：2013
• 卷：7
• 期：2
• 页码：214-235
• 全文大小：2234KB
• 参考文献：1. Alur R, Dill D L. A theory of timed automata. Theoretical Computer Science, 1994, 126: 183鈥?35 CrossRef
  2. Ouaknine J, Schneider S. Timed csp: a retrospective. Electronics Notes in Theoretical Computer Science, 2006, 162: 273鈥?76 CrossRef
  3. Baresi L, Pezz猫 M. An introduction to software testing. Electronics Notes in Theoretical Computer Science, 2006, 148(1): 89鈥?11 CrossRef
  4. Zhang J. Specification analysis and test data generation by solving Boolean combinations of numeric constraints. In: Proceedings of Asia-Pacific Conference on Quality Software (APAQS). 2000, 267鈥?74 CrossRef
  5. Staats M, Whalen M W, Heimdahl M P. Programs, tests, and oracles: the foundations of testing revisited. In: Proceedings of the International Conference on Software Engineering (ICSE). 2011, 391鈥?00
  6. Chen M, Mishra P, Kalita D. Efficient test case generation for validation of UML activity diagrams. Design Automation for Embedded Systems, 2010, 14: 105鈥?30 CrossRef
  7. Chen M, Mishra P. Property learning techniques for efficient generation of directed tests. IEEE Trans. Computers, 2011, 60(6): 852鈥?64 CrossRef
  8. Wang Z, Yu X, Sun T, Pu G, Ding Z, Hu J. Test data generation for derived types in c program. In: Proceedings of the 3rd IEEE International Symposium on Theoretical Aspects of Software Engineering. 2009, 155鈥?62
  9. Plotkin G D. A structural approach to operational semantics. Journal of Logic and Algebra Programming, 2004, 60鈥?1: 17鈥?39
  10. Wang Z, Li J, Zhao Y, Qi Y, Pu G, He J, Gu B. SPARDL: a requirement modeling language for periodic control system. In: Proceedings of International Symposium on Leveraging Applications (ISoLA). 2010, 594鈥?08
  11. Li J, Wang Z, Zhao Y, Pu G, Qi Y, Gu B. An event-b interpretation for spardl model. In: Proceedings of the 13th International Symposium on High-Assurance System Engineering. 2011, 41鈥?8
  12. Nielson F, Nielson H R, Hankin C. Principles of program analysis. Secaucus, NJ, USA: Springer-Verlag New York, Inc., 1999 CrossRef
  13. Hammond K, Michaelson G. Hume: a domain-specific language for real-time embedded systems. In: Proceedings of Conference on Generative Programming and Component Engineering (GPCE). 2003, 37鈥?6 CrossRef
  14. Heitmeyer C. Using the scr toolset to specify software requirements. In: Proceedings of the IEEE Workshop on Industrial Strength Formal Specification Techniques (WIFT). 1998, 12鈥?3
  15. Clements P C. A survey of architecture description languages. In: Proceedings of the 8th International Workshop on Software Specification and Design (IWSSD). 1996, 16鈥?5 CrossRef
  16. Jahanian F, Mok A K. Modechart: a specification language for realtime systems. IEEE Transactions on Software Engineering, 1994, 20: 933鈥?47 CrossRef
  17. Oh H, Ha S. Hardware-software cosynthesis of multi-mode multi-task embedded systems with real-time constraints. In: Proceedings of the International Symposium on Hardware/Software Codesign (CODES). 2002, 133鈥?38 CrossRef
  18. Schmitz M T, Al-Hashimi B M, Eles P. Cosynthesis of energy-efficient multimode embedded systems with consideration of mode-execution probabilities. IEEE Transactions on CAD of Integrated Circuits and Systems, 2005, 24(2): 153鈥?69 CrossRef
  19. Harel D. Statecharts: a visual formalism for complex systems. Science of Computer Programming, 1987, 8(3): 231鈥?74 CrossRef
  20. Architecture analysis & design language (AADL). http://http://www.aadl.info/
  21. Liu N, Grundy J, Hosking J. A visual language and environment for composing web services. In: Proceedings of the IEEE/ACM international Conference on Automated Software Engineering (ASE). 2005, 321鈥?24 CrossRef
  22. Luna E R, Rossi G, Garrig贸s I. Webspec: a visual language for specifying interaction and navigation requirements in web applications. Requirements Engineering, 2011, 16(4): 297鈥?21 CrossRef
  23. Cornelissen B, Zaidman A, Deursen V A. A controlled experiment for program comprehension through trace visualization. IEEE Transactions on Software Engineering, 2011, 37: 341鈥?55 CrossRef
  24. Chen M, Qin X, Koo H M, Mishra P. System-level validation: high-level modeling and directed test generation techniques. Springer, 2012
  25. Smith M, Havelund K. Requirements capture with rcat. In: Proceedings of the International Requirements Engineering Conference (RE). 2008, 183鈥?92
  26. Spin model checker. http://spinroot.com/
  27. Alur R, Ivancic F, Kim J, Lee I, Sokolsky O. Generating embedded software from hierarchical hybrid models. ACM SIGPLAN Notice, 2003, 38(7): 171鈥?82 CrossRef
  28. Havelund K. Runtime verification of c programs. In: Proceedings of the International conference on Testing of Software and Communicating Systems (TestCom). 2008, 7鈥?2 CrossRef
  29. Stolz V, Bodden E. Temporal assertions using aspectj. Electronics Notes on Theoretical Computer Science, 2006, 144: 109鈥?24 CrossRef
  30. Henzinger T A, Horowitz B, Kirsch C M. Giotto: a time-triggered language for embedded programming. Technical Report, Department of Electronic Engineering and Computer Science, University of California, Berkeley, 2001
  31. Liu X, Xiong Y, Lee E A. The ptolemy ii framework for visual languages. In: Proceedings of the IEEE Symposia on Human Centric Computing Languages and Environments (HCC). 2001, 50鈥?1
  32. The mathworks: stateflow and stateflow coder, user鈥檚 guide. www.mathworks.com/help/releases/R13sp2/pdf_doc/stateflow/sf_ug.pdf
  33. Hamon G, Rushby J. An operational semantics for stateflow. International Journal on Software Tools for Technology Transfer, 2007, 9: 447鈥?56 CrossRef
  34. Reps T, Horwitz S, Sagiv M. Precise interprocedural dataflow analysis via graph reachability. In: Proceedings of the ACM SIGPLANSIGACT Symposium on Principles of Programming Languages (POPL). 1995, 49鈥?1
  35. Sagiv M, Reps T, Horwitz S. Precise interprocedural dataflow analysis with applications to constant propagation. Theoretical Computer Science, 1996, 167(1鈥?): 131鈥?70 CrossRef
  36. Goodwin D W. Interprocedural dataflow analysis in an executable optimizer. In: Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). 1997, 122鈥?33
  37. Ball T, Rajamani S K. Bebop: a path-sensitive interprocedural dataflow engine. In: Proceedings of ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering (PASTE). 2001, 97鈥?03
  38. Ball T, Levin V, Rajamani S K. A decade of software model checking with slam. Communications of ACM, 2011, 54(7): 68鈥?6 CrossRef
  39. Godefroid P. Compositional dynamic test generation. In: Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL). 2007, 47鈥?4 CrossRef
  
• 作者单位：Zheng Wang (12008) (22008)
  Geguang Pu (12008)
  Jiangwen Li (12008)
  Yuxiang Chen (12008)
  Yongxin Zhao (12008) (32008)
  Mingsong Chen (12008)
  Bin Gu (22008)
  Mengfei Yang (42008)
  Jifeng He (12008)
  
  12008. Shanghai Key Laboratory of Trustworthy Computing, Software Engineering Institute, East China Normal University, Shanghai, 200241, China
  22008. Beijing Institute of Control Engineering, Beijing, 100080, China
  32008. School of Computing, National University of Singapore, Singapore, 119077, Singapore
  42008. China Academy of Space Technology, Beijing, 100094, China
  
• ISSN：1673-7466

文摘

Periodic control systems (PCSs) are widely used in real-time embedded system domain. However, traditional manual requirement analysis assumes the expert knowledge, which is laborious and error-prone. This paper proposes a novel requirement analysis approach, which supports the automated validation of the informal requirement specifications. Based on the normalized initial requirement documents, our approach can construct an intermediate SPARDL model with both formal syntax and semantics. To check the overall system behaviors, our approach can transform the SPARDL models into executable code for simulation. The derived prototype simulator from SPARDL models enables the testing-based system behavior validation. Moreover, our approach enables the analysis of the dataflow relations in SPARDL models. By revealing input/output and affecting relations, our dataflow analysis techniques can help software engineers to figure out the potential data dependencies between SPARDL modules. This is very useful for the module reuse when a new version of the system is developed. A study of our approach using an industry design demonstrates the practicality and effectiveness of our approach.