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 Sherif1835.26
He Jifeng21771190.43
Ana Cavalcanti322418.41
Augusto Sampaio49613.42