An engineering process for the verification of real-time systems

A. Burns; T. -M. Lin

doi:10.1007/s00165-006-0021-4

An engineering process for the verification of real-time systems

A. Burns, T. -M. Lin

Computer Science

Research output: Contribution to journal › Article › peer-review

Abstract

The complete verification of the timing properties of a large critical system cannot be undertaken in a single step or with a single method. In this paper we present a process that links together a number of techniques and approaches that cover all stages of development from requirements analysis to code testing. The key elements of the process are: a constrained form of timed automata that uses delay and deadline to define temporal behaviour, notions of rely and guarantee to cover temporal dependencies, model checking for design verification, SPARK and Ravenscar restrictions for programming, and scheduling and response time analysis for asserting implementation compliance. Extended examples of the use of the process are given.

Original language	English
Pages (from-to)	111-136
Number of pages	25
Journal	Formal Aspects of Computing
Volume	19
Issue number	1
DOIs	https://doi.org/10.1007/s00165-006-0021-4
Publication status	Published - Mar 2007

Keywords

scheduling analysis
Ravenscar profile
model checking
UPPAAL
SPARK
Ada95
rely/guarantee conditions
EXECUTION TIMES

Access to Document

10.1007/s00165-006-0021-4

http://dx.doi.org/10.1007/s00165-006-0021-4

Cite this

@article{c56aba09ede34c92b95c4cd3866771b5,

title = "An engineering process for the verification of real-time systems",

abstract = "The complete verification of the timing properties of a large critical system cannot be undertaken in a single step or with a single method. In this paper we present a process that links together a number of techniques and approaches that cover all stages of development from requirements analysis to code testing. The key elements of the process are: a constrained form of timed automata that uses delay and deadline to define temporal behaviour, notions of rely and guarantee to cover temporal dependencies, model checking for design verification, SPARK and Ravenscar restrictions for programming, and scheduling and response time analysis for asserting implementation compliance. Extended examples of the use of the process are given.",

keywords = "scheduling analysis, Ravenscar profile, model checking, UPPAAL, SPARK, Ada95, rely/guarantee conditions, EXECUTION TIMES",

author = "A. Burns and Lin, {T. -M.}",

year = "2007",

month = mar,

doi = "10.1007/s00165-006-0021-4",

language = "English",

volume = "19",

pages = "111--136",

journal = "Formal Aspects of Computing",

issn = "0934-5043",

publisher = "ACM",

number = "1",

}

TY - JOUR

T1 - An engineering process for the verification of real-time systems

AU - Burns, A.

AU - Lin, T. -M.

PY - 2007/3

Y1 - 2007/3

N2 - The complete verification of the timing properties of a large critical system cannot be undertaken in a single step or with a single method. In this paper we present a process that links together a number of techniques and approaches that cover all stages of development from requirements analysis to code testing. The key elements of the process are: a constrained form of timed automata that uses delay and deadline to define temporal behaviour, notions of rely and guarantee to cover temporal dependencies, model checking for design verification, SPARK and Ravenscar restrictions for programming, and scheduling and response time analysis for asserting implementation compliance. Extended examples of the use of the process are given.

AB - The complete verification of the timing properties of a large critical system cannot be undertaken in a single step or with a single method. In this paper we present a process that links together a number of techniques and approaches that cover all stages of development from requirements analysis to code testing. The key elements of the process are: a constrained form of timed automata that uses delay and deadline to define temporal behaviour, notions of rely and guarantee to cover temporal dependencies, model checking for design verification, SPARK and Ravenscar restrictions for programming, and scheduling and response time analysis for asserting implementation compliance. Extended examples of the use of the process are given.

KW - scheduling analysis

KW - Ravenscar profile

KW - model checking

KW - UPPAAL

KW - SPARK

KW - Ada95

KW - rely/guarantee conditions

KW - EXECUTION TIMES

U2 - 10.1007/s00165-006-0021-4

DO - 10.1007/s00165-006-0021-4

M3 - Article

SN - 0934-5043

VL - 19

SP - 111

EP - 136

JO - Formal Aspects of Computing

JF - Formal Aspects of Computing

IS - 1

ER -