Name
Abstract | ||
|---|---|---|
We present a pattern-based method to express time specifications in the language TLA +. A real-time module RealTimeNew is introduced to encapsulate the definitions of commonly used time patterns. We present a general framework to differentiate the temporal characterizations from system functionality with time constraints. The temporal specification is concise and provably as a refinement of its corresponding functional description without time. The method ameliorates the usability of TLA + in specifying and verifying time-sensitive systems. A case study is harnessed to illustrate and validate the approach. © 2010 IEEE. |
Year | DOI | Venue |
|---|---|---|
2010 | 10.1109/COMPSAC.2010.50 | Proceedings - International Computer Software and Applications Conference |
Keywords | Field | DocType |
Real-time,Refinement,Specification,TLA+ | Time patterns,Programming language,Formal language,Computer science,Upper and lower bounds,Usability,Time sensitive,Real-time computing,Formal specification,Software,Functional description | Conference |
Volume | Issue | ISSN |
null | null | null |
ISBN | Citations | PageRank |
978-0-7695-4085-6 | 0 | 0.34 |
References | Authors | |
5 | 3 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Hehua Zhang | 1 | 109 | 12.65 |
| Ming Gu | 2 | 554 | 74.82 |
| Xiaoyu Song | 3 | 471 | 51.61 |