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
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Innovations in Systems and Software Engineering
Erschienen in: Innovations in Systems and Software Engineering 4/2013

01.12.2013 | SI: SwHM

Copilot: monitoring embedded systems

verfasst von: Lee Pike, Nis Wegmann, Sebastian Niller, Alwyn Goodloe

Erschienen in: Innovations in Systems and Software Engineering | Ausgabe 4/2013

Einloggen

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

search-config
loading …

Abstract

Runtime verification (RV) is a natural fit for ultra-critical systems that require correct software behavior. Due to the low reliability of commodity hardware and the adversity of operational environments, it is common in ultra-critical systems to replicate processing units (and their hosted software) and incorporate fault-tolerant algorithms to compare the outputs, even if the software is considered to be fault-free. In this paper, we investigate the use of software monitoring in distributed fault-tolerant systems and the implementation of fault-tolerance mechanisms using RV techniques. We describe the Copilot language and compiler that generates monitors for distributed real-time systems, and we discuss two case-studies in which Copilot-generated monitors were used to detect onboard software and hardware faults and monitor air-ground data link messaging protocols.
Vorheriger Artikel Software health management: a necessity for safety critical systems
Nächster Artikel Maintaining the health of software monitors

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
To use conditionals (if-then-else’s) in Copilot specifications, as in Figs. 1 and 2, the GHC language extension RebindableSyntax must be set on.
 
2
The function permutations comes from the Haskell standard library Data.list.
 
5
Two explanations are in order: (1) reify allows sharing in the expressions to be compiled [19], and >>= is a higher-order operator that takes the result of reification and “feeds” it to the compile function.
 
6
http://​www.​cprover.​org/​cbmc/​LICENSE. It is the user’s responsibility to ensure their use conforms to the license.
 
7
Tape left on the static pitot tube of Aeroperú Flight 603 in 1996 resulted in the death of 70 passengers and crew [28].
 
9
At the time of this writing, Copilot did not handle streams of arrays. Modeling the protocol as a stream of Word32s, as we explain herein, is inefficient, resulting in a large specification.
 
10
Copilot’s nscanl is a fixed-length (of n) analogue of the Haskell scanl function in Haskell, such that scanl f z [x1, x2, ...] == [z, z ‘f‘ x1, (z ‘f‘ x1) ‘f‘ x2, ...].
 
11
We could incorporate further analysis of the packets as well, like checking for the correct length of certain MAVLink packet types or inspection of the payload. Some of these tests could be derived from the MAVLink XML protocol description automatically.
 
12
Latitude and longitude in degrees, altitude in meters.
 
13
When streams of arrays are implemented in Copilot, the CRC can be derived from a Copilot specification.
 
Literatur
1.
2.
(2010) Aeronautical radio: avionics application software standard interface: ARINC specification 653p1-3. ARINC, Inc., Annapolis. ARINC 653 Part 1
3.
(2012) Aeronautical radio: avionics application software standard interface: ARINC specification 653p2-2 extended services. ARINC Inc., Annapolis. ARINC 653 Part 2
4.
5.
Axelsson E, Claessen K, Dévai G, Horváth Z, Keijzer K, Lyckegård B, Persson A, Sheeran M, Svenningsson J, Vajda A (2010) Feldspar: a domain specific language for digital signal processing algorithms. In: 8th ACM/IEEE international conference on formal methods and models for codesign
6.
Barrett C, Sebastiani R, Seshia S, Tinelli C (2009) Satisfiability modulo theories, chap. 26, pp 825–885. In: Frontiers in artificial intelligence and applications. IOS Press, Amsterdam
7.
8.
Bonakdarpour B, Kulkarni SS (2008) SYCRAFT: a tool for synthesizing distributed fault-tolerant programs. In: International conference on concurrency theory (CONCUR ’08). Springer, Berlin, pp 167–171
9.
Bonakdarpour B, Navabpour S, Fischmeister S (2011) Sampling-based runtime verification. In: 17th International symposium on formal methods (FM)
10.
Bureau ATS (2007) In-flight upset event 240 Km North-West of Perth, WA Boeing Company 777-200, 9M-MRG 1 August 2005. ATSB Transport Safety Investigation Report. Aviation Occurrace Report-200503722
11.
Butler RW, Finelli GB (1993) The infeasibility of quantifying the reliability of life-critical real-time software. IEEE Trans Softw Eng 19:3–12CrossRef
12.
Chen F, d’Amorim M, Roşu G (2006) Checking and correcting behaviors of java programs at runtime with Java-MOP. Electron Notes Theor Comput Sci 144:3–20CrossRef
13.
Chen F, Roşu G (2005) Java-MOP: a monitoring oriented programming environment for Java. In: 11th International conference on tools and algorithms for the construction and analysis of systems (TACAS’05). LNCS, vol 3440. Springer, Berlin, pp 546–550
14.
Claessen K, Hughes J (2000) Quickcheck: a lightweight tool for random testing of haskell programs. In: ACM SIGPLAN notices. ACM, New York, pp 268–279
15.
Clarke E, Kroening D, Lerda F (2004) A tool for checking ANSI-C programs. In: Tools and algorithms for the construction and analysis of systems (TACAS). LNCS. Springer, Berlin, pp 168–176
16.
Dwyer M, Diep M, Elbaum S (2008) Reducing the cost of path property monitoring through sampling. In: Proceedings of the 23rd international conference on automated software engineering, pp 228–237
17.
Farhat H (2004) Digital design and computer organization, 1st edn. In: Digital Design and Computer Organization. CRC Press, Boca Raton
18.
Fischmeister S, Ba Y (2010) Sampling-based program execution monitoring. In: ACM International conference on Languages, compilers, and tools for embedded systems (LCTES), pp 133–142
19.
Gill A (2009) Type-safe observable sharing in Haskell. In: Proceedings of the 2009 ACM SIGPLAN Haskell Symposium
20.
Halbwachs N, Raymond P (1999) Validation of synchronous reactive systems: from formal verification to automatic testing. In: ASIAN’99 Asian computing science conference. LNCS, vol 1742. Springer, Berlin
21.
Havelund K (2008) Runtime verification of C programs. In: Testing of software and communicating systems (TestCom/FATES). Springer, Berlin, pp 7–22
22.
23.
Hesselink WH (2005) The Boyer–Moore majority vote algorithm
24.
25.
Kim M, Viswanathan M, Ben-Abdallah H, Kannan S, Lee I, Sokolsky O (1999) Formally specified monitoring of temporal properties. In: 11th euromicro conference on real-time systems, pp 114–122
26.
Klein G, Andronick J, Elphinstone K, Heiser G, Cock D, Derrin P, Elkaduwe D, Engelhardt K, Kolanski R, Norrish M, Sewell T, Tuch H, Winwood S (2010) seL4: Formal verification of an OS kernel. Commun ACM 53(6):107–115CrossRef
27.
Krüger IH, Meisinger M, Menarini M (2007) Runtime verification of interactions: from MSCs to aspects. In: International conference on runtime verification. Springer, Berlin, pp 63–74
28.
29.
Lamport L, Shostak R, Pease M (1982) The Byzantine generals problem. ACM Trans Program Lang Syst 4:382–401CrossRefMATH
30.
Leveson NG, Turner CS (1993) An investigation of the Therac-25 accidents. Computer 26:18–41CrossRef
31.
32.
33.
Moore SJ, Boyer RS (1981) MJRTY—a fast majority vote algorithm. Technical Report 1981-32, Institute for Computing Science, University of Texas
34.
Nuseibeh B (1997) Soapbox: Ariane 5: Who dunnit? IEEE Softw 14(3):15–16CrossRef
35.
Pike L, Goodloe A, Morisset R, Niller S (2010) Copilot: a hard real-time runtime monitor. In: Runtime verification (RV), vol 6418. Springer, Berlin, pp 345–359
36.
Pike L, Wegmann N, Niller S, Goodloe A (2012) Experience report: do-it-yourself high-assurance compiler. In: Proceedings of the 17th ACM SIGPLAN conference on functional programming. ACM, New York
37.
RTCA (1992) Software considerations in airborne systems and equipment certification. RTCA, Inc., USA. RCTA/DO- 178B
38.
Rushby J (2008) Runtime certification. In: RV’08: Proceedings of runtime verification, Budapest, Hungary, March 30, 2008. Selected Papers. Springer, Berlin, pp 21–35
39.
Rushby J (2009) Software verification and system assurance. In: International conference on software engineering and formal methods (SEFM). IEEE, New York, pp 3–10
40.
Sammapun U, Lee I, Sokolsky O (2005) RT-MaC: runtime monitoring and checking of quantitative and probabilistic properties. In: Proceedings of the 11th IEEE international conference on embedded and real-time computing systems and applications, pp 147–153
41.
Stoller SD, Bartocci E, Seyster J, Grosu R, Havelund K, Smolka SA, Zadok E (2011) Runtime verification with state estimation. In: Proceedings of the 2nd international conference on runtime verification (RV’11)
Metadaten
Titel
Copilot: monitoring embedded systems
verfasst von
Lee Pike
Nis Wegmann
Sebastian Niller
Alwyn Goodloe
Publikationsdatum
01.12.2013
Verlag
Springer London
Erschienen in
Innovations in Systems and Software Engineering / Ausgabe 4/2013
Print ISSN: 1614-5046
Elektronische ISSN: 1614-5054
DOI
https://doi.org/10.1007/s11334-013-0223-x

Weitere Artikel der Ausgabe 4/2013

Innovations in Systems and Software Engineering 4/2013 Zur Ausgabe

SI: SwHM

Maintaining the health of software monitors

SI: SwHM

Software health management: a necessity for safety critical systems

Editorial

Software health management

SI:SwHM

Deliberative, search-based mitigation strategies for model-based software health management

SI: SwHM

Software health management with Bayesian networks