By the same authors

From the same journal

From the same journal

An engineering process for the verification of real-time systems

Research output: Contribution to journalArticle



Publication details

JournalFormal Aspects of Computing
DatePublished - Mar 2007
Issue number1
Number of pages25
Pages (from-to)111-136
Original languageEnglish


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.

    Research areas

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

Discover related content

Find related publications, people, projects, datasets and more using interactive charts.

View graph of relations