nach oben

Erschienen in:

2020 | OriginalPaper | Buchkapitel

Towards Formal Co-validation of Hardware and Software Timing Models of CPSs

verfasst von : Mihail Asavoae, Imane Haur, Mathieu Jan, Belgacem Ben Hedia, Martin Schoeberl

Erschienen in: Cyber Physical Systems. Model-Based Design

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

Timing analysis of safety-critical systems derives timing bounds of applications, or software (SW), executed on dedicated platforms, or hardware (HW). The ensemble HW–SW features, from a timing perspective, two different types of computation – a SW-specific, instruction-driven timing progression and a HW-specific, cycle-driven one. The two timings are unified under a concept of timing model, which is crucial to establish a sound and precise worst-case timing reasoning. In this paper, we propose an investigation on how to systematically derive and formally prove such timing models. Our approach is exemplified on a simple, accumulator-based processor called Lipsi.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel Guaranteed Optimal Reachability Control of Reaction-Diffusion Equations Using One-Sided Lipschitz Constants and Model Reduction

Nächstes Kapitel A Remote Test Environment for a Large-Scale Microcontroller Laboratory Course

Armstrong, A., et al.: ISA semantics for ARMv8-a, RISC-V, and CHERI-MIPS. PACMPL 3(POPL), 71:1–71:31 (2019)CrossRef

Asavoae, M.: K semantics for assembly languages: a case study. Electr. Notes Theor. Comput. Sci. 304, 111–125 (2014)MathSciNetCrossRef

Asavoae, M., Hedia, B.B., Jan, M.: Formal executable models for automatic detection of timing anomalies. In: 18th International Workshop on Worst-Case Execution Time Analysis, WCET 2018, pp. 2:1–2:13 (2018)

Bachrach, J., et al.: Chisel: constructing hardware in a Scala embedded language. In: Proceedings of the 49th Annual Design Automation Conference, DAC 2012, pp. 1216–1225. ACM (2012)

Beatty, D.L., Bryant, R.E.: Formally verifying a microprocessor using a simulation methodology. In: Proceedings of the 31st Conference on Design Automation, pp. 596–602 (1994)

Béchennec, J., Cassez, F.: Computation of WCET using program slicing and real-time model-checking. CoRR abs/1105.1633 (2011). http://arxiv.org/abs/1105.1633

Benveniste, A., Caspi, P., Edwards, S.A., Halbwachs, N., Guernic, P.L., de Simone, R.: The synchronous languages 12 years later. Proc. IEEE 91(1), 64–83 (2003)CrossRef

Bradlee, D.G., Henry, R.R., Eggers, S.J.: The Marion system for retargetable instruction scheduling. SIGPLAN Not. 26(6), 229–240 (1991)CrossRef

Dalsgaard, A.E., Olesen, M.C., Toft, M., Hansen, R.R., Larsen, K.G.: METAMOC: modular execution time analysis using model checking. In: Lisper, B. (ed.) 10th International Workshop on Worst-Case Execution Time Analysis (WCET 2010). OpenAccess Series in Informatics (OASIcs), vol. 15, pp. 113–123 (2010)

10.

Dasgupta, S., Park, D., Kasampalis, T., Adve, V.S., Rosu, G.: A complete formal semantics of x86–64 user-level instruction set architecture. In: Proceedings of the 40th PLDI 2019, pp. 1133–1148 (2019)

11.

Gordon, M.J.C.: The semantic challenge of Verilog HDL. In: Proceedings of the 10th Annual IEEE Symposium on Logic in Computer Science, San Diego, 26–29, pp. 136–145 (1995)

12.

Große, D., Kühne, U., Drechsler, R.: HW/SW co-verification of embedded systems using bounded model checking. In: Proceedings of the 16th ACM Great Lakes Symposium on VLSI 2006, pp. 43–48 (2006)

13.

Hahn, S., Reineke, J., Wilhelm, R.: Towards compositionality in execution time analysis: definition and challenges. SIGBED Rev. 12(1), 28–36 (2015)CrossRef

14.

Hebbache, F., Jan, M., Brandner, F., Pautet, L.: Shedding the shackles of time-division multiplexing. In: 2018 IEEE Real-Time Systems Symposium, RTSS, 2018, pp. 456–468 (2018)

15.

Herbegue, H., Filali, M., Cassé, H.: Formal architecture specification for time analysis. In: Maehle, E., Römer, K., Karl, W., Tovar, E. (eds.) ARCS 2014. LNCS, vol. 8350, pp. 98–110. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-04891-8_9CrossRef

16.

Hoover, S.F.: Timing-abstract circuit design in transaction-level Verilog. In: 2017 IEEE International Conference on Computer Design (ICCD), pp. 525–532, November 2017

17.

Huang, B., Zhang, H., Subramanyan, P., Vizel, Y., Gupta, A., Malik, S.: Instruction-level abstraction (ILA): a uniform specification for system-on-chip (SOC) verification. ACM Trans. Design Autom. Electr. Syst. 24(1), 10:1–10:24 (2019)

18.

Kern, C., Greenstreet, M.: Formal verification in hardware design: a survey. ACM Trans. Des. Autom. Electron. Syst. 4 (2002). https://doi.org/10.1145/307988.307989CrossRef

19.

Kurshan, R.P., Levin, V., Minea, M., Peled, D.A., Yenigün, H.: Combining software and hardware verification techniques. Formal Methods Syst. Des. 21(3), 251–280 (2002)CrossRef

20.

Lamport, L.: Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley Longman Publishing Co., Inc., Boston (2002)

21.

Leupers, R., Marwedel, P.: A BDD-based frontend for retargetable compilers. In: Proceedings the European Design and Test Conference, ED TC 1995, pp. 239–243, March 1995

22.

Li, H., Puaut, I., Rohou, E.: Tracing flow information for tighter WCET estimation: application to vectorization. In: 21st IEEE International Conference on Embedded and Real-Time Computing Systems and Applications, RTCSA 2015, Hong Kong, China, 19–21 August 2015, pp. 217–226 (2015)

23.

Li, J., Xie, F., Ball, T., Levin, V., McGarvey, C.: An automata-theoretic approach to hardware/software co-verification. In: Rosenblum, D.S., Taentzer, G. (eds.) FASE 2010. LNCS, vol. 6013, pp. 248–262. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-12029-9_18CrossRef

24.

Li, X., Roychoudhury, A., Mitra, T., Mishra, P., Cheng, X.: A retargetable software timing analyzer using architecture description language. In: 2007 Asia and South Pacific Design Automation Conference, pp. 396–401, January 2007

25.

Li, X., Roychoudhury, A., Mitra, T.: Modeling out-of-order processors for WCET analysis. Real-Time Syst. 34(3), 195–227 (2006)CrossRef

26.

Liu, I., et al.: A PRET microarchitecture implementation with repeatable timing and competitive performance. In: 2012 IEEE 30th International Conference on Computer Design (ICCD), pp. 87–93. IEEE (2012)

27.

Meredith, P.O., Katelman, M., Meseguer, J., Rosu, G.: A formal executable semantics of Verilog. In: 8th ACM/IEEE MEMOCODE 2010, Grenoble, France, pp. 179–188 (2010)

28.

Mishra, P., Dutt, N. (eds.): Processor Description Languages, Application and Methodologies. Systems on Silicon, vol. 1. Morgan Kaufman, Burlington (2008)

29.

Monniaux, D.: Verification of device drivers and intelligent controllers: a case study. In: Proceedings of the 7th ACM & IEEE International Conference on Embedded software, EMSOFT 2007, pp. 30–36 (2007)

30.

Mukherjee, R., Purandare, M., Polig, R., Kroening, D.: Formal techniques for effective co-verification of hardware/software co-designs. In: Proceedings of the 54th Annual Design Automation Conference, DAC 2017, pp. 35:1–35:6 (2017)

31.

Pees, S., Hoffmann, A., Zivojnovic, V., Meyr, H.: Lisa-machine description language for cycle-accurate models of programmable DSP architectures. In: Proceedings 1999 Design Automation Conference (Cat. No. 99CH36361), pp. 933–938, June 1999

32.

Pister, M.: Timing model derivation: pipeline analyzer generation from hardware description languages. Ph.D. thesis, Saarland University (2012)

33.

Rau, B.R., Kathail, V., Aditya, S.: Machine-description driven compilers for EPIC and VLIW processors. Des. Autom. Embed. Syst. 4(2), 71–118 (1999)CrossRef

34.

Raymond, P., Maiza, C., Parent-Vigouroux, C., Carrier, F., Asavoae, M.: Timing analysis enhancement for synchronous program. Real-Time Syst. 51(2), 192–220 (2015)CrossRef

35.

Reineke, J., et al.: A definition and classification of timing anomalies. In: 6th International Workshop on Worst-Case Execution Time (WCET) Analysis (2006)

36.

Schlickling, M.: Timing model derivation: static analysis of hardware description languages. Ph.D. thesis, Saarland University (2013)

37.

Schoeberl, M.: Lipsi: probably the smallest processor in the world. In: Berekovic, M., Buchty, R., Hamann, H., Koch, D., Pionteck, T. (eds.) ARCS 2018. LNCS, vol. 10793, pp. 18–30. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-77610-1_2CrossRef

38.

Schoeberl, M., Puffitsch, W., Hepp, S., Huber, B., Prokesch, D.: Patmos: a time-predictable microprocessor. Real-Time Syst. 54(2), 389–423 (2018). https://doi.org/10.1007/s11241-018-9300-4CrossRefMATH

39.

Thiele, L., Wilhelm, R.: Design for timing predictability. Real-Time Syst. 28(2–3), 157–177 (2004)CrossRef

40.

Wilhelm, R.: Formal analysis of processor timing models. In: Graf, S., Mounier, L. (eds.) SPIN 2004. LNCS, vol. 2989, pp. 1–4. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-24732-6_1CrossRef

41.

Wilhelm, R., et al.: The worst-case execution-time problem - overview of methods and survey of tools. ACM Trans. Embedded Comput. Syst. 7(3), 36:1–36:53 (2008)CrossRef

42.

Wilson, S.: Verilator 4.0 - open simulation goes multithreaded. In: The Open Source Digital Design Conference (ORConf), September 2018

43.

Yu, Y., Manolios, P., Lamport, L.: Model checking TLA\(^{+}\) specifications. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol. 1703, pp. 54–66. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-48153-2_6CrossRef

Titel: Towards Formal Co-validation of Hardware and Software Timing Models of CPSs
verfasst von: Mihail Asavoae
Imane Haur
Mathieu Jan
Belgacem Ben Hedia
Martin Schoeberl
Verlag: Springer International Publishing
Buch: Cyber Physical Systems. Model-Based Design
Print ISBN: 978-3-030-41130-5

Electronic ISBN: 978-3-030-41131-2

Copyright-Jahr: 2020
DOI: https://doi.org/10.1007/978-3-030-41131-2_10

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner