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
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
Erschienen in:
A Trusted Mechanised Specification of JavaScript: One Year On Kapitel lesen Erstes Kapitel lesen

2015 | OriginalPaper | Buchkapitel

Algorithms for Model Checking HyperLTL and HyperCTL\(^*\)

verfasst von : Bernd Finkbeiner, Markus N. Rabe, César Sánchez

Erschienen in: Computer Aided Verification

Verlag: Springer International Publishing

Einloggen

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

search-config
loading …

Abstract

We present an automata-based algorithm for checking finite state systems for hyperproperties specified in HyperLTL and HyperCTL\(^*\). For the alternation-free fragments of HyperLTL and HyperCTL\(^*\) the automaton construction allows us to leverage existing model checking technology. Along several case studies, we demonstrate that the approach enables the verification of real hardware designs for properties that could not be checked before. We study information flow properties of an I2C bus master, the symmetric access to a shared resource in a mutual exclusion protocol, and the functional correctness of encoders and decoders for error resistant codes.

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 On Automation of CTL* Verification for Infinite-State Systems
Nächstes Kapitel Fairness Modulo Theory: A New Approach to LTL Software Model Checking
Fußnoten
1
Our definition of circuits can be considered as a model of and-inverter graphs in the Aiger standard [9], where the gate list is abstracted to a transition relation.
 
2
The tool and the experiments are available online [40].
 
Literatur
1.
Alur, R., Černý, P., Zdancewic, S.: Preserving secrecy under refinement. In: Bugliesi, M., Preneel, B., Sassone, V., Wegener, I. (eds.) ICALP 2006. LNCS, vol. 4052, pp. 107–118. Springer, Heidelberg (2006) CrossRef
2.
Andersen, H.R.: A polyadic modal \(\mu \)-calculus. Technical report (1994)
3.
Askarov, A., Myers, A.: A semantic framework for declassification and endorsement. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol. 6012, pp. 64–84. Springer, Heidelberg (2010) CrossRef
4.
Balliu, M., Dam, M., Le Guernic, G.: Epistemic temporal logic for information flow security. In: Proceedings of PLAS, ACM (2011)
5.
Banerjee, A., Naumann, D.A., Rosenberg, S.: Expressive declassification policies and modular static enforcement. In: Proceedings of S & P, pp. 339–353, IEEE CS Press (2008)
6.
Barthe, G., Crespo, J.M., Kunz, C.: Beyond 2-safety: asymmetric product programs for relational program verification. In: Artemov, S., Nerode, A. (eds.) LFCS 2013. LNCS, vol. 7734, pp. 29–43. Springer, Heidelberg (2013) CrossRef
7.
Barthe, G., D’Argenio, P.R., Rezk, T.: Secure information flow by self-composition. In: Proceedings CSFW, pp. 100–114, June 2004
8.
Biere, A., Clarke, E., Raimi, R., Zhu, Y.: Verifying safety properties of a PowerPC\(^{\rm TM}\) microprocessor using symbolic model checking without BDDs. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 60–71. Springer, Heidelberg (1999) CrossRef
9.
10.
Bradley, A.R.: SAT-based model checking without unrolling. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 70–87. Springer, Heidelberg (2011) CrossRef
11.
Brayton, R., Mishchenko, A.: ABC: an academic industrial-strength verification tool. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 24–40. Springer, Heidelberg (2010) CrossRef
12.
Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L.: Sequential circuit verification using symbolic model checking. In: Proceedings of DAC 1990, pp. 46–51, IEEE CS Press (1990)
13.
Claessen, K., Eén, N., Sterin, B.: A circuit approach to LTL model checking. In: Proceedings of FMCAD, pp. 53–60 (2013)
14.
Clarkson, M.R., Finkbeiner, B., Koleini, M., Micinski, K.K., Rabe, M.N., Sánchez, C.: Temporal logics for hyperproperties. In: Abadi, M., Kremer, S. (eds.) POST 2014 (ETAPS 2014). LNCS, vol. 8414, pp. 265–284. Springer, Heidelberg (2014) CrossRef
15.
Clarkson, M.R., Schneider, F.B.: Hyperproperties.In: Proceedings IEEE Symposium on Computer Security Foundations, pp. 51–65, June 2008
16.
Dimitrova, R., Finkbeiner, B., Kovács, M., Rabe, M.N., Seidl, H.: Model checking information flow in reactive systems. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol. 7148, pp. 169–185. Springer, Heidelberg (2012) CrossRef
17.
D’Souza, D., Holla, R., Raghavendra, K.R., Sprick, B.: Model-checking trace-based information flow properties. J. Comput. Secur. 19(1), 101–138 (2011)
18.
Eén, N., Mishchenko, A., Brayton, R.K.: Efficient implementation of property directed reachability. In: Proceedings of FMCAD, pp. 125–134 (2011)
19.
Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.Y.: Reasoning About Knowledge. MIT Press, Cambridge (1995)
20.
Finkbeiner, B., Rabe, M.N.: The linear-hyper-branching spectrum of temporal logics. IT Inf. Technol. 56, 273–279 (2014)
21.
Gammie, P., van der Meyden, R.: MCK: model checking the logic of knowledge. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 479–483. Springer, Heidelberg (2004) CrossRef
22.
Goguen, J.A., Meseguer, J.: Security policies and security models. In: Proceedings IEEE Symposium on Security and Privacy, pp. 11–20, IEEE CS Press (1982)
23.
Huisman, M., Worah, P., Sunesen, K.: A temporal logic characterisation of observational determinism. In: Proceedings of CSFW, IEEE CS Press (2006)
24.
Kesten, Y., Pnueli, A., Raviv, L.: Algorithmic verification of linear temporal logic specifications. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol. 1443, pp. 1–16. Springer, Heidelberg (1998) CrossRef
25.
26.
Lamport, L.: A new solution of Dijkstra’s concurrent programming problem. Commun. ACM 17(8), 453–455 (1974)MathSciNetCrossRef
27.
Lange, M., Lozes, É.: Model-checking the higher-dimensional modal mu-calculus. In: Proceedings of FICS, EPTCS, vol. 77, pp. 39–46 (2012)
28.
Lomuscio, A., Pecheur, C., Raimondi, F.: Automatic verification of knowledge and time with NuSMV. In: Proceedings of IJCAI, pp. 1384–1389 (2007)
29.
Lomuscio, A., Qu, H., Raimondi, F.: MCMAS: a model checker for the verification of multi-agent systems. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 682–688. Springer, Heidelberg (2009) CrossRef
30.
Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems. Springer, New York (1992) CrossRef
31.
Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems: Safety. Springer, New York (1995)CrossRef
32.
McMillan, K.L.: Craig interpolation and reachability analysis. In: Cousot, R. (ed.) SAS 2003. LNCS, vol. 2694, p. 336. Springer, Heidelberg (2003) CrossRef
33.
Meski, A., Penczek, W., Szreter, M., Wozna-Szczesniak, B., Zbrzezny, A.: Bounded model checking for knowledge and linear time. In: Proceedings of AAMAS, pp. 1447–1448, IFAAMAS (2012)
34.
Milushev, D.: Reasoning about hyperproperties. Ph.D thesis, Faculty of Engineering, Katholieke Universiteit Leuven, Celestijnenlaan 200A, box 2402, B3001 Heverlee, Belgium, 6 (2013)
35.
Milushev, D., Clarke, D.: Towards incrementalization of holistic hyperproperties. In: Degano, P., Guttman, J.D. (eds.) Principles of Security and Trust. LNCS, vol. 7215, pp. 329–348. Springer, Heidelberg (2012) CrossRef
36.
Miyano, S., Hayashi, T.: Alternating finite automata on omega-words. Theor. Comput. Sci. 32, 321–330 (1984)MathSciNetCrossRef
37.
Muller, D.E., Saoudi, A., Schupp, P.E.: Weak alternating automata give a simple explanation of why most temporal and dynamic logics are decidable in exponential time. In: Proceedings of LICS, pp. 422–427, IEEE CS Press (1988)
38.
Otto, M.: Bisimulation-invariant PTIME and higher-dimensional \(\mu \)-calculus. Theor. Comput. Sci. 224, 237–265 (1998)CrossRef
39.
Pencze, W., Lomuscio, A.: Verifying epistemic properties of multi-agent systems via bounded model checking. In: Proceedings of AAMAS, pp. 209–216, IFAAMAS (2003)
40.
41.
Sabelfeld, A., Myers, A.C.: A model for delimited information release. In: Futatsugi, K., Mizoguchi, F., Yonezaki, N. (eds.) ISSS 2003. LNCS, vol. 3233, pp. 174–191. Springer, Heidelberg (2004) CrossRef
42.
Sistla, P.A., Clarke, E.M.: The complexity of propositional linear temporal logics. J. ACM 32(3), 733–749 (1985)MathSciNetCrossRef
43.
44.
van der Meyden, R., Zhang, C.: Algorithmic verification of noninterference properties. Electr. Notes Theor. Comput. Sci. 168, 61–75 (2007)CrossRef
45.
Vardi, M.Y.: Alternating automata and program verification. In: van Leeuwen, J. (ed.) Computer Science Today. LNCS, vol. 1000, pp. 471–485. Springer, Heidelberg (1995)CrossRef
46.
Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: Proceedings of LICS 1986, pp. 332–344, IEEE CS Press (1986)
47.
Metadaten
Titel
Algorithms for Model Checking HyperLTL and HyperCTL
verfasst von
Bernd Finkbeiner
Markus N. Rabe
César Sánchez
Copyright-Jahr
2015
Buch
Computer Aided Verification

Print ISBN: 978-3-319-21689-8

Electronic ISBN: 978-3-319-21690-4

Copyright-Jahr: 2015

DOI
https://doi.org/10.1007/978-3-319-21690-4_3

Premium Partner

    Bildnachweise