Name
Abstract | ||
|---|---|---|
Following the trend to combine techniques to cover several facets of the development of modern systems, an integration of Z and CSP, called Circus, has been proposed as a refinement language; its relational model, based on the unifying theories of programming (UTP), justifies refinement in the context of both Z and CSP. In this paper, we introduce Circus Time, a timed extension of Circus, and present a new UTP time theory, which we use to give semantics to Circus Time and to validate some of its laws. In addition, we provide a framework for validation of timed programs based on FDR, the CSP model-checker. In this technique, a syntactic transformation strategy is used to split a timed program into two parallel components: an untimed program that uses timer events, and a collection of timers. We show that, with the timer events, it is possible to reason about time properties in the untimed language, and so, using FDR. Soundness is established using a Galois connection between the untimed UTP theory of Circus (and CSP) and our time theory. |
Year | DOI | Venue |
|---|---|---|
2010 | 10.1007/s00165-009-0119-6 | Formal Asp. Comput. |
Keywords | Field | DocType |
circus time,timer event,untimed utp theory,time property,untimed program,unifying theories of programming,relational models,process algebraic framework,galois connections,csp model-checker,untimed language,new utp time theory,time theory,csp,unifying theory,real-time system,relational model,real time systems,process algebra | Galois connection,Algebraic number,Programming language,Computer science,Theoretical computer science,Real-time operating system,Soundness,Timer,Relational model,Syntax,Semantics | Journal |
Volume | Issue | ISSN |
22 | 2 | 1433-299X |
Citations | PageRank | References |
30 | 1.07 | 31 |
Authors | ||
4 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Adnan Sherif | 1 | 83 | 5.26 |
| Ana Cavalcanti | 2 | 140 | 7.68 |
| He Jifeng | 3 | 1771 | 190.43 |
| Augusto Sampaio | 4 | 96 | 13.42 |