mdh.sePublikationer
Ändra sökning
RefereraExporteraLänk till posten
Permanent länk

Direktlänk
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf
A Run-Time Kernel for Ravenscar
Mälardalens högskola, Institutionen för datavetenskap och elektronik.
(Engelska)Manuskript (Övrigt vetenskapligt)
Nationell ämneskategori
Elektroteknik och elektronik
Identifikatorer
URN: urn:nbn:se:mdh:diva-4208OAI: oai:DiVA.org:mdh-4208DiVA, id: diva2:121238
Tillgänglig från: 2005-11-24 Skapad: 2005-11-24 Senast uppdaterad: 2015-10-12Bibliografiskt granskad
Ingår i avhandling
1. A Formal Approach to Embedded High-Integrity Real-Time Systems
Öppna denna publikation i ny flik eller fönster >>A Formal Approach to Embedded High-Integrity Real-Time Systems
2005 (Engelska)Doktorsavhandling, sammanläggning (Övrigt vetenskapligt)
Abstract [sv]

Den här avhandlingen handlar inte om obskyra teoretiska datavetenskapliga hemligheter, den handlar om hur datorsystem kan göras säkrare. Ur ett annat perspektiv kan den sägas försöka sig på att göra svåra metoder, som formella sådana, lättare att använda så att fler programmerare och systemdesigners kan dra nytta av dem. Massor av dagligen använda system tros vara korrekta, utan att de bevisats vara det. Testning, den vanligaste metoden för att upptäcka defekter och fel kan bara hitta fel som testaren letar efter, de problem som förväntas. Formell verifiering, en mindre använd metod för att hitta fel, kan bättre hitta oväntade problem.

Med ökningen i antal säkerhetskritiska system ökar även kraven som ställs på att de ska fungera tillförlitligt. Samtidigt måste de som utvecklar systemen hålla nere utvecklingskostnaden och med de begränsade resurser som finns tillhanda kan de oftast inte kosta på sig att nyttja alla traditionellt säkra, men dyra, metoder för att tillse systemens tillförlitlighet.

SafetyChip-ramverket, som presenteras i den här avhandlingen, ger ett sätt att angripa problemet genom maskinell modellering som används till att både assistera formell verifiering samt till att låta delar av investeringen i dem återanvändas senare under systemets livscykel. T.ex. använder specialkonstruerad hårdvara biprodukter från verifieringen till att övervaka och styra systemet under drift.

Flera problem som begränsar användandet av formella metoder i säkerhets\-kritiska system undersöks och löses, t.ex. med användandet av en realtidskärna för Ravenscar (en programmeringsprofil). Kärnan beskrivs formellt, verifieras och realiseras delvis i hårdvara. Experiment för att värdera användbarheten av ramverket i en medelstor tillämpningar har genomförts med lovande utgång.

Förlag
s. 52
Serie
Mälardalen University Press Dissertations, ISSN 1651-4238 ; 19
Nationell ämneskategori
Datavetenskap (datalogi)
Forskningsämne
Datavetenskap
Identifikatorer
urn:nbn:se:mdh:diva-64 (URN)91-88834-89-1 (ISBN)
Disputation
2005-10-07, Kappa, Västerås, 13:15
Opponent
Handledare
Tillgänglig från: 2005-11-24 Skapad: 2005-11-24 Senast uppdaterad: 2018-01-13

Open Access i DiVA

Fulltext saknas i DiVA

Av organisationen
Institutionen för datavetenskap och elektronik
Elektroteknik och elektronik

Sök vidare utanför DiVA

GoogleGoogle Scholar

urn-nbn

Altmetricpoäng

urn-nbn
Totalt: 56 träffar
RefereraExporteraLänk till posten
Permanent länk

Direktlänk
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf