https://www.mdu.se/

mdh.sePublikasjoner
Endre søk
RefereraExporteraLink to record
Permanent link

Direct link
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annet format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annet språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf
Temporal Skeletons for Verifying Time
Mälardalens högskola, Institutionen för datavetenskap och elektronik.
Dept. of Aeronautics and Astronautics, Massachusetts Institute of Technology, United States.ORCID-id: 0000-0003-0904-3712
Mälardalens högskola, Institutionen för datavetenskap och elektronik.ORCID-id: 0000-0001-5141-7242
2005 (engelsk)Inngår i: Proceedings of the ACM SIGAda Annual International Conference; SIGAda, 2005, s. 49-56Konferansepaper, Publicerat paper (Annet vitenskapelig)
Abstract [en]

This paper presents an intermediate notation used in a framework for verification of real-time properties. The framework aims at overcoming the need for the framework user to have significant knowledge of the verification specific detail that formal verification at some level is bound to impose on a model. In order to accomplish this, model extraction from source code of an initial formal model, a timing skeleton, is made automatically. The model refinement needed to transform the temporal skeleton into a model that can be verified is not done immediately. This allows postponement of the abstraction and specialisation needed for the verification which further improves the readability of the skeleton. The purpose of the timing skeleton is that it easily can be validated to represent the source code it was created from. The timing skeleton is then automatically refined with verification detail, and then hidden for the user, transformed into the notation of a verification tool. This transformation is hidden from the user. In order to reduce the complexity of the application model the framework uses a formally verified run-time kernel with a clear separation from the application. The kernel supports preemption, dynamic priorities and multiple processors.

sted, utgiver, år, opplag, sider
2005. s. 49-56
HSV kategori
Identifikatorer
URN: urn:nbn:se:mdh:diva-4205DOI: 10.1145/1104011.1103854Scopus ID: 2-s2.0-33244487858ISBN: 1-59593-185-6 (tryckt)OAI: oai:DiVA.org:mdh-4205DiVA, id: diva2:121235
Konferanse
ACM SIGAda Annual International Conference, SIGAda 2005: The Engineering of Correct and Reliable Software for Real-Time and Distributed Systems using Ada and Related Technologies; Atlanta, GA; United States; 13 November 2005 through 17 November 2005
Tilgjengelig fra: 2005-11-24 Laget: 2005-11-24 Sist oppdatert: 2015-07-27bibliografisk kontrollert
Inngår i avhandling
1. A Formal Approach to Embedded High-Integrity Real-Time Systems
Åpne denne publikasjonen i ny fane eller vindu >>A Formal Approach to Embedded High-Integrity Real-Time Systems
2005 (engelsk)Doktoravhandling, med artikler (Annet vitenskapelig)
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
s. 52
Serie
Mälardalen University Press Dissertations, ISSN 1651-4238 ; 19
HSV kategori
Forskningsprogram
Datavetenskap
Identifikatorer
urn:nbn:se:mdh:diva-64 (URN)91-88834-89-1 (ISBN)
Disputas
2005-10-07, Kappa, Västerås, 13:15
Opponent
Veileder
Tilgjengelig fra: 2005-11-24 Laget: 2005-11-24 Sist oppdatert: 2018-01-13

Open Access i DiVA

Fulltekst mangler i DiVA

Andre lenker

Forlagets fulltekstScopus

Person

Lundqvist, KristinaAsplund, Lars

Søk i DiVA

Av forfatter/redaktør
Lundqvist, KristinaAsplund, Lars
Av organisasjonen

Søk utenfor DiVA

GoogleGoogle Scholar

doi
isbn
urn-nbn

Altmetric

doi
isbn
urn-nbn
Totalt: 433 treff
RefereraExporteraLink to record
Permanent link

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