|
|
A novel requirement analysis approach for periodic control systems |
Zheng WANG1,2, Geguang PU1( ), Jiangwen LI1, Yuxiang CHEN1, Yongxin ZHAO1,3, Mingsong CHEN1, Bin GU2, Mengfei YANG4, Jifeng HE1 |
1. Shanghai Key Laboratory of Trustworthy Computing, Software Engineering Institute, East China Normal University, Shanghai 200241, China; 2. Beijing Institute of Control Engineering, Beijing 100080, China; 3. School of Computing, National University of Singapore, Singapore 119077, Singapore; 4. China Academy of Space Technology, Beijing 100094, China |
|
|
Abstract 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.
|
Keywords
SPARDL
simulation
dataflow analysis
code generation
|
Corresponding Author(s):
PU Geguang,Email:ggpu@sei.ecnu.edu.cn
|
Issue Date: 01 April 2013
|
|
1 |
Alur R, Dill D L. A theory of timed automata. Theoretical Computer Science , 1994, 126: 183-235 doi: 10.1016/0304-3975(94)90010-8
|
2 |
Ouaknine J, Schneider S. Timed csp: a retrospective. Electronics Notes in Theoretical Computer Science , 2006, 162: 273-276 doi: 10.1016/j.entcs.2005.12.093
|
3 |
Baresi L, Pezzè M. An introduction to software testing. Electronics Notes in Theoretical Computer Science , 2006, 148(1): 89-111 doi: 10.1016/j.entcs.2005.12.014
|
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-274
|
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-400
|
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-130 doi: 10.1007/s10617-010-9052-4
|
7 |
Chen M, Mishra P. Property learning techniques for efficient generation of directed tests. IEEE Trans. Computers , 2011, 60(6): 852-864 doi: 10.1109/TC.2011.49
|
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-162
|
9 |
Plotkin G D. A structural approach to operational semantics. Journal of Logic and Algebra Programming , 2004, 60-61 : 17-139
|
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-608
|
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-48
|
12 |
Nielson F, Nielson H R, Hankin C. Principles of program analysis. Secaucus, NJ, USA: Springer-Verlag New York, Inc., 1999 doi: 10.1007/978-3-662-03811-6
|
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-56 doi: 10.1007/978-3-540-39815-8_3
|
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-13
|
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-25 doi: 10.1109/IWSSD.1996.501143
|
16 |
Jahanian F, Mok A K. Modechart: a specification language for realtime systems. IEEE Transactions on Software Engineering , 1994, 20: 933-947 doi: 10.1109/32.368134
|
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-138 doi: 10.1145/774789.774817
|
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-169 doi: 10.1109/TCAD.2004.837729
|
19 |
Harel D. Statecharts: a visual formalism for complex systems. Science of Computer Programming , 1987, 8(3): 231-274 doi: 10.1016/0167-6423(87)90035-9
|
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-324
|
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-321 doi: 10.1007/s00766-011-0124-1
|
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-355 doi: 10.1109/TSE.2010.47
|
24 |
Chen M, Qin X, Koo H M, Mishra P. System-level validation: highlevel 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-192
|
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-182 doi: 10.1145/780731.780756
|
28 |
Havelund K. Runtime verification of c programs. In: Proceedings of the International conference on Testing of Software and Communicating Systems (TestCom) . 2008, 7-22
|
29 |
Stolz V, Bodden E. Temporal assertions using aspectj. Electronics Notes on Theoretical Computer Science , 2006, 144: 109-124 doi: 10.1016/j.entcs.2006.02.007
|
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-51
|
32 |
The mathworks: stateflow and stateflow coder, user’s 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-456 doi: 10.1007/s10009-007-0049-7
|
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-61
|
35 |
Sagiv M, Reps T, Horwitz S. Precise interprocedural dataflow analysis with applications to constant propagation. Theoretical Computer Science , 1996, 167(1-2): 131-170 doi: 10.1016/0304-3975(96)00072-2
|
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-133
|
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-103
|
38 |
Ball T, Levin V, Rajamani S K. A decade of software model checking with slam. Communications of ACM , 2011, 54(7): 68-76 doi: 10.1145/1965724.1965743
|
39 |
Godefroid P. Compositional dynamic test generation. In: Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL) . 2007, 47-54 doi: 10.1145/1190216.1190226
|
|
Viewed |
|
|
|
Full text
|
|
|
|
|
Abstract
|
|
|
|
|
Cited |
|
|
|
|
|
Shared |
|
|
|
|
|
Discussed |
|
|
|
|