Name
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. |
Year | DOI | Venue |
|---|---|---|
2007 | 10.1007/s00165-006-0021-4 | Formal Asp. Comput. |
Keywords | Field | DocType |
temporal dependency,uppaal,complete verification,extended example,ravenscar profile,single step,engineering process,ada95,spark,rely/guarantee conditions,design verification,model checking,response time analysis,ravenscar restriction,single method,temporal behaviour,requirements analysis,real-time system,scheduling analysis,real time systems,requirement analysis | Spark (mathematics),Model checking,Computer science,Automaton,Requirements analysis,Ravenscar profile,Real-time computing,Verification,Real-time operating system,Engineering design process | Journal |
Volume | Issue | ISSN |
19 | 1 | 1433-299X |
Citations | PageRank | References |
6 | 0.52 | 26 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Alan Burns | 1 | 739 | 59.60 |
| T. -M. Lin | 2 | 6 | 0.52 |