Title | ||
---|---|---|
A framework for specification and validation of real-time systems using circus actions |
Abstract | ||
---|---|---|
In this work we propose a framework for specification and validation of real-time programs using Circus actions. Circus is a language that combines CSP, Z, and refinement calculus constructs. We have extended Circus and its model to capture time properties, and explored the relationship between the timed and the untimed model. Here we present a framework based on the integration of the timed and untimed versions of Circus. The integration aims at building a heterogeneous model that can express time properties using the untimed model. It is useful for the validation of real-time systems properties based on techniques and tools available for untimed languages. To illustrate the use of the framework, we apply it to an alarm system controller. |
Year | DOI | Venue |
---|---|---|
2004 | null | Lecture Notes in Computer Science |
Keywords | Field | DocType |
real-time program,untimed model,untimed language,time property,circus action,untimed version,heterogeneous model,real-time systems property,alarm system controller,refinement calculus construct,formal method,formal verification,real time systems,real time | System controller,Refinement calculus,Computer science,Real-time computing,Theoretical computer science,Formal verification | Conference |
Volume | Issue | ISSN |
3407 | null | null |
ISBN | Citations | PageRank |
3-540-25304-1 | 11 | 0.76 |
References | Authors | |
7 | 4 |
Name | Order | Citations | PageRank |
---|---|---|---|
Adnan Sherif | 1 | 83 | 5.26 |
He Jifeng | 2 | 1771 | 190.43 |
Ana Cavalcanti | 3 | 224 | 18.41 |
Augusto Sampaio | 4 | 96 | 13.42 |