Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Bücher
Zeitschriften
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
ATZ-Fachkongress

Chassis.tech plus 2024


4 Kongresse in einer Veranstaltung

Treffen Sie in München die Fachleute von Chassis, Lenkung, Bremsen sowie Reifen/Räder.
Erweiterte Suche
Anmelden
nach oben
Formal Methods in System Design
Erschienen in: Formal Methods in System Design 3/2012

01.12.2012

Optimized temporal monitors for SystemC

verfasst von: Deian Tabakov, Kristin Y. Rozier, Moshe Y. Vardi

Erschienen in: Formal Methods in System Design | Ausgabe 3/2012

Einloggen

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

search-config
loading …

Abstract

SystemC is a modeling language built as an extension of C++. Its growing popularity and the increasing complexity of designs have motivated research efforts aimed at the verification of SystemC models using assertion-based verification (ABV), where the designer asserts properties that capture the design intent in a formal language such as PSL or SVA. The model then can be verified against the properties using runtime or formal verification techniques. In this paper we focus on automated generation of runtime monitors from temporal properties. Our focus is on minimizing runtime overhead, rather than monitor size or monitor-generation time. We identify four issues in monitor generation: state minimization, alphabet representation, alphabet minimization, and monitor encoding. We conduct extensive experimentation and identify a combination of settings that offers the best performance in terms of runtime overhead.
Vorheriger Artikel Introduction to the special issue on runtime verification
Nächster Artikel Safer asynchronous runtime monitoring using compensations

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 "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

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
Fußnoten
1
IEEE Standard 1666–2005.
 
2
Property Specification Language, IEEE Standard 1850–2007.
 
3
SystemVerilog Assertions, IEEE Standard 1800–2005.
 
4
Note that the comparison is between different monitor implementations and is applicable to other C or C++ modeling languages.
 
5
BRICS Automaton represents the alphabet of the automaton as Unicode characters, which have one-to-one correspondence to the set of 16-bit integers.
 
Literatur
1.
Abarbanel Y, Beer I, Gluhovsky L, Keidar S, Wolfsthal Y (2000) Focs: Automatic generation of simulation checkers from formal specifications. In: CAV’00: Proc of the 12th international conference on computer aided verification, pp 538–542 CrossRef
2.
Armoni R, Korchemny D, Tiemeyer A, Vardi M, Zbar Y (2006) Deterministic dynamic monitors for linear-time assertions. In: Proc workshop on formal approaches to testing and runtime verification. LNCS, vol 4262. Springer, Berlin
3.
Bauer A, Leucker M, Schallhart C (2006) Monitoring of real-time properties. In: FSTTCS’06: Foundations of software technology and theoretical computer science, 26th international conference. LNCS, vol 4337. Springer, Berlin, pp 260–272 CrossRef
4.
Bodden E, Hendren LJ, Lam P, Lhoták O, Naeem NA (2010) Collaborative runtime verification with tracematches. J Log Comput 20(3):707–723 MATHCrossRef
5.
Boulé M, Zilic Z (2008) Generating hardware assertion checkers. Springer, Berlin CrossRef
6.
Bryant R (1986) Graph-based algorithms for Boolean-function manipulation. IEEE Trans Comput C-35(8)
7.
Bryant R (1992) Symbolic Boolean manipulation with ordered binary-decision diagrams. ACM Comput Surv 24(3):293–318 CrossRef
8.
Bunker A, Gopalakrishnan G, McKee SA (2004) Formal hardware specification languages for protocol compliance verification. ACM Trans Des Autom Electron Syst 9(1):1–32 CrossRef
9.
Bustan D, Fisman D, Havlicek J (2005) Automata construction for PSL. Tech Rep, The Weizmann Institute of Science
10.
Chang H, Cooke L, Hunt M, Martin G, McNelly AJ, Todd L (1999) Surviving the SOC revolution: a guide to platform-based design. Kluwer Academic, Norwell
11.
Chen F, Jin D, Meredith P, Roşu G (2009) Monitoring oriented programming—a project overview. In: Proceedings of the fourth international conference on intelligent computing and information systems (ICICIS’09). ACM, New York, pp 72–77
12.
Cooper KD, Torczon L (2004) Engineering a compiler. Morgan Kaufmann, San Mateo
13.
Courcoubetis C, Vardi M, Wolper P, Yannakakis M (1992) Memory efficient algorithms for the verification of temporal properties. Form Methods Syst Des 1:275–288 CrossRef
14.
d’Amorim M, Rosu G (2005) Efficient monitoring of ω-languages. In: Proc 17th international conference on computer aided verification, pp 364–378 CrossRef
15.
Daniele M, Giunchiglia F, Vardi MY (1999) Improved automata generation for linear temporal logic. In: CAV’99: Proc 11th int conf on computer aided verification. Springer, London, pp 249–260 CrossRef
16.
17.
Eisner C, Fisman D (2006) A practical introduction to PSL. Springer, New York
18.
19.
Geilen M (2001) On the construction of monitors for temporal logic properties. Electr Notes Theor Comput Sci 55(2)
20.
Geist D, Biran G, Arons T, Slavkin M, Nustov Y, Farkas M, Holtz K, Long A, King D, Barret S (1999) A methodology for the verification of a “system on chip”. In: DAC’99: Proc 36th design automation conference. ACM, New York, pp 574–579. doi:10.​1145/​309847.​310001
21.
Geldenhuys J, Hansen H (2006) Larger automata and less work for LTL model checking. In: Model checking software, 13th int SPIN workshop. LNCS, vol 3925. Springer, Berlin, pp 53–70
22.
Gerth R, Peled D, Vardi M, Wolper P (1995) Simple on-the-fly automatic verification of Linear Temporal Logic. In: Dembiski P, Sredniawa M (eds) Protocol specification, testing, and verification. Chapman & Hall, London, pp 3–18
23.
Giannakopoulou D, Havelund K (2001) Automata-based verification of temporal properties on running programs. In: Int conf on automated software engineering. IEEE, Washington, p 412
24.
Grotker T, Liao S, Martin G, Swan S (2002) System design with SystemC. Kluwer Academic, Norwell
25.
26.
27.
Hoos HH (2008) Computer-aided design of high-performance algorithms. Tech rep, University of British Columbia
28.
Hopcroft J, Ullman J (1979) Introduction to automata theory, languages, and computation. Addison-Wesley, Reading MATH
29.
Jard C, Jeron T (1989) On-line model-checking for finite linear temporal logic specifications. In: Automatic verification methods for finite state systems, Proc international workshop, Grenoble. LNCS, vol 407. Springer, Grenoble, pp 189–196 CrossRef
30.
Jin D, Meredith P, Griffith D, Roşu G (2011) Garbage collection for monitoring parametric properties. In: Programming language design and implementation (PLDI’11). ACM, New York, pp 415–424. doi:10.​1145/​1993316.​1993547
31.
Kupferman O, Lampert R (2006) On the construction of fine automata for safety properties. In: ATVA’06: Proc of the international symposium on automated technology for verification and analysis, pp 110–124 CrossRef
32.
33.
34.
35.
Morin-Allory K, Borrione D (2006) Proven correct monitors from PSL specifications. In: DATE’06: Proc conf on design, automation and test in Europe, European Design and Automation Association, pp 1246–1251
36.
de Moura LM, Bjørner N (2008) Z3: An efficient SMT solver. In: TACAS’08: Tools and algorithms for the construction and analysis of systems, 14th international conference, pp 337–340 CrossRef
37.
38.
39.
Rozier KY, Vardi MY (2007) LTL satisfiability checking. In: Proc 14th int SPIN conference on model checking software. Springer, Berlin, pp 149–167
40.
41.
Tabakov D, Vardi M (2010) Monitoring temporal SystemC properties. In: Proc 8th int’l conf on formal methods and models for codesign. IEEE, New York, pp 123–132
42.
43.
Tabakov D, Vardi MY (2005) Experimental evaluation of classical automata constructions. In: LPAR’05: 12th int conf on logic for programming, artificial intelligence, and reasoning, pp 396–411 CrossRef
44.
45.
Vijayaraghavan S, Ramanathan M (2005) A practical guide for SystemVerilog assertions. Springer, New York
Metadaten
Titel
Optimized temporal monitors for SystemC
verfasst von
Deian Tabakov
Kristin Y. Rozier
Moshe Y. Vardi
Publikationsdatum
01.12.2012
Verlag
Springer US
Erschienen in
Formal Methods in System Design / Ausgabe 3/2012
Print ISSN: 0925-9856
Elektronische ISSN: 1572-8102
DOI
https://doi.org/10.1007/s10703-011-0139-8

Weitere Artikel der Ausgabe 3/2012

Formal Methods in System Design 3/2012 Zur Ausgabe

OriginalPaper

Efficient data race detection for async-finish parallelism

OriginalPaper

Safer asynchronous runtime monitoring using compensations

EditorialNotes

Introduction to the special issue on runtime verification

OriginalPaper

InterAspect: aspect-oriented instrumentation with GCC

Premium Partner

    Bildnachweise