Addressing architectural and mobility considerations in the formal specification and design of concurrent systems

As the use of computer systems in critical application areas continues to rise, there is an increasing need for approaches which can deliver dependable software. Formal methods offer one possible venue for achieving the required dependability. Program derivation is a formal design technique which attempts to guarantee that programs are correct by construction. Software design becomes a process of refining a formal specification of the system's requirements via transformations which can be proven to be correct. This thesis is concerned with the applicability of program derivation methods to two classes of systems: (1) systems in which one must prove formally the compatibility between the application software and the underlying hardware architecture, and (2) systems composed of autonomous, mobile components whose interactions are location dependent. We show that technical issues which are important to these two classes of systems can be addressed within the context provided by an existing formal model of concurrent computations combined with a tailored methodological approach rooted in program derivation. The approach emphasizes the development of abstractions germane to the specific problem area, along with a careful organization of the refinement process in an effort to minimize the need for complete proofs after every refinement. This study increases our understanding of the fundamental issues in the specification and design of software systems and is expected to contribute to the emergence of industrial-grade methodologies and tools.