- Abstract:
- In distributed real-time applications tasks on different nodes and components may require access to the same data. In the case of data replication, the data is duplicated on several components and procedures have to exist to ensure that the local copies of replicated data are kept temporally consistent. Further, different components of the system may have different temporal validity constraints for the same data, and as long as these constraints are satisfied overall system inconsistency is not harmful. We proposae the use of a formal analysis technique for guaranteeing temporal validity of replicated data. At the design level, we express general timing constraints on the temporal validity of data in UML's Object Constraint Language (OCL). To make this possible we provide a simple time-enriched liveness template for OCL. Further we can translate these OCL constraints into logical formulae. The logic is a real-time temporal logic of knowledge suitable for verification through model checking. It allows us to check that the shared data in the system is consistent "enough" and cannot be a source of failure. We illustrate the approach with an open dynamic real-time distributed system. The PDF is a link to the workshop version of the paper eventually the link will point to the full text when the paper is published.
- Links To Paper
- This is the workshop version of the paper - full reference when published
- Bibtex format
- @Article{EDI-INF-RR-0332,
- author = {
Juliana Bowles
and Stuart Anderson
},
- title = {On a time enriched OCL liveness template},
- journal = {International Journal on Software Tools for Technology Transfer (STTT)},
- publisher = {Springer},
- year = 2005,
- volume = {# 8(2)},
- pages = {156-166},
- doi = {10.1007/s10009-005-0210-0},
- url = {http://www-verimag.imag.fr/EVENTS/2003/SVERTS/PAPERS-WEB/18-Kuester-OCLRT.pdf},
- }
|