Abstract:
Several languages and techniques have been proposed for formal specification and validation of concurrent systems. However, these techniques provide no support for modelling incremental changes that take place during software development, such as successive refinements that take place during the design phase or changes that take place later on as a result of software evolution. Consequently, any changes to the system model need to be incorporated by manual editing of system specification, which is cumbersome and error-prone. Moreover, editing being an uncontrolled process, there is no way to automatically carry over (most of the) correctness properties after minor changes to the system. These factors can make formal approaches very expensive for large and evolving systems. To alleviate this problem, we present a language RL (Refinement Language) in this paper that provides syntactic as well as semantic support for modelling incremental changes. Based on the language mechanisms, we then present a method for automatically carrying over properties after refinement. We also present algortihms for compiling RL specifications into finite state automata (FSA) that can be analyzed using traditional algorithms for establishing new properties that hold only after refinement.
Bibtex Entry:
@inproceedings{SLR:FORTE94, author = {R. Sekar and Yow-Jian Lin and C. R. Ramakrishnan}, title = {Modelling techniques for evolving distributed applications}, booktitle = {Seventh IFIP WG6.1 International Conference on Formal Description Techniques ({FORTE})}, publisher = {Chapman {\&} Hall}, pages = {461--476}, year = {1994} }
| Full Paper: | [pdf] |
C. R. Ramakrishnan
(cram@cs.sunysb.edu)