Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Real-Time Systems
Published in: Real-Time Systems 5/2017

27-07-2017

High-assurance timing analysis for a high-assurance real-time operating system

Authors: Thomas Sewell, Felix Kam, Gernot Heiser

Published in: Real-Time Systems | Issue 5/2017

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

Worst-case execution time (WCET) analysis of real-time code needs to be performed on the executable binary code for soundness. Obtaining tight WCET bounds requires determination of loop bounds and elimination of infeasible paths. The binary code, however, lacks information necessary to determine these bounds. This information is usually provided through manual intervention, or preserved in the binary by a specially modified compiler. We propose an alternative approach, using an existing translation-validation framework, to enable high-assurance, automatic determination of loop bounds and infeasible paths. We show that this approach automatically determines all loop bounds and many (possibly all) infeasible paths in the seL4 microkernel, as well as in standard WCET benchmarks which are in the language subset of our C parser. We also design and validate an improvement to the seL4 implementation, which permits a key part of the kernel’s API to be available to users in a mixed-criticality setting.
previous article Mixed-criticality federated scheduling for parallel real-time tasks

Dont have a licence yet? Then find out more about our products and how to get one now:

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!

inform now

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!

inform now

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!

inform now
Footnotes
1
Here and later we use “SMT model” to mean a set of definitions in the SMT language, used to phrase a satisfiability query, rather than a satisfying model of such a query.
 
2
This expression is constant at each address in the loop. If the initial value of r4 were 4, the expression would be evaluate to the constant 0 whenever execution was at the first two instructions, but 4 after the add instruction.
 
3
The story is a little more complex. Some calls to f in the source code may not be present in the binary thanks to inlining, and functions which are known not to inspect memory may be moved across memory updates. The TV tool picks a particular concrete input relation for each binary function, and proves that this holds at all its call sites.
 
4
Some loops in the binary are preemptible and do not have bounds.
 
5
Note that the total number of loops here is higher than in our earlier work. This results from this work targeting the verified kernel, and thus using preemption points less aggressively, see Sect. 2.2.
 
6
The minimum setting, 1, eliminates the outer loop entirely.
 
7
Higher optimisation settings usually result in larger binaries, and instruction cache pressure is known to be an important factor in microkernel performance.
 
8
The TV toolset handles some very simple cases of limited recursion.
 
Literature
Amadio RM, Ayache N, Bobot F, Boender JP, Campbell B, Garnier I, Madet A, McKinna J, Mulligan DP, Piccolo M, et al Certified complexity (CerCo) (2013) In: International workshop on foundational and practical aspects of resource analysis. Springer, Berlin, pp 1–18
Ayache N, Amadio R, Régis-Gianas Y (2012) Certifying and reasoning on cost annotations in C programs. In: FMICS 2012—17th international workshop on formal methods for industrial critical systems, Paris, France, Aug 2012
Andronick J, Lewis C, Morgan C (2015) Controlled owicki-gries concurrency: reasoning about the preemptible eChronos embedded operating system. In: van Glabbeek RJ, Groote JF, Höfner P (eds) Workshop on models for formal analysis of real systems (MARS 2015), Suva, Fiji, pp 10–24, Nov 2015
Alkassar E, Paul W, Starostin A, Tsyban A (2010) Pervasive verification of an OS microkernel: inline assembly, memory consumption, concurrent devices. In: O’Hearn P, Leavens GT, Rajamani S (eds) VSTTE 2010. LNCS, vol 6217, Edinburgh, UK. Springer, pp 71–85, Aug 2010
Avionics Application Software Standard Interface (2012) ARINC Standard 653
Bevier WR (1989) Kit: a study in operating system verification. Trans Softw Eng 15(11):1382–1396CrossRef
Bromberger AC, Peri Frantz A, Frantz WS, Hardy AC, Hardy N, Landau CR, Shapiro JS (1992) The KeyKOS nanokernel architecture. In: USENIX WS Microkernels & other Kernel Arch. Seattle, WA, US, pp 95–112
Blackham B, Heiser G (2013) Sequoll: a framework for model checking binaries. In: Tovar E (ed) RTAS, Philadelphia, USA, pp 97–106, Apr 2013
Blanc R, Henzinger TA, Hottelier T, Kovács L (2010) ABC: algebraic bound computation for loops. In: 16th international conference on logic programming, artificial intelligence & reasoning. Springer, pp 103–118
Bardin S, Herrmann P, Védrine F (2011) Refinement-based CFG reconstruction from unstructured programs. In: International conference on verification, model checking & abstract interpretation. Springer, Berlin, pp 54–69
Blackham B, Liffiton M, Heiser G (2014) Trickle: automated infeasible path detection using all minimal unsatisfiable subsets. In: West R (ed) RTAS, Berlin, Germany, pp 169–178, Apr 2014
Burguière C, Rochange C (2006) History-based schemes and implicit path enumeration. In: 6th WS worst-case execution-time analysis
Blackham B, Shi Y, Chattopadhyay S, Roychoudhury A, Heiser G (2011) Timing analysis of a protected operating system kernel. In: RTSS, Vienna, Austria, pp 339–348, Nov 2011
Blackham B, Shi Y, Heiser G (2012) Improving interrupt response time in a verifiable protected microkernel. In: EuroSys, Bern, Switzerland, pp 323–336, Apr 2012
Blackham B, Tang V, Heiser G (2012) To preempt or not to preempt, that is the question. In: APSys, ACM, Seoul, Korea, p 7, July 2012
Clarke E, Grumberg O, Jha S, Yuan L, Veith H (2003) Counterexample-guided abstraction refinement for symbolic model checking. J ACM 50(5):752–794MathSciNetCrossRefMATH
Cullmann C, Martin F (2007) Data-flow based detection of loop bounds. In: 7th WS worst-case execution-time analysis
Cohen E, Schirmer N (2010) From total store order to sequential consistency: a practical reduction theorem. In: Kaufmann M, Paulson L (eds) 1st ITP. LNCS, vol 6172. Springer, Edinburgh, UK, pp 403–418, July 2010
Dietz W, Li P, Regehr J, Adve V (2012) Understanding integer overflow in C/C++. In: Proceedings of the 34th international conference on software engineering, ICSE ’12. IEEE Press, Piscataway, NJ, USA, pp 760–770
de Roever WP, de Boer F, Hanneman U, Hooman J, Lakhnech Y, Poel M, Zwiers J (2001) Concurrency verification: introduction to compositional and non-compositional methods. Cambridge Tracts in Theoretical Computer Science
Dennis JB, Van Horn EC (1966) Programming semantics for multiprogrammed computations. CACM 9:143–155CrossRefMATH
Ermedahl A, Sandberg C, Gustafsson J, Bygde S, Lisper B (2007) Loop bound analysis based on a combination of program slicing, abstract interpretation, and invariant analysis. In: WS worst-case execution-time analysis
Feng X, Ferreira R, Shao Z (2007) On the relationship between concurrent separation logic and assume-guarantee reasoning. In: ESOP. Springer, pp 173–188
Ferdinand C, Heckmann R, Langenbach M, Martin F, Schmidt M, Theiling H, Thesing S, Wilhelm R (2001) Reliable and precise WCET determination for a real-life processor. In: EMSOFT. Springer, London, UK, pp 469–485
Fox A, Myreen M (2010) A trustworthy monadic formalization of the ARMv7 instruction set architecture. In: Kaufmann M, Paulson LC (eds) 1st ITP. LNCS, vol 6172. Springer, Edinburgh, UK, pp 243–258, July 2010
Gustafsson J, Betts A, Ermedahl A, Lisper B (2010) The Mälardalen WCET benchmarks—past, present and future. In: 10th WS worst-case execution-time analysis. OCG, Brussels, BE, pp 137–147, July 2010
Gustafsson J, Ermedahl A, Sandberg C, Lisper B (2006) Automatic derivation of loop bounds and infeasible paths for WCET analysis using abstract execution. In: RTSS. IEEE Computer Society, Washington, DC, US, pp 57–66
Gammie P, Hosking T, Engelhardt K (2015) Relaxing safely: verified on-the-fly garbage collection for x86-TSO. In: Blackburn S (ed) PLDI 2015: the 36th annual ACM SIGPLAN conference on Programming Language Design and Implementation. ACM, Portland, Oregon, United States, p 11, June 2015
Gu R, Shao Z, Chen H, Wu X, Kim J, Sjöberg V, Costanzo D (2016) An extensible architecture for building certified concurrent OS kernels. In: OSDI, CertiKOS
Healy CA, Arnold RD, Müller F, Whalley DB, Harmon Marion G (1999) Bounding pipeline and instruction cache performance. Trans Comput 48:63–70CrossRef
Heiser G, Elphinstone K (2016) L4 microkernels: the lessons from 20 years of research and deployment. Trans Comput Syst 34(1):1:1–1:29
Hergenhan A, Heiser G (2008) Operating systems technology for converged ECUs. In: 6th embedded security in cars conference (escar), Hamburg, Germany, Nov 2008
Henzinger TA, Jhala R, Majumdar R (2003) Counterexample-guided control. In: 30th ICALP, Eindhoven, The Netherlands, pp 886–902, July 2003
ISO (2011) ISO26262: road vehicles—functional safety
Klein G, Andronick J, Elphinstone K, Murray T, Sewell T, Kolanski R, Heiser G (2014) Comprehensive formal verification of an OS microkernel. Trans Comput Syst 32(1):2:1–2:70
Kim TH, Bang HJ, Cha SD (2010) A systematic representation of path constraints for implicit path enumeration technique. Softw Test Verif Reliab 20(1):39–61CrossRef
Klein G, Elphinstone K, Heiser G, Andronick J et al (2009) seL4: formal verification of an OS kernel. In: SOSP, Big Sky, MT, US, pp 207–220, Oct 2009
Kirner R, Knoop J, Prantl A, Schordan M, Kadlec A (2011) Beyond loop bounds: comparing annotation languages for worst-case execution time analysis. Softw Syst Model 10(3):411–437CrossRef
Knoop J, Kovács L, Zwirchmayr J (2011) Symbolic loop bound computation for WCET analysis. In: International Andrei Ershov memorial conference
Knoop J, Kovács L, Zwirchmayr J (2013) WCET squeezing: On-demand feasibility refinement for proven precise WCET-bounds. In: Proceedings of the 21st international conference on real-time networks and systems, RTNS ’13. ACM, New York, NY, USA, pp 161–170
Kinder J, Zuleger F, Veith H (2009) An abstract interpretation-based framework for control flow reconstruction from binaries. In: 10th International conference on verification, model checking & abstract interpretation. Springer, pp 214–228
Lokuciejewski P, Cordes D, Falk H, Marwedel P (2009) A fast and precise static loop analysis based on abstract interpretation, program slicing and polytope models. In: 7th symposium code generation & optimization. IEEE Computer Society, Washington, DC, US, pp 136–146
Leroy X (2009) Formal verification of a realistic compiler. CACM 52(7):107–115CrossRef
Lyons A, Heiser G (2014) Mixed-criticality support in a high-assurance, general-purpose microkernel. In: Davis R, Cucu-Grosjean L (eds) WS mixed criticality system, Rome, Italy, pp 9–14, Dec 2014
Lyons A, Heiser G (2016) It’s time: OS mechanisms for enforcing asymmetric temporal integrity. arXiv preprint
Liedtke J (1994) Page table structures for fine-grain virtual memory. In: IEEE Technical Committee on Computer Architecture Newsletter, Oct 1994
Lisper B (2005) Ideas for annotation language (s). Technical report, Technical Report Oct. 25, Department of Computer Science and Engineering, University of Mälardalen
Li X, Liang Y, Mitra T, Roychoudhury A (2007) Chronos: a timing analyzer for embedded software. Sci Comput Program Spec Issue Exp Softw Toolkit 69(1–3):56–67MathSciNetMATH
Li Y-T, Malik S (1995) Performance analysis of embedded software using implicit path enumeration. In: Proceedings of the 32nd ACM/IEEE design automation conference. ACM, pp 456–461, June 1995
Lundqvist T, Stenström P (1998) Integrating path and timing analysis using instruction level simulation techniques. In: Proceedings of the ACM SIGPLAN workshop on languages, compilers and tools for embedded systems. LNCS. Springer, Montreal CA, June 1998
Li Y, West R, Missimer ES (2013) The quest-V separation kernel for mixed criticality systems. In: WS mixed criticality system, pp 31–36, Dec 2013
MISRA (2012) Guidelines for the Use of the C language in critical systems
Murray T, Matichuk D, Brassil M, Gammie P, Bourke T, Seefried S, Lewis C, Gao X, Klein G (2013) seL4: from general purpose to a proof of information flow enforcement. In: S&P, San Francisco, CA, pp 415–429, May 2013
Martin WB, White PD, Taylor FS (2002) Creating high confidence in a separation kernel. Autom Softw Eng 9(3):263–284CrossRefMATH
Nipkow T, Paulson L, Wenzel M (2002) Isabelle/HOL—a proof assistant for higher-order logic. LNCS, vol 2283. Springer, Berlin
Puschner P, Koza C (1989) Calculating the maximum execution time of real-time programs. Real-Time Syst 1(2):159–176CrossRef
Prantl A, Knoop J, Kirner R, Kadlec A, Schordan M (2009) From trusted annotations to verified knowledge. In: WS worst-case execution-time analysis, Dublin, IE, pp 35–45, June 2009
Park CY, Shaw AC (1991) Experiments with a program timing tool based on source–level timing schema. Trans Comput 24(5):48–57
Raymond P (2014) A general approach for expressing infeasibility in implicit path enumeration technique. In: Proceedings of the 14th international conference on embedded software. ACM, pp 8
Rieder B, Puschner P, Wenzel I (2008) Using model checking to derive loop bounds of general loops within ANSI-C applications for measurement based WCET analysis. In: 2008 International Workshop on intelligent solutions in embedded systems, pp 1–7, Jul 2008
RTCA (1992) DO-178B: Software Considerations in Airborne Systems and Equipment Certification
RTCA (2011) DO-178C: Software Considerations in Airborne Systems and Equipment Certification
Rushby J (1981) Design and verification of secure systems. In: SOSP, Pacific Grove, CA, USA, pp 12–21, Dec 1981
Shi Y, Blackham B, Heiser G (2013) Code optimizations using formally verified properties. In: OOPSLA, Indianapolis, USA, pp 427–442, Oct 2013
Schlich B (2010) Model checking of software for microcontrollers. ACM Trans Embed Comput Syst 9(4):36CrossRef
Sewell T, Myreen M, Klein G (2013) Translation validation for a verified OS kernel. In: PLDI. ACM, Seattle, Washington, USA, pp 471–481, Jun 2013
Slind K, Norrish M (2008) A brief overview of HOL4. In: Mohamed OA, Muoz C, Tahar S (eds) TPHOLs. Springer, Montral, Canada, pp 28–32, Aug 2008
Sewell T, Winwood S, Gammie P, Murray T, Andronick J, Klein G (2011) seL4 enforces integrity. In: van Eekelen M, Geuvers H, Schmaltz J, Wiedijk F (eds) ITP. Springer, Nijmegen, The Netherlands, pp 325–340, Aug 2011
Tuch H, Klein G, Norrish M (2007) Types, bytes, and separation logic. In: Hofmann M, Felleisen M (eds) POPL. ACM, Nice, France, pp 97–108, Jan 2007
Turon A, Vafeiadis V, Dreyer D (2014) GPS: navigating weak memory with ghosts, protocols, and separation. In: ACM SIGPLAN notices, vol 49. ACM, pp 691–707
Wilhelm R, Engblom J, Ermedahl A, Holsti N, Thesing S, Whalley D, Bernat G, Ferdinand C, Heckmann R, Mitra Tulika, Mueller Frank, Puaut I, Puschner P, Staschulat J, Stenström P (2008) The worst-case execution-time problem—overview of methods and survey of tools. Trans Embed Comput Syst 7(3):1–53CrossRef
Walker BJ, Kemmerer RA, Popek GJ (1980) Specification and verification of the UCLA Unix security kernel. CACM 23(2):118–131CrossRefMATH
Yang J, Hawblitzel C (2010) Safe to the last instruction: automated verification of a type-safe operating system. In: 2010 PLDI. ACM, Toronto, Ont, CA, pp 99–110, Jun 2010
Metadata
Title
High-assurance timing analysis for a high-assurance real-time operating system
Authors
Thomas Sewell
Felix Kam
Gernot Heiser
Publication date
27-07-2017
Publisher
Springer US
Published in
Real-Time Systems / Issue 5/2017
Print ISSN: 0922-6443
Electronic ISSN: 1573-1383
DOI
https://doi.org/10.1007/s11241-017-9286-3

Other articles of this Issue 5/2017

Real-Time Systems 5/2017 Go to the issue

EditorialNotes

Guest editorial: special issue on mixed-criticality, multi-core, and micro-kernels

OriginalPaper

Addressing isolation challenges of non-blocking caches for multicore real-time systems

OriginalPaper

Attacking the one-out-of-m multicore problem by combining hardware management with mixed-criticality provisioning

OriginalPaper

Mixed-criticality federated scheduling for parallel real-time tasks

Premium Partner

    Image Credits