Formal analysis of a real-time kernel specification

被引：0
|
作者：
Fowler, S
Wellings, A
机构：
来源：
FORMAL TECHNIQUES IN REAL-TIME AND FAULT-TOLERANT SYSTEMS | 1996年 / 1135卷
关键词：
D O I：
暂无
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
The specification of a red-time kernel and the analysis of certain properties of the kernel using the PVS system is presented in this paper. The kernel is designed to provide the minimal functionality to support real-time Ada 95 applications on a uniprocessor system, and the requirements for the kernel are derived from this. The specification consists of an abstract model of the functional and timing requirements for the kernel, and a minimal model of the system that the kernel is do signed to support. This system model allows properties such as mutual exclusion to be proved about the kernel with respect to certain assumptions about the system.
引用
收藏
页码：440 / 458
页数：19
相关论文
共 50 条
  • [21] Specification and Timing Analysis of Real-Time Systems
    Shuhua Wang
    Grace Tsai
    Real-Time Systems, 2004, 28 : 69 - 90
  • [22] Specification and analysis of real-time systems in statecharts
    Cha, SD
    Hong, HS
    SECOND WORKSHOP ON OBJECT-ORIENTED REAL-TIME DEPENDABLE SYSTEMS, PROCEEDINGS OF WORDS '96, 1996, : 137 - 143
  • [23] Specification and timing analysis of real-time systems
    Wang, SH
    Tsai, G
    REAL-TIME SYSTEMS, 2004, 28 (01) : 69 - 90
  • [24] Specification and analysis of real-time systems with PARAGON
    Sokolsky, O
    Lee, I
    Ben-Abdallah, H
    ANNALS OF SOFTWARE ENGINEERING, 1999, 7 : 211 - 234
  • [25] Formal analysis of real-time systems with SAM
    Yu, HQ
    He, XD
    Deng, Y
    Mo, LA
    FORMAL METHODS AND SOFTWARE ENGINEERING, PROCEEDINGS, 2002, 2495 : 275 - 286
  • [26] Cost monitoring and enforcement in the real-time specification for java']java - A formal evaluation
    dos Santos, OM
    Wellings, A
    RTSS 2005: 26TH IEEE INTERNATIONAL REAL-TIME SYSTEMS SYMPOSIUM, PROCEEDINGS, 2005, : 177 - 186
  • [27] Process activities for student projects involving the formal specification of real-time software
    Hilburn, TB
    REAL-TIME SYSTEMS EDUCATION, 1996, : 120 - 125
  • [28] A TLA+ Formal Specification and Verification of a New Real-Time Communication Protocol
    Regnier, Paul
    Lima, George
    Andrade, Aline
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2009, 240 : 221 - 238
  • [29] Formal Specification and Verification of a Protocol for Consistent Diagnosis in Real-Time Embedded Systems
    Barbosa, Raul
    Karlsson, Johan
    2008 INTERNATIONAL SYMPOSIUM ON INDUSTRIAL EMBEDDED SYSTEMS, 2008, : 192 - 199
  • [30] Zone-based formal specification and timing analysis of real-time self-adaptive systems
    Camilli, Matteo
    Gargantini, Angelo
    Scandurra, Patrizia
    SCIENCE OF COMPUTER PROGRAMMING, 2018, 159 : 28 - 57
12345