More Web Proxy on the site http://driver.im/

research-article

Runtime verification for multicore SoC with high-quality trace data

Authors:

Christian Hochberger,

Alexander Weiss,

Martin Leucker,

Richard LasslopAuthors Info & Claims

ACM Transactions on Design Automation of Electronic Systems (TODAES), Volume 18, Issue 2

Article No.: 18, Pages 1 - 26

https://doi.org/10.1145/2442087.2442089

Published: 11 April 2013 Publication History

Abstract

Multicore System-on-Chip (SoC) implementations of embedded systems are becoming very popular. In these systems it is possible to spread out computations over many cores. On one hand this leads to better energy efficiency if clock frequencies and core voltages are reduced. On the other hand this delivers very high performance to the software developer and thus enables complex software systems to be implemented. Unfortunately, debugging and validation of these systems becomes extremely difficult. Various technological approaches try to solve this dilemma. In this contribution we will show a new approach to observe multi-core SoCs and make their internal operations visible to external analysis tools. Also, we show that runtime verification can be employed to analyze and validate these internal operations while the system operates in its normal environment. The combination of these two approaches delivers unprecedented options to the developer to understand and verify system behavior even in complex multicore SoCs.

References

[1]

ARM. 2012. Coresight. http://www.arm.com/products/system-ip/coresight/index.php.

[2]

Barringer, H. and Havelund, K. 2011. TraceContract: A Scala DSL for trace analysis. In Proceedings of the International Symposium on Formal Methods. Lecture Notes in Computer Science, vol. 6664, Springer.

Digital Library

[3]

Bauer, A. and Leucker, M. 2011. The theory and practice of salt. In Proceedings of the International Symposium on Formal Methods. M. G. Bobaru, K. Havelund, G. J. Holzmann, and R. Joshi, Eds., Lecture Notes in Computer Science, vol. 6617, Springer, 13--40.

Digital Library

[4]

Bauer, A., Leucker, M., and Schallhart, C. 2011. Runtime verification for LTL and TLTL. ACM Trans. Softw. Engin. Methodol. 20, 4.

Digital Library

[5]

Bauer, A., Leucker, M., and Streit, J. 2006. SALT—structured assertion language for temporal logic. In Proceedings of the 8th International Conference on Formal Engineering Methods. Lecture Notes in Computer Science, vol. 4260.

Digital Library

[6]

Blackburn, S. M., Garner, R., et al. 2006. The DaCapo benchmarks: Java benchmarking development and analysis. In Proceedings of the 21st annual ACM SIGPLAN Conference on Object-Oriented Programing, Systems, Languages, and Applications (OOPSLA'06). ACM Press, New York, NY, 169--190.

Digital Library

[7]

Broy, M., Jonsson, B., Katoen, J.-P., Leucker, M., and Pretschner, A., Eds. 2005. Model-based Testing of Reactive Systems. Lecture Notes in Computer Science, vol. 3472, Springer.

Digital Library

[8]

Chen, F. and Rosu, G. 2005. Java-mop: A monitoring oriented programming environment for java. In Proceedings of the 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. N. Halbwachs and L. D. Zuck, Eds., Lecture Notes in Computer Science, vol. 3440, Springer, 546--550.

Digital Library

[9]

Chipestimate. 2012. Chipestimate.com chip planning & ip portal. http://www.chipestimate.com.

[10]

Clarke, E. M., Grumberg, O., and Peled, D. A. 1999. Model Checking. The MIT Press, Cambridge, MA.

Digital Library

[11]

Clos, C. 1953. A study of non-blocking switching networks. Bell Syst. Tech. J.

[12]

Dwyer, M. B., Avrunin, G. S., and Corbett, J. C. 1999. Patterns in property specifications for finite-state verification. In Proceedings of the International Conference on Software Engineering. IEEE, 411--420.

Digital Library

[13]

Gaisler. 2012. Leon3 processor. http://www.gaisler.com/cms/index.php&quest;task=view&id=13&Itemid=53.

[14]

Hempel, G. and Hochberger, C. 2007a. A resource optimized processor core for fpga based socs. In Proceedings of the 10th Euromicro Conference on Digital System Design. IEEE, 51--58.

Digital Library

[15]

Hempel, G. and Hochberger, C. 2007b. A resource optimized soc kit for fpgas. In Proceedings of the International Conference on Field Programmable Logic and Applications. K. Bertels, W. A. Najjar, A. J. van Genderen, and S. Vassiliadis, Eds., IEEE, 761--764.

[16]

Hochberger, C. and Weiss, A. 2008a. Acquiring an exhaustive, continuous and real-time trace from socs. In Proceedings of the IEEE International Conference on Computer Design. 356--362.

[17]

Hochberger, C. and Weiss, A. 2008b. A new methodology for debugging and validation of soft cores. In Proceedings of the International Conference on Field Programmable Logic and Applications. 551--554.

[18]

Jin, D., Meredith, P. O., Lee, C., and Ros Ų. G. 2012. Javamop: Efficient parametric runtime monitoring framework. In Proceeding of the 34th International Conference on Software Engineering (ICSE'12). IEEE.

Digital Library

[19]

Leucker, M. and Schallhart, C. 2009. A brief account of runtime verification. J. Logic Algebraic Program. 78, 5, 293--303.

[20]

Leucker, M., Zhao, C., Zheng, B., and Dong, W. 2010. Runtime verification for ltl schemas. In Harnessing Theories for Tool Support in Software, M. Zhang and V. Stolz, Eds., The United Nations University, 76--90.

[21]

LTL3 - Sourceforge.net 2012. Ltl3 tools. http://ltl3tools.sourceforge.net/.

[22]

Stollon, N. 2011. On-Chip Instrumentation: Design and Debug for Systems on Chip. Springer.

Digital Library

[23]

Weiss, A. and Hochberger, C. 2008. A new methodology for the test of SoCs and for analyzing elusive failures. In Proceedings of the 9th International Workshop on Microprocessor Test and Verification. (MTV'08). IEEE Computer Society, 18--23.

Digital Library

Cited By

Benny AChandran SKalayappan RPhawade RKurur P(2024)faRM-LTL: A Domain-Specific Architecture for Flexible and Accelerated Runtime Monitoring of LTL PropertiesRuntime Verification10.1007/978-3-031-74234-7_7(109-127)Online publication date: 14-Oct-2024
https://dl.acm.org/doi/10.1007/978-3-031-74234-7_7
Noami AKumar BPaidimarry CSafi NAlammari A(2021)SoC Verification For The AXI Interconnect Based on The Static Fixed-Priority Scheduling Algorithm2021 Fourth International Conference on Electrical, Computer and Communication Technologies (ICECCT)10.1109/ICECCT52121.2021.9616823(1-6)Online publication date: 15-Sep-2021
https://doi.org/10.1109/ICECCT52121.2021.9616823
Ainsworth SJones TLarus JCeze LStrauss K(2020)The Guardian CouncilProceedings of the Twenty-Fifth International Conference on Architectural Support for Programming Languages and Operating Systems10.1145/3373376.3378463(1277-1293)Online publication date: 9-Mar-2020
https://dl.acm.org/doi/10.1145/3373376.3378463
Show More Cited By

Index Terms

Runtime verification for multicore SoC with high-quality trace data
1. Software and its engineering
  1. Software organization and properties
    1. Software functional properties
      1. Correctness
2. Theory of computation
  1. Logic
    1. Proof theory

Recommendations

A Distributed Hardware Monitoring System for Runtime Verification on Multi-Tile MPSoCs

Exhaustive verification techniques do not scale with the complexity of today’s multi-tile Multi-processor Systems-on-chip (MPSoCs). Hence, runtime verification (RV) has emerged as a complementary method, which verifies the correct behavior of ...
Scalable lossless high definition image coding on multicore platforms
EUC'07: Proceedings of the 2007 international conference on Embedded and ubiquitous computing

With the advent of multicores in all processor segments including mobile, embedded, desktop and server ones, we are in the new era of multiplying computing power via scaling the number of cores. The multicore approach is more versatile and programmable ...
Formally enhanced runtime verification to ensure NoC functional correctness
MICRO-44: Proceedings of the 44th Annual IEEE/ACM International Symposium on Microarchitecture

As silicon technology scales, modern processors and embedded systems are rapidly shifting towards complex chip multi-processor (CMP) and system-on-chip (SoC) designs, comprising several processor cores and IP components communicating via a network-on-...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Transactions on Design Automation of Electronic Systems

ACM Transactions on Design Automation of Electronic Systems Volume 18, Issue 2

March 2013

429 pages

ISSN:1084-4309

EISSN:1557-7309

DOI:10.1145/2442087

Issue’s Table of Contents

Copyright © 2013 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Journal Family

ACM Journals for the Design of Smart and Connected Systems

Publication History

Published: 11 April 2013

Accepted: 01 September 2012

Revised: 01 June 2012

Received: 01 May 2011

Published in TODAES Volume 18, Issue 2

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article
Research
Refereed

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

27
Total Citations
View Citations
610
Total Downloads

Downloads (Last 12 months)19
Downloads (Last 6 weeks)3

Reflects downloads up to 15 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Benny AChandran SKalayappan RPhawade RKurur P(2024)faRM-LTL: A Domain-Specific Architecture for Flexible and Accelerated Runtime Monitoring of LTL PropertiesRuntime Verification10.1007/978-3-031-74234-7_7(109-127)Online publication date: 14-Oct-2024
https://dl.acm.org/doi/10.1007/978-3-031-74234-7_7
Noami AKumar BPaidimarry CSafi NAlammari A(2021)SoC Verification For The AXI Interconnect Based on The Static Fixed-Priority Scheduling Algorithm2021 Fourth International Conference on Electrical, Computer and Communication Technologies (ICECCT)10.1109/ICECCT52121.2021.9616823(1-6)Online publication date: 15-Sep-2021
https://doi.org/10.1109/ICECCT52121.2021.9616823
Ainsworth SJones TLarus JCeze LStrauss K(2020)The Guardian CouncilProceedings of the Twenty-Fifth International Conference on Architectural Support for Programming Languages and Operating Systems10.1145/3373376.3378463(1277-1293)Online publication date: 9-Mar-2020
https://dl.acm.org/doi/10.1145/3373376.3378463
Banerjee MBorges CChoo KLee JNicopoulos C(2020)A Hardware-assisted Heartbeat Mechanism for Fault Identification in Large-scale IoT SystemsIEEE Transactions on Dependable and Secure Computing10.1109/TDSC.2020.3009212(1-1)Online publication date: 2020
https://doi.org/10.1109/TDSC.2020.3009212
Jindal NChandran SPanda PPrasad SMitra ASinghal KGupta STuli S(2019)DHOOMProceedings of the 56th Annual Design Automation Conference 201910.1145/3316781.3317799(1-6)Online publication date: 2-Jun-2019
https://dl.acm.org/doi/10.1145/3316781.3317799
Patil SScholten STao MAl-Asaad H(2019)Survey of Memory, Timing, and Power Management Verification Methods for Multi-core Processors2019 IEEE 10th Annual Information Technology, Electronics and Mobile Communication Conference (IEMCON)10.1109/IEMCON.2019.8936198(0110-0119)Online publication date: Oct-2019
https://doi.org/10.1109/IEMCON.2019.8936198
Zhang YYang MBaghdadi RKamil SShun JAmarasinghe S(2018)GraphIt: a high-performance graph DSLProceedings of the ACM on Programming Languages10.1145/32764912:OOPSLA(1-30)Online publication date: 24-Oct-2018
https://dl.acm.org/doi/10.1145/3276491
Li PZhang D(2018)A derivation framework for dependent security label inferenceProceedings of the ACM on Programming Languages10.1145/32764852:OOPSLA(1-26)Online publication date: 24-Oct-2018
https://dl.acm.org/doi/10.1145/3276485
Muehlboeck FTate R(2018)Empowering union and intersection types with integrated subtypingProceedings of the ACM on Programming Languages10.1145/32764822:OOPSLA(1-29)Online publication date: 24-Oct-2018
https://dl.acm.org/doi/10.1145/3276482
Mendis CAmarasinghe S(2018)goSLP: globally optimized superword level parallelism frameworkProceedings of the ACM on Programming Languages10.1145/32764802:OOPSLA(1-28)Online publication date: 24-Oct-2018
https://dl.acm.org/doi/10.1145/3276480
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Issue’s Table of Contents