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 条
  • [31] Real time formal specification using VDM(++)
    vanKatwijk, J
    Durr, E
    Goldsack, S
    SECOND WORKSHOP ON OBJECT-ORIENTED REAL-TIME DEPENDABLE SYSTEMS, PROCEEDINGS OF WORDS '96, 1996, : 17 - 24
  • [32] SPECIFICATION OF REAL-TIME SYSTEMS
    PATNAIK, LM
    MALL, R
    INTERNATIONAL JOURNAL OF SOFTWARE ENGINEERING AND KNOWLEDGE ENGINEERING, 1993, 3 (02) : 267 - 285
  • [33] Real-time specification patterns
    Konrad, S
    Cheng, BHC
    ICSE 05: 27TH INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING, PROCEEDINGS, 2005, : 372 - 381
  • [34] A real-time specification language
    do Amaral, FN
    Haeusler, EH
    Endler, M
    ADVANCES IN LOGIC, ARTIFICIAL INTELLIGENCE AND ROBOTICS, 2002, 85 : 194 - 201
  • [35] Formal modeling for a real-time scheduler and schedulability analysis
    Kim, SJ
    Choi, JY
    PARALLEL COMPUTING TECHNOLOGIES, PROCEEDINGS, 2003, 2763 : 253 - 258
  • [36] Formal Analysis of Sporadic Bursts in Real-Time Systems
    Quinton, Sophie
    Negrean, Mircea
    Ernst, Rolf
    DESIGN, AUTOMATION & TEST IN EUROPE, 2013, : 767 - 772
  • [37] Formal Analysis of Sporadic Overload in Real-Time Systems
    Quinton, Sophie
    Hanke, Matthias
    Ernst, Rolf
    DESIGN, AUTOMATION & TEST IN EUROPE (DATE 2012), 2012, : 515 - 520
  • [38] The TASM toolset: Specification, simulation, and formal verification of real-time systems - (Tool paper)
    Ouimet, Martin
    Lundqvist, Kristina
    COMPUTER AIDED VERIFICATION, PROCEEDINGS, 2007, 4590 : 126 - +
  • [39] A formal approach to the specification and the behavior validation of real-time systems based on rewriting logic
    Attoui, A
    Schneider, M
    REAL-TIME SYSTEMS, 1996, 10 (01) : 5 - 22
  • [40] Formal Specification for Compiler Based Test Case Generation of Embedded Real-Time System
    Chen, Yong
    He, Yanxiang
    Xu, Chao
    Wu, Wei
    Liu, Jianbo
    BUSINESS, ECONOMICS, FINANCIAL SCIENCES, AND MANAGEMENT, 2012, 143 : 643 - 650
12345