mdh.sePublications
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Evaluation of Delay Queues for a Ravenscar Hardware Kernel
Mälardalen University, Department of Computer Science and Electronics.
2005 (English)In: Proceedings - Third ACM and IEEE International Conference on Formal Methods and Models for Co-Design, MEMOCODE'05, 2005, 247-248 p.Conference paper, Published paper (Other academic)
Place, publisher, year, edition, pages
2005. 247-248 p.
National Category
Engineering and Technology
Identifiers
URN: urn:nbn:se:mdh:diva-4206DOI: 10.1109/MEMCOD.2005.1487926Scopus ID: 2-s2.0-33745182537ISBN: 0-7803-9227-2 (print)OAI: oai:DiVA.org:mdh-4206DiVA: diva2:121236
Conference
3rd ACM and IEEE International Conferenceon Formal Methods and Models for Co-Design, MEMOCODE'05; Verona; 11 July 2005 through 14 July 2005
Available from: 2005-11-24 Created: 2005-11-24 Last updated: 2016-01-11Bibliographically approved
In thesis
1. A Formal Approach to Embedded High-Integrity Real-Time Systems
Open this publication in new window or tab >>A Formal Approach to Embedded High-Integrity Real-Time Systems
2005 (English)Doctoral thesis, comprehensive summary (Other scientific)
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.

Publisher
52 p.
Series
Mälardalen University Press Dissertations, ISSN 1651-4238 ; 19
National Category
Computer Science
Research subject
Datavetenskap
Identifiers
urn:nbn:se:mdh:diva-64 (URN)91-88834-89-1 (ISBN)
Public defence
2005-10-07, Kappa, Västerås, 13:15
Opponent
Supervisors
Available from: 2005-11-24 Created: 2005-11-24

Open Access in DiVA

No full text

Other links

Publisher's full textScopus
By organisation
Department of Computer Science and Electronics
Engineering and Technology

Search outside of DiVA

GoogleGoogle Scholar

Altmetric score

Total: 17 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf