A formal model of the Ada Ravenscar Tasking Profile; Protected objects

被引：0
|
作者：
Lundqvist, K
Asplund, L
Michell, S
机构：
[1] Univ Uppsala, Dept Comp Syst, S-75105 Uppsala, Sweden
[2] Maurya Software, Ottawa, ON K1G 5S3, Canada
来源：
RELIABLE SOFTWARE TECHNOLOGIES - ADA-EUROPE' 99 | 1999年 / 1622卷
关键词：
D O I：
暂无
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
The definition of the Ravenscar Tasking Profile for Ada95 provides a definition of a tasking runtime system with deterministic behaviour and low enough complexity to permit a formal description of the model. The complete model of the Protected Object portion of the Ravenscar Model is presented in UPPAAL. Some important properties are verified such as timing of calls to protected procedure. This is the first time a part of an Ada run-time has been formally verified.
引用
收藏
页码：12 / 25
页数：14
相关论文
共 37 条
  • [1] A formal model of the Ada Ravenscar Tasking Profile; Delay until
    Lundqvist, K
    Asplund, L
    ACM SIGADA ANNUAL INTERNATIONAL CONFERENCE (SIGADA'99) - PROCEEDINGS, 1999, 19 (03): : 15 - 21
  • [2] On a formal model of the tasking concept in Ada
    Løvengreen, Hans Henrik
    Bjørner, Dines
    ACM SIGPLAN Notices, 1980, 15 (11): : 213 - 222
  • [3] A Circus semantics for Ravenscar protected objects
    Atiya, DA
    King, S
    Woodcock, JCP
    FME 2003: FORMAL METHODS, PROCEEDINGS, 2003, 2805 : 617 - 635
  • [4] Preservation of Timing Properties with the Ada Ravenscar Profile
    Mezzetti, Enrico
    Panunzio, Marco
    Vardanega, Tullio
    RELIABLE SOFTWARE TECHNOLOGIES - ADA-EUROPE 2010, 2010, 6106 : 153 - 166
  • [5] Process algebra model of Ada protected objects
    Liu, YA
    Xu, BW
    ACM SIGPLAN NOTICES, 2004, 39 (02) : 34 - 39
  • [6] THE ADA TASKING MODEL
    不详
    LECTURE NOTES IN COMPUTER SCIENCE, 1987, 262 : 9 - 26
  • [7] A real-time framework for Ada 2005 and the Ravenscar profile
    Gregertsen, Kristoffer Nyborg
    Skavhaug, Amund
    2009 35TH EUROMICRO CONFERENCE ON SOFTWARE ENGINEERING AND ADVANCED APPLICATIONS, PROCEEDINGS, 2009, : 515 - 522
  • [8] The Ravenscar tasking profile for high integrity real-time programs
    Burns, A
    Dobbing, B
    Romanski, G
    RELIABLE SOFTWARE TECHNOLOGIES - ADA-EUROPE, 1998, 1411 : 263 - 275
  • [9] Implementing execution-time clocks for the Ada Ravenscar profile
    Zamorano, J
    Alonso, A
    Pulido, JA
    de la Puente, JA
    RELIABLE SOFTWARE TECHNOLOGIES- ADA-EUROPE 2004, 2004, 3063 : 132 - 143
  • [10] Visual execution model for Ada tasking
    Dillon, Laura K.
    ACM Transactions on Software Engineering and Methodology, 1993, 2 (04) : 1 - 11
1234