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
A Formal Approach to Embedded High-Integrity Real-Time Systems
Mälardalen University, Department of Computer Science and Electronics.
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.

Place, publisher, year, edition, pages
2005. , 52 p.
Series
Mälardalen University Press Dissertations, ISSN 1651-4238 ; 19
National Category
Computer Science
Research subject
Datavetenskap
Identifiers
URN: urn:nbn:se:mdh:diva-64ISBN: 91-88834-89-1 (print)OAI: oai:DiVA.org:mdh-64DiVA: diva2:121240
Public defence
2005-10-07, Kappa, Västerås, 13:15
Opponent
Supervisors
Available from: 2005-11-24 Created: 2005-11-24
List of papers
1. Component-Based Approach to Run-Time Kernel Specification and Verification
Open this publication in new window or tab >>Component-Based Approach to Run-Time Kernel Specification and Verification
2005 (English)In: Proceedings - Euromicro Conference on Real-Time Systems, 2005, 68-76 p.Conference paper, Published paper (Other academic)
National Category
Engineering and Technology
Identifiers
urn:nbn:se:mdh:diva-4204 (URN)10.1109/ECRTS.2005.11 (DOI)000231059000008 ()2-s2.0-33749057483 (Scopus ID)0769524001 (ISBN)
Conference
17th Euromicro Conference on Real-Time Systems, ECRTS 2005; Palma de Mallorca, Balearic Islands; 6 July 2005 through 8 July 2005
Available from: 2005-11-24 Created: 2005-11-24 Last updated: 2016-01-11Bibliographically approved
2. Temporal Skeletons for Verifying Time
Open this publication in new window or tab >>Temporal Skeletons for Verifying Time
2005 (English)In: Proceedings of the ACM SIGAda Annual International Conference; SIGAda, 2005, 49-56 p.Conference paper, Published paper (Other academic)
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.

National Category
Computer Systems
Identifiers
urn:nbn:se:mdh:diva-4205 (URN)10.1145/1104011.1103854 (DOI)2-s2.0-33244487858 (Scopus ID)1-59593-185-6 (ISBN)
Conference
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
Available from: 2005-11-24 Created: 2005-11-24 Last updated: 2015-07-27Bibliographically approved
3. Evaluation of Delay Queues for a Ravenscar Hardware Kernel
Open this publication in new window or tab >>Evaluation of Delay Queues for a Ravenscar Hardware Kernel
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)
National Category
Engineering and Technology
Identifiers
urn:nbn:se:mdh:diva-4206 (URN)10.1109/MEMCOD.2005.1487926 (DOI)2-s2.0-33745182537 (Scopus ID)0-7803-9227-2 (ISBN)
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
4. SafetyChip: A Time Monitoring and Policing Device
Open this publication in new window or tab >>SafetyChip: A Time Monitoring and Policing Device
2005 (English)In: Proceedings of the ACM SIGAda Annual International Conference; SIGAda, 2005, 63-68 p.Conference paper, Published paper (Other academic)
Abstract [en]

The SafetyChip proposes a strategy where parts of the effort invested in the formal verification during the development of a system can be reused during the system's operation. The strength in a formal verification of a system is that a system can mathematically be proven to fulfil certain requirements, e.g., timing requirements. The SafetyChip uses information from verification to monitor and police a system during run-time. The monitoring is done by surveillance of the applications communication with the run-time kernel. If deviance from the predefined verified behaviour is detected, the SafetyChip can signal (police) this in different ways, e.g., by generating interrupts the system can respond to. In our experiments we use systems written in Ravenscar compliant Ada code and have automated model extraction from source code to the models used to verify the system. This paper presents the functionality and design of the SafetyChip. Properties of an implementation of the Safety-Chip are also presented. 

National Category
Computer Systems Other Electrical Engineering, Electronic Engineering, Information Engineering
Identifiers
urn:nbn:se:mdh:diva-4207 (URN)10.1145/1104011.1103856 (DOI)2-s2.0-33244482621 (Scopus ID)1-59593-185-6 (ISBN)
Conference
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
Available from: 2005-11-24 Created: 2005-11-24 Last updated: 2015-07-27Bibliographically approved
5. A Run-Time Kernel for Ravenscar
Open this publication in new window or tab >>A Run-Time Kernel for Ravenscar
(English)Manuscript (Other academic)
National Category
Electrical Engineering, Electronic Engineering, Information Engineering
Identifiers
urn:nbn:se:mdh:diva-4208 (URN)
Available from: 2005-11-24 Created: 2005-11-24 Last updated: 2015-10-12Bibliographically approved
6. Transforming Timing Skeletons to Timed Automata
Open this publication in new window or tab >>Transforming Timing Skeletons to Timed Automata
(English)Manuscript (Other academic)
National Category
Electrical Engineering, Electronic Engineering, Information Engineering
Identifiers
urn:nbn:se:mdh:diva-4209 (URN)
Available from: 2005-11-24 Created: 2005-11-24 Last updated: 2015-10-12Bibliographically approved

Open Access in DiVA

No full text

By organisation
Department of Computer Science and Electronics
Computer Science

Search outside of DiVA

GoogleGoogle Scholar

Total: 121 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