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
MTZ-Fachkongress

Antriebe und Energiesysteme von morgen


Austausch von Automobil- und Energiewirtschaft

Am 14./15. Mai geht es in Chemnitz um die Mobilitätswende durch Elektro- und Wasserstofffahrzeuge.
Erweiterte Suche
Anmelden
nach oben
Journal of Combinatorial Optimization
Erschienen in: Journal of Combinatorial Optimization 2/2016

01.02.2016

Verifying safety critical task scheduling systems in PPTL axiom system

verfasst von: Nan Zhang, Mengfei Yang, Bin Gu, Zhenhua Duan, Cong Tian

Erschienen in: Journal of Combinatorial Optimization | Ausgabe 2/2016

Einloggen

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

search-config
loading …

Abstract

This paper presents a case study of formal verification of safety critical task scheduling systems. First, a scheduling algorithm described in a temporal logic programming language is presented; then a sufficient and necessary condition for the schedulability of task set is formalized. Further, the correctness of the condition is proved by means of theorem proving in the axiom system of Propositional Projection Temporal Logic.
Vorheriger Artikel Modified differential evolution with self-adaptive parameters method
Nächster Artikel -labeling number of Cartesian product of path and cycle

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
Anhänge
Nur mit Berechtigung zugänglich
Literatur
Bertot Y, Castéran P (2004) Interactive theorem proving and program development. Springer-Verlag, Berlin, Heidelberg
Brock B, Kaufmann M, Moore J (1996) Acl2 theorems about commercial microprocessors. In: Srivas M, Camilleri A (eds) Proceedings of the 1st international conference on formal methods in computer-aided design. Springer-Verlag, London, pp 275–293
Duan Z (2005) Temporal logic and temporal logic programming. Science Press, Beijing
Duan Z, Zhang N, Koutny M (2013) A complete proof system for propositional projection temporal logic. Theoret Comput Sci 497:84–107MathSciNetCrossRefMATH
Gordon M, Melham T (1993) Introduction to HOL: a theorem proving environment for higher order logic. Cambridge University Press, Cambridge
McMillan K (1993) Symbolic model checking: an approach to the state explosion problem. Kluwer Academic, DordrechtCrossRef
Owre S, Rushby J (1992) Pvs: a prototype verification system. In: Kapur D (ed) Proceedings of the 11th international conference on automated deduction. Springer-Verlag, Heidelberg, pp 748–752
Paulson L (1994) Isabelle—a generic theorem prover. Springer, BerlinMATH
Sistla A (1983) Theoretical issues in the design and verification of distributed systems. PhD thesis, Harvard University
Vardi M (1988) A temporal fixpoint calculus. In: POPL ’88 Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages. ACM, New York, pp 250–259
Metadaten
Titel
Verifying safety critical task scheduling systems in PPTL axiom system
verfasst von
Nan Zhang
Mengfei Yang
Bin Gu
Zhenhua Duan
Cong Tian
Publikationsdatum
01.02.2016
Verlag
Springer US
Erschienen in
Journal of Combinatorial Optimization / Ausgabe 2/2016
Print ISSN: 1382-6905
Elektronische ISSN: 1573-2886
DOI
https://doi.org/10.1007/s10878-014-9776-3

Weitere Artikel der Ausgabe 2/2016

Journal of Combinatorial Optimization 2/2016 Zur Ausgabe

OriginalPaper

-labeling for brick product graphs

OriginalPaper

Adjacent vertex-distinguishing edge coloring of 2-degenerate graphs

OriginalPaper

An approximation algorithm for the partial vertex cover problem in hypergraphs

OriginalPaper

Dynamic monopolies and feedback vertex sets in cycle permutation graphs, generalized Petersen graphs and torus cordalis

OriginalPaper

Scheduling dedicated jobs with variative processing times

OriginalPaper

Approximation algorithms for minimum weight partial connected set cover problem

Premium Partner

    Bildnachweise