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 条
  • [21] Approach for transforming Ada83 serving tasks to Ada95 protected objects
    Li, Bangqing
    Xu, Baowen
    Ruan Jian Xue Bao/Journal of Software, 2000, 11 (06): : 836 - 840
  • [22] Ada95 protected objects and data-oriented synchronization
    Jisuanji Yanjiu yu Fazhan, 1 (72-77):
  • [23] Integrating object-oriented programming and protected objects in Ada 95
    Wellings, AJ
    ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 2000, 22 (03): : 506 - 539
  • [24] Ada-I: An extension language supporting inheritance of protected objects based on Ada95
    Lu, Jia
    Wen, Dongchan
    Wang, Dingxing
    Ruan Jian Xue Bao/Journal of Software, 2000, 11 (04): : 494 - 501
  • [25] A FORMAL MODEL FOR LEARNING OBJECTS
    Perez-Lezama, Claudia V.
    Alfredo Sanchez, J.
    EDULEARN10: INTERNATIONAL CONFERENCE ON EDUCATION AND NEW LEARNING TECHNOLOGIES, 2010, : 15 - 24
  • [26] Design-space evaluation for non-blocking synchronization in Ada: lock elision of protected objects, concurrent objects, and low-level atomics
    Yang, Shinhyung
    Jeong, Seongho
    Min, Byunguk
    Kim, Yeonsoo
    Burgstaller, Bernd
    Blieberger, Johann
    JOURNAL OF SYSTEMS ARCHITECTURE, 2020, 110
  • [27] Equilibrium beach profile model for reef-protected beaches
    Muñóz-Pérez, JJ
    Tejedor, L
    Medina, R
    JOURNAL OF COASTAL RESEARCH, 1999, 15 (04) : 950 - 957
  • [28] Meta objects for access control: A formal model for role-based principals
    Riechmann, T
    Hauck, FJ
    NEW SECURITY PARADIGMS WOEKSHOP, PROCEEDINGS, 1999, : 30 - 38
  • [29] A formal model describing topological relations between spatial linear objects in GIS-T
    Zhang Shuijian
    Li Yongshu
    GEOINFORMATICS 2008 AND JOINT CONFERENCE ON GIS AND BUILT ENVIRONMENT: ADVANCED SPATIAL DATA MODELS AND ANALYSES, PARTS 1 AND 2, 2009, 7146
  • [30] Impact of pedestrian on the speed and acceleration profile model to the protected left-turn traffic
    Chen, Yi-Xin
    He, Yu-Long
    Sun, Xiao-Duan
    Xu, Ting
    Jiaotong Yunshu Xitong Gongcheng Yu Xinxi/Journal of Transportation Systems Engineering and Information Technology, 2015, 15 (01): : 198 - 204
1234