Formal specification and verification of a real-time kernel

17 December 2002

conference paper
Published by Institute of Electrical and Electronics Engineers (IEEE)

p. 205-211
https://doi.org/10.1109/emwrts.1994.336841

Abstract

The paper presents a case study of application of the VDM formal method to specification and verification of a simple real-time kernel. Specifications of selected external services of the kernel are presented. Then the verification methodology is introduced by demonstrating its basic steps in relation to verification of a selected function-a process waiting for a signal on a condition variable. The experience from the study is discussed.

Keywords

FORMAL SPECIFICATIONS
KERNEL
SYNCHRONIZATION
CONCRETE
SPECIFICATION LANGUAGES
LABORATORIES
DOCUMENTATION
PROGRAMMING PROFESSION
SOFTWARE DEVELOPMENT MANAGEMENT
COMMUNICATIONS TECHNOLOGY

This publication has 2 references indexed in Scilit:

mural: A Formal Development Support System
Published by Springer Nature ,1991
An axiomatic definition of the programming language PASCAL
Acta Informatica, 1973