|
|
Modelling Techniques for Evolving Distributed ApplicationsSeveral 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 the 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 (standing for Refinement
Language.} in this paper that provides syntactic as well as semantic
support for modelling incremental changes. In particular, the language provides two new
mechanisms, called type derivation and module derivation that work in
conjunction to support evolution. We illustrate the power and convenience of these
mechanisms through examples. Based on these Based on the language mechanisms, we then
present a method for automatically carrying over properties after refinement, provided the
refinement meets certain criteria. We also present algorithms 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. For properties
that cannot be carried over in this manner, or to establish additional properties that
hold only for the refined specification, we can make use of traditional algorithms and
techniques for validation of finite state automata. In order to accomplish this, we
present algorithms for compiling RL specifications into such automata. |
|
Maintained by Sekar, sekar@cs.sunysb.edu |