TRAP: trace runtime analysis of properties

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

References

[1] Dahan A, Geist D, Gluhovsky L, Pidan D, Shapir G, Wolfsthal Y, Benalycherif L, Kamidem R, Lahbib Y. Combining system level modeling with assertion based verification. In: Proceedings of the 6th International Symposium on Quality Electronic Design. 2005, 310–315

[2] Foster H. Assertion-based verification: industry myths to realities. In: Proceedings of International Conference on Computer Aided Verification. 2008, 5–10

[3] Krahl D. Debugging simulation models. In: Proceedings of the Winter Simulation Conference. 2005, 62–68

[4] Leucker M, Schallhart C. A brief account of runtime verification. The Journal of Logic and Algebraic Programming, 2009, 78(5): 293–303

[5] Pnueli A. The temporal logic of programs. In: Proceedings of the 18th IEEE Symposium on Foundations of Computer Science. 1977, 46–57

[6] Balarin F, Burch J, Lavagno L, Watanabe Y, Passerone R, Sangiovanni-Vincentelli A. Constraints specification at higher levels of abstraction. In: Proceedings of IEEE International High Level Design Validation and Test Workshop. 2001, 129–133

[7] Chen X, Hsieh H, Balarin F, Watanabe Y. Automatic trace analysis for logic of constraints. In: Proceedings of the 40th Annual Design Automation Conference. 2003, 460–465

[8] Hong W, Viehl A, Bannow N, Kerstan C, Post H, Bringmann O, Rosenstiel W. 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] Tabakov D, Kamhi G, Vardi M Y, Singerman E. A temporal language for systemc. In: Proceedings of International Conference on Formal Methods in Computer-Aided Design. 2008, 1–9

[10] Khlif M, Shawky M, Tahan O. Co-simulation trace analysis (cosita) tool for vehicle electronic architecture diagnosability analysis. In: Proceedings of IEEE Intelligent Vehicles Symposium. 2010, 572–578

[11] Bhargavan K, Gunter C, Kim M, Lee I, Obradovic D, Sokolsky O, Viswanathan M. Verisim: formal analysis of network simulations. IEEE Transactions on Software Engineering, 2002, 28(2): 129–145

[12] Kim M, Viswanathan M, Ben-Abdallah H, Kannan S, Lee I, Sokolsky O. Formally specified monitoring of temporal properties. In: Proceedings of the 11th Euromicro Conference on Real-Time Systems. 1999, 114–122

[13] Dwyer M B, Avrunin G S, Corbett J C. Patterns in property specifications for finite-state verification. In: Proceedings of International Conference on Software Engineering. 1999, 411–420

[14] Konrad S, Cheng B H. Real-time specification patterns. In: Proceedings of the 27th International Conference on Software Engineering. 2005, 372–381

[15] Some S, Dssouli R, Vaucher J. From scenarios to timed automata: building specifications from users requirements. In: Proceedings of Asia Pacific Software Engineering Conference. 1995, 48–57

[16] Tsai W T, Yu L, Zhu F, Paul R. Rapid embedded system testing using verification patterns. IEEE Software, 2005, 22(4): 68–75

[17] Tokarnia A M, Cruz E P. 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 Á, Ráth I, Varró D. Replaying execution trace models for dynamic modeling languages. Periodica Polytechnica Electrical Engineering and Computer Science, 2012, 56(3): 71

[19] Eschweiler D, Wagner M, Geimer M, Knüpfer A, Nagel W E, Wolf F. Open Trace Format 2: the next generation of scalable trace formats and support libraries. In: Proceedings of PARCO. 2011, 481–490

[20] Hamou-Lhadj A, Lethbridge T C. A metamodel for the compact but lossless exchange of execution traces. Software & Systems Modeling, 2012, 11(1): 77–98

[21] Mallet F, André C, Simone d R. CCSL: specifying clock constraints with UML/Marte. Innovations in Systems and Software Engineering, 2008, 4(3): 309–314

[22] Lamport L. Time, clocks, and the ordering of events in a distributed system. Communications of the ACM, 1978, 21(7): 558–565

[23] Benveniste A, Caspi P, Edwards S A, Halbwachs N, Le Guernic P, Simone D R. The synchronous languages 12 years later. Proceedings of the IEEE, 2003, 91(1): 64–83

[24] Gascon R, Mallet F, DeAntoni J. 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] André C. Syntax and semantics of the clock constraint specification language (CCSL). Research Report RR-6925, INRIA, 2009

[26] Deantoni J, Diallo I P, Teodorov C, Champeau J, Combemale B. 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] André C, Mallet F. Specification and verification of time requirements with CCSL and esterel. ACM Sigplan Notices, 2009, 44(7): 167–176

[28] Yu H, Talpin J, Besnard L, Gautier T, Marchand H, Guernic P L. 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] DeAntoni J, Mallet F. Timesquare: treat your models with logical time. In: Proceedings of the 50th International Conference on Objects, Models, Components, Patterns. 2012, 34–41

[30] Noord v G, Gerdemann D. Finite state transducers with predicates and identities. Grammars, 2001, 4(3): 263–286

[31] Veanes M, Hooimeijer P, Livshits B, Molnar D, Bjorner N. Symbolic finite state transducers: algorithms and applications. ACM SIGPLAN Notices, 2012, 47(1): 137–150

[32] Helmstetter C, Joloboff V. 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] Joloboff V, Gerstlauer A. 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] Drechsler R, Soeken M, Wille R. 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] Steinberg D, Budinsky F, Merks E, Paternostro M. EMF: Eclipse Modeling Framework. Pearson Education, 2008

RIGHTS & PERMISSIONS

2019 Higher Education Press and Springer-Verlag GmbH Germany, part of Springer Nature