nach oben

Journal of Combinatorial Optimization

Erschienen in:

03.09.2018

Verifying a scheduling protocol of safety-critical systems

verfasst von: Meng Wang, Cong Tian, Nan Zhang, Zhenhua Duan, Hongwei Du

Erschienen in: Journal of Combinatorial Optimization | Ausgabe 4/2019

Einloggen

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

search-config

KI-gestützte Suche

Aus

Abstract

It is of great importance to ensure safety and reliability of the scheduling protocol of safety-critical systems since the failure will cause serious damage. This paper analyzes a real-time scheduling protocol of a safety-critical system and models it using a Modeling, Simulation and Verification Language program. Further, the schedulability and other desired properties are specified using Propositional Projection Temporal Logic formulas. As a result, these properties are proved with theorem proving and further verified using the runtime verification approach at code level.

Vorheriger Artikel An approximation algorithm for genome sorting by reversals to recover all adjacencies

Nächster Artikel A new look at the returning secretary problem

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

Ahmed W, Hasan O, Tahar S (2015) Formal reliability analysis of wireless sensor network data transport protocols using HOL. In: IEEE international conference on wireless and mobile computing, networking and communications, pp 217–224

Angeletti D, Giunchiglia E, Narizzano M, Puddu A, Sabina S (2010) Using bounded model checking for coverage analysis of safety-critical software in an industrial setting. J Autom Reason 45(4):397–414MathSciNetCrossRef

Armando A, Mantovani J, Platania L (2006) Bounded model checking of software using SMT solvers instead of SAT solvers. In: Valmari A (ed) Model checking software. SPIN 2006. Lecture notes in computer science, vol 3925. Springer, Berlin, Heidelberg, pp 146–162

Bernardeschi C, Domenici A (2016) Verifying safety properties of a nonlinear control by interactive theorem proving with the prototype verification system. Inf Process Lett 116(6):409–415MathSciNetCrossRefMATH

Bertot Y, Castéran P (2004) Interactive theorem proving and program development. Springer, New YorkCrossRefMATH

Beyer D, Keremoglu ME (2011) CPAchecker: a tool for configurable software verification. In: Gopalakrishnan G, Qadeer S (eds) Computer aided verification. CAV 2011. Lecture notes in computer science, vol 6806. Springer, Berlin, Heidelberg, pp 184–190

Blech JO, Ould Biha S (2011) Verification of PLC properties based on formal semantics in Coq. In: Barthe G, Pardo A, Schneider G (eds) Software engineering and formal methods. Springer, Berlin, pp 58–73CrossRef

Brockschmidt M, Cook B, Ishtiaq S, Khlaaf H, Piterman N (2016) T2: temporal property verification. In: International conference on tools and algorithms for the construction and analysis of systems, Springer, pp 387–393

Chen L, Jiao J, Wei Q, Zhao T (2017) An improved formal failure analysis approach for safety-critical system based on MBSA. Eng Fail Anal 82:713–725CrossRef

Cimatti A, Clarke E, Giunchiglia F, Roveri M (2000) NuSMV: a new symbolic model checker. Int J Softw Tools Technol Transf 2(4):410–425CrossRefMATH

Clarke E, Grumberg O, Jha S, Lu Y, Veith H (2000) Counterexample-guided abstraction refinement. In: International conference on computer aided verification, Springer, pp 154–169

Clarke EM, Emerson EA, Sistla AP (1986) Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans Program Lang Syst (TOPLAS) 8(2):244–263CrossRefMATH

Clarke EM, Grumberg O, Peled D (1999) Model checking. MIT press, Cambridge

Dietsch D, Heizmann M, Langenfeld V, Podelski A (2015) Fairness modulo theory: a new approach to LTL software model checking. In: Computer aided verification

Duan Z (1996) An extended interval temporal logic and a framing technique for temporal logic programming. PhD thesis, University of Newcastle upon Tyne

Duan Z (2005) Temporal logic and temporal logic programming. Science Press, Henderson

Duan Z, Koutny M (2004) A framed temporal logic programming language. J Comput Sci Technol 19(3):341–351MathSciNetCrossRef

Duan Z, Tian C (2014) A practical decision procedure for propositional projection temporal logic with infinite models. Theor Comput Sci 554:169–190MathSciNetCrossRefMATH

Duan Z, Yang X, Koutny M (2008) Framed temporal logic programming. Sci Comput Program 70(1):31–61MathSciNetCrossRefMATH

Duan Z, Zhang N, Koutny M (2013) A complete proof system for propositional projection temporal logic. Theor Comput Sci 497:84–107 (Combinatorial Algorithms and Applications)MathSciNetCrossRefMATH

Duan Z, Tian C, Zhang N (2016) A canonical form based decision procedure and model checking approach for propositional projection temporal logic. Elsevier, New YorkCrossRefMATH

Gordon MJC, Melham TF (1993) Introduction to HOL: a theorem proving environment for higher order logic. IEEE Trans Reliab 89:317–320MATH

Holzmann GJ (1997) The model checker SPIN. IEEE Trans Software Eng 23(5):279–295CrossRef

Kaufmann M, Moore JS (2008) An ACL2 tutorial. In: Mohamed OA, Muñoz C, Tahar S (eds) Theorem proving in higher order logics. Springer, Berlin, pp 17–21CrossRef

Kroening D, Tautschnig M (2014) CBMC–C bounded model checker. In: Tools and algorithms for construction and analysis of systems

Melham T (1993) Higher order logic and hardware verification. Cambridge University Press, CambridgeCrossRefMATH

Owre S, Rushby JM, Shankar N (1992) PVS: a prototype verification system. In: International conference on automated deduction, Springer, pp 748–752

Paulson LC (1994) Isabelle–a generic theorem prover. Of LNCS. Springer, New YorkMATH

Pnueli A (1977) The temporal logic of programs. In: 18th annual symposium on foundations of computer science, 1977, IEEE, pp 46–57

Richards RJ (2010) Modeling and security analysis of a commercial real-time operating system kernel. Springer, Boston, pp 301–322

Spichkova M, Blech JO, Herrmann P, Schmidt H (2014) Modeling spatial aspects of safety-critical systems with focus-st. In: The workshop on model driven engineering, pp 49–58

Sun J, Liu Y, Dong JS (2008) Model checking CSP revisited: introducing a process analysis toolkit. In: international symposium on leveraging applications of formal methods, verification and validation, Springer, pp 307–322

Tuan LA, Man CZ, Quan TT (2010) Modeling and verification of safety critical systems: a case study on pacemaker. In: Fourth international conference on secure software integration and reliability improvement, pp 23–32

Vardi MY (1991) Verification of concurrent programs: the automata-theoretic framework. Ann Pure Appl Logic 51(1–2):79–98MathSciNetCrossRefMATH

Wang M, Tian C, Duan Z (2017) Full regular temporal property verification as dynamic program execution. In: Proceedings of the 39th international conference on software engineering, ICSE 2017, Buenos Aires, Argentina, May 20–28, 2017—companion volume, pp 226–228

Wang X, Tian C, Duan Z, Zhao L (2017) MSVL: a typed language for temporal logic programming. Front Comput Sci 11(5):762–785CrossRef

Yang K, Duan Z, Tian C, Zhang N (2017) A compiler for MSVL and its applications. Theor Comput Sci. https://doi.org/10.1016/j.tcs.2017.07.032

Yang X, Duan Z (2007) Operational semantics of framed temporal logic programs. Logic Program Proceed 3668:356–370MATH

Yasmeen A, Feigh KM, Gelman G, Gunter EL (2012) Formal analysis of safety-critical system simulations. In: International conference on application and theory of automation in command and control systems, ATACCS ’12, London, UK, May 29–31, 2012, pp 71–81

Zhang N, Yang M, Gu B, Duan Z, Tian C (2014) Verifying safety critical task scheduling systems in PPTL axiom system. J Comb Optim 31(2):1–27MathSciNetMATH

Titel: Verifying a scheduling protocol of safety-critical systems
verfasst von: Meng Wang
Cong Tian
Nan Zhang
Zhenhua Duan
Hongwei Du
Publikationsdatum: 03.09.2018
Verlag: Springer US
Erschienen in: Journal of Combinatorial Optimization / Ausgabe 4/2019
Print ISSN: 1382-6905
Elektronische ISSN: 1573-2886
DOI: https://doi.org/10.1007/s10878-018-0343-1

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

Springer Professional "Technik"

Weitere Artikel der Ausgabe 4/2019

An approximation algorithm for genome sorting by reversals to recover all adjacencies

Estimating the number of basins of attraction of multi-objective combinatorial problems

LP-based pivoting algorithm for higher-order correlation clustering

Efficient algorithms for computing one or two discrete centers hitting a set of line segments

On operations preserving semi-transitive orientability of graphs

A new look at the returning secretary problem