Please wait a minute...
Shopping Cart Email List Chinese
Advanced Search Fig/Tab
Frontiers of Computer Science

ISSN 2095-2228

ISSN 2095-2236(Online)

CN 10-1014/TP

Postal Subscription Code 80-970

2018 Impact Factor: 1.129

Featured Articles  |  Most Downloaded  |  Most Reading
Online Submission Subscribe to Our RSS Content Feed
Front. Comput. Sci.    2020, Vol. 14 Issue (3) : 143201    https://doi.org/10.1007/s11704-018-7217-7
RESEARCH ARTICLE
TRAP: trace runtime analysis of properties
Daian YUE1,2, Vania JOLOBOFF1,2, Frédéric MALLET1,3()
1. MOE Trustworthy Software International Joint Lab, East China Normal University, Shanghai 200062, China
2. INRIA, Rennes 35042, France
3. Université Cote d’Azur, CNRS, INRIA, I3S, Sophia Antipolis 06900, France
 Download: PDF(798 KB)  
 Export: BibTeX | EndNote | Reference Manager | ProCite | RefWorks
Abstract

We present a method and a tool for the verification of causal and temporal properties for embedded systems. We analyze trace streams resulting from the execution of virtual prototypes that combine simulated hardware and embedded software. The main originality lies in the use of logical clocks to abstract away irrelevant information from the trace. We propose a model-based approach that relies on domain specific languages (DSL). A first DSL, called TISL (trace item specification language), captures the relevant data structures. A second DSL, called STML (simulation trace mapping language), abstracts the simulation raw data into logical clocks, abstracting simulation data into relevant observation probes and thus reducing the trace streams size. The third DSL, called TPSL, defines a set of behavioral patterns that include widely used temporal properties. This is meant for users who are not familiar with temporal logics. Each pattern is transformed into an automata. All the automata are executed concurrently and each one raises an error if and when the related TPSL property is violated. The contribution is the integration of this pattern-based property specification language into the SimSoC virtual prototyping framework without requiring to recompile all the simulation models when the properties evolve. We illustrate our approach with experiments that show the possibility to use multi-core platforms to parallelize the simulation and verification processes, thus reducing the verification time.
Keywords runtime verification      trace analysis      property specification      logical clocks      simulation      virtual prototyping     
Corresponding Author(s): Frédéric MALLET   
Issue Date: 10 January 2020
 Cite this article:   
Daian YUE,Vania JOLOBOFF,Frédéric MALLET. TRAP: trace runtime analysis of properties[J]. Front. Comput. Sci., 2020, 14(3): 143201.
 URL:  
https://academic.hep.com.cn/fcs/EN/10.1007/s11704-018-7217-7
https://academic.hep.com.cn/fcs/EN/Y2020/V14/I3/143201
1 A Dahan, D Geist, L Gluhovsky, D Pidan, G Shapir, Y Wolfsthal, L Benalycherif, R Kamidem, Y Lahbib. Combining system level modeling with assertion based verification. In: Proceedings of the 6th International Symposium on Quality Electronic Design. 2005, 310–315
2 H Foster. Assertion-based verification: industry myths to realities. In: Proceedings of International Conference on Computer Aided Verification. 2008, 5–10
3 D Krahl. Debugging simulation models. In: Proceedings of the Winter Simulation Conference. 2005, 62–68
4 M Leucker, C Schallhart. A brief account of runtime verification. The Journal of Logic and Algebraic Programming, 2009, 78(5): 293–303
5 A Pnueli. The temporal logic of programs. In: Proceedings of the 18th IEEE Symposium on Foundations of Computer Science. 1977, 46–57
6 F Balarin, J Burch, L Lavagno, Y Watanabe, R Passerone, A Sangiovanni-Vincentelli. Constraints specification at higher levels of abstraction. In: Proceedings of IEEE International High Level Design Validation and Test Workshop. 2001, 129–133
7 X Chen, H Hsieh, F Balarin, Y Watanabe. Automatic trace analysis for logic of constraints. In: Proceedings of the 40th Annual Design Automation Conference. 2003, 460–465
8 W Hong, A Viehl, N Bannow, C Kerstan, H Post, O Bringmann, W Rosenstiel. Cult: a unified framework for tracing and logging c-based designs. In: Proceedings of the System, Software, SoC and Silicon Debug Conference. 2012, 1–6
9 D Tabakov, G Kamhi, M Y Vardi, E Singerman. A temporal language for systemc. In: Proceedings of International Conference on Formal Methods in Computer-Aided Design. 2008, 1–9
10 M Khlif, M Shawky, O Tahan. Co-simulation trace analysis (cosita) tool for vehicle electronic architecture diagnosability analysis. In: Proceedings of IEEE Intelligent Vehicles Symposium. 2010, 572–578
11 K Bhargavan, C Gunter, M Kim, I Lee, D Obradovic, O Sokolsky, M Viswanathan. Verisim: formal analysis of network simulations. IEEE Transactions on Software Engineering, 2002, 28(2): 129–145
12 M Kim, M Viswanathan, H Ben-Abdallah, S Kannan, I Lee, O Sokolsky. Formally specified monitoring of temporal properties. In: Proceedings of the 11th Euromicro Conference on Real-Time Systems. 1999, 114–122
13 M B Dwyer, G S Avrunin, J C Corbett. Patterns in property specifications for finite-state verification. In: Proceedings of International Conference on Software Engineering. 1999, 411–420
14 S Konrad, B H Cheng. Real-time specification patterns. In: Proceedings of the 27th International Conference on Software Engineering. 2005, 372–381
15 S Some, R Dssouli, J Vaucher. From scenarios to timed automata: building specifications from users requirements. In: Proceedings of Asia Pacific Software Engineering Conference. 1995, 48–57
16 W T Tsai, L Yu, F Zhu, R Paul. Rapid embedded system testing using verification patterns. IEEE Software, 2005, 22(4): 68–75
17 A M Tokarnia, E P Cruz. Scenario patterns and trace-based temporal verification of reactive embedded systems. In: Proceedings of Euromicro Conference on Digital System Design. 2013, 734–741
18 Á Hegedüs, I Ráth, D Varró. Replaying execution trace models for dynamic modeling languages. Periodica Polytechnica Electrical Engineering and Computer Science, 2012, 56(3): 71
19 D Eschweiler, M Wagner, M Geimer, A Knüpfer, W E Nagel, F Wolf. Open Trace Format 2: the next generation of scalable trace formats and support libraries. In: Proceedings of PARCO. 2011, 481–490
20 A Hamou-Lhadj, T C Lethbridge. A metamodel for the compact but lossless exchange of execution traces. Software & Systems Modeling, 2012, 11(1): 77–98
21 F Mallet, C André, d R Simone. CCSL: specifying clock constraints with UML/Marte. Innovations in Systems and Software Engineering, 2008, 4(3): 309–314
22 L Lamport. Time, clocks, and the ordering of events in a distributed system. Communications of the ACM, 1978, 21(7): 558–565
23 A Benveniste, P Caspi, S A Edwards, N Halbwachs, P Le Guernic, D R Simone. The synchronous languages 12 years later. Proceedings of the IEEE, 2003, 91(1): 64–83
24 R Gascon, F Mallet, J DeAntoni. Logical time and temporal logics: comparing UML MARTE/CCSL and PSL. In: Proceedings of the International Symposium on Temporal Representation and Reasoning. 2011, 141–148
25 C André. Syntax and semantics of the clock constraint specification language (CCSL). Research Report RR-6925, INRIA, 2009
26 J Deantoni, I P Diallo, C Teodorov, J Champeau, B Combemale. Towards a meta-language for the concurrency concern in DSLs. In: Proceedings of 2015 Design, Automation & Test in Europe Conference & Exhibition. 2015, 313–316
27 C André, F Mallet. Specification and verification of time requirements with CCSL and esterel. ACM Sigplan Notices, 2009, 44(7): 167–176
28 H Yu, J Talpin, L Besnard, T Gautier, H Marchand, P L Guernic. Polychronous controller synthesis from MARTE CCSL timing specifications. In: Proceedings of the 9th IEEE/ACM International Conference on Formal Methods and Models for Codesign. 2011, 21–30
29 J DeAntoni, F Mallet. Timesquare: treat your models with logical time. In: Proceedings of the 50th International Conference on Objects, Models, Components, Patterns. 2012, 34–41
30 v G Noord, D Gerdemann. Finite state transducers with predicates and identities. Grammars, 2001, 4(3): 263–286
31 M Veanes, P Hooimeijer, B Livshits, D Molnar, N Bjorner. Symbolic finite state transducers: algorithms and applications. ACM SIGPLAN Notices, 2012, 47(1): 137–150
32 C Helmstetter, V Joloboff. SimSoC: a systemC TLMintegrated ISS for full system simulation. In: Proceedings of IEEE Asia Pacific Confer ence on Circuits and Systems. 2008, 1759–1762
33 V Joloboff, A Gerstlauer. Virtual prototyping of embedded systems: speed and accuracy tradeoffs. In: Nakajima S, Talpin J P, Toyoshima M, Yu H, eds. Cyber Physical System Design from an Architecture Analysis Viewpoint: Communications of NII Shonan Meetings. Springer, Singapore, 2017, 1–31
34 R Drechsler, M Soeken, R Wille. Formal specification level: towards verification-driven design based on natural language processing. In: Proceedings of the 2012 Forum on Specification and Design Languages. 2012, 53–58
35 IEEE. Property Specification Language (PSL), 2010
36 D Steinberg, F Budinsky, E Merks, M Paternostro. EMF: Eclipse Modeling Framework. Pearson Education, 2008
[1] Article highlights Download
[1] Najme MANSOURI, Mohammad Masoud JAVIDI, Behnam Mohammad Hasani ZADE. Hierarchical data replication strategy to improve performance in cloud computing[J]. Front. Comput. Sci., 2021, 15(2): 152501-.
[2] Jianpeng HU, Linpeng HUANG, Tianqi SUN, Ying FAN, Wenqiang HU, Hao ZHONG. Proactive planning of bandwidth resource using simulation-based what-if predictions forWeb services in the cloud[J]. Front. Comput. Sci., 2021, 15(1): 151201-.
[3] Samuel IRVING, Bin LI, Shaoming CHEN, Lu PENG, Weihua ZHANG, Lide DUAN. Computer comparisons in the presence of performance variation[J]. Front. Comput. Sci., 2020, 14(1): 21-41.
[4] Ying JIANG, Shichao LIU, Thomas EHRHARD. A fully abstract semantics for value-passing CCS for trees[J]. Front. Comput. Sci., 2019, 13(4): 828-849.
[5] Jing LIU, Tengfei LI, Zuohua DING, Yuqing QIAN, Haiying SUN, Jifeng HE. AADL+: a simulation-based methodology for cyber-physical systems[J]. Front. Comput. Sci., 2019, 13(3): 516-538.
[6] Jin HUANG, Jiong CHEN, Weiwei XU, Hujun BAO. A survey on fast simulation of elastic objects[J]. Front. Comput. Sci., 2019, 13(3): 443-459.
[7] Juan ZHANG, Fuqing DUAN, Mingquan ZHOU, Dongcan JIANG, Xuesong WANG, Zhongke WU, Youliang HUANG, Guoguang DU, Shaolong LIU, Pengbo ZHOU, Xiangang SHANG. Stable and realistic crack pattern generation using a cracking node method[J]. Front. Comput. Sci., 2018, 12(4): 777-797.
[8] Wenhao ZHOU,Juan CHEN,Chen CUI,Qian WANG,Dezun DONG,Yuhua TANG. Detailed and clock-driven simulation for HPC interconnection network[J]. Front. Comput. Sci., 2016, 10(5): 797-811.
[9] Xi CHANG,Zhuo ZHANG,Peng ZHANG,Jianxin XUE,Jianjun ZHAO. BIFER: a biphasic trace filter approach to scalable prediction of concurrency errors[J]. Front. Comput. Sci., 2015, 9(6): 944-955.
[10] Xiaodong LI,Xiaotie DENG,Shanfeng ZHU,Feng WANG,Haoran XIE. An intelligent market making strategy in algorithmic trading[J]. Front. Comput. Sci., 2014, 8(4): 596-608.
[11] Najme MANSOURI. Network and data location aware approach for simultaneous job scheduling and data replication in large-scale data grid environments[J]. Front. Comput. Sci., 2014, 8(3): 391-408.
[12] Zheng WANG, Geguang PU, Jiangwen LI, Yuxiang CHEN, Yongxin ZHAO, Mingsong CHEN, Bin GU, Mengfei YANG, Jifeng HE. A novel requirement analysis approach for periodic control systems[J]. Front Comput Sci, 2013, 7(2): 214-235.
[13] Wei DUAN, Xiaogang QIU. Fostering artificial societies using social learning and social control in parallel emergency management systems[J]. Front Comput Sci, 2012, 6(5): 604-610.
[14] Yanfang MA, Min ZHANG, Yixiang CHEN, Liang CHEN. Two-thirds simulation indexes and modal logic characterization[J]. Front Comput Sci Chin, 2011, 5(4): 454-471.
[15] Ming C. LIN, Dinesh MANOCHA, . Virtual cityscapes: recent advances in crowd modeling and traffic simulation[J]. Front. Comput. Sci., 2010, 4(3): 405-416.
Viewed
Full text


Abstract

Cited
  Shared   
  Discussed