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 条
  • [31] Model-Based Analysis and Design of Real-Time Distributed Systems with Ada and the UML Profile for MARTE
    Medina, Julio L.
    Garcia Cuesta, Alvaro
    RELIABLE SOFTWARE TECHNOLOGIES - ADA-EUROPE 2011, 2011, 6652 : 89 - 102
  • [32] Identifying the objects in the structure of an e-model by means of identified formal parameters in the design and engineering environment
    Lavrentyieva, Mariya
    Govorkov, Aleksey
    INTERNATIONAL CONFERENCE ON MODERN TRENDS IN MANUFACTURING TECHNOLOGIES AND EQUIPMENT (ICMTMTE 2017), 2017, 129
  • [33] BROA: An agent-based model to recommend relevant Learning Objects from Repository Federations adapted to learner profile
    Rodriguez, Paula A.
    Tabares, Valentina
    Duque, Nestor D.
    Ovalle, Demetrio A.
    Vicari, Rosa M.
    INTERNATIONAL JOURNAL OF INTERACTIVE MULTIMEDIA AND ARTIFICIAL INTELLIGENCE, 2013, 2 (01): : 6 - 11
  • [34] Formal Model of the Synthesized Screen Image of a Dynamic Situation in Areas of Monitoring Mobile Objects and its Implementation in a Web-Oriented Geoinformation System
    Qasem A.M.
    Cybernetics and Systems Analysis, 2017, 53 (1) : 125 - 137
  • [35] Simulation of Ku-Band Profile Radar Waveform by Extending Radiosity Applicable to Porous Individual Objects (RAPID2) Model
    Du, Kai
    Huang, Huaguo
    Zhu, Yuyi
    REMOTE SENSING, 2020, 12 (04)
  • [36] Simulation of Ku-Band Profile Radar Waveform by Extending Radiosity Applicable to Porous Individual Objects (RAPID2) Model (vol 12, 684, 2020)
    Du, Kai
    Huang, Huaguo
    Zhu, Yuyi
    Feng, Ziyi
    Hakala, Teemu
    Chen, Yuwei
    Hyyppa, Juha
    REMOTE SENSING, 2020, 12 (17)
  • [37] Discussion of:: !Munoz-Perez, J.J.;: !Tejedor, L., and !Medina, R., 1999.: Equilibrium beach profile model for reef protected beaches.: Journal of Coastal Research, 15(4), 950-957.
    Smith, AWS
    JOURNAL OF COASTAL RESEARCH, 2001, 17 (01) : 241 - 242
1234