An engineering process for the verification of real-time systems |
| |
Authors: | A. Burns T. -M. Lin |
| |
Affiliation: | (1) Real-Time Systems Research Group, Department of Computer Science, The University of York, York, YO10 5DD, UK |
| |
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 |
本文献已被 SpringerLink 等数据库收录! |
|