On the Mechanized Validation of Infinite-State and Parameterized Reactive and Mobile Systems
Christine Röckl · mediaTUM – the media and publications repository of the Technical University Munich (Technical University Munich) · 2001
The growing in uence of telecommunication-systems in all areas has brought with it the need for elaborate and reliable software running on concurrent and, in particular, dynamically changing systems.With the development of such systems becoming ever more complex, the outline and development o f m e c hanized and mechanizable veri cation-techniques is indispensable.This overall goal can be divided into three tasks: (1) outline of a framework in which (2) complex systems can be analysed, and the (3) design and implementation of eÆcient prooftechniques.It is certainly beyond the scope of a thesis to provide an integrated framework dealing with these questions within one environment.This work therefore concentrates on dominant aspects of each of the three tasks in separate discussions.A major result of the thesis is that the approaches outlined for each of the three questions obviously t together, so that they can be used as a basis for the development of an integrated framework.Often an automatic veri cation of larger hardware-and software-applications is impossible, because the systems are too large or even in nite.This thesis focusses on in nite-state and parameterized systems, and builds tool-support on interactive theorem-proving.Further, it concentrates on the validation of correct implementations by exploiting behavioural reasoning.It demonstrates how to apply various techniques to tackle proofs about in nite-state and parameterized systems with large descriptions, discusses the support that theorem-provers can oer, and presents a foundational platform for reasoning about mobile systems in a general-purpose theorem-prover.Several design-decisions have to be taken.This thesis uses process-algebra as a framework, in particular CCS for the description and analysis of in nite-state reactive systems, and the -calculus for the discussion of mobile and higher-order systems.For a validation, it applies observation-equivalence, exploiting a range of proof-techniques that have been developed for the two calculi.The contributions of the thesis with respect to the three veri cation-tasks are as follows.(1) A formalization of the -calculus in Isabelle/HOL is presented.It uses a shallow embedding, in which -conversions and -reductions on names bound by input and restriction are dealt with by a -calculus provided by Isabelle.A shallow e m bedding has the advantage that substitutions do not have to be de ned and applied in a semantic analysis of the processes, like in a deep embedding; implementing substitutions in theorem-provers usually is a tedious task and prone to errors.On the other hand, syntax-analysis in shallow embeddings is intricate, because structural induction fails; further, exotic terms arise from an application of operators that do not belong to the -calculus, in de nitions of the continuations of an input or restriction.This thesis discusses how to mimic structural induction by rule-induction over a well-formedness predicate on processes which simultaneously rules out exotic terms.It discusses proof-techniques based on instantiations and re-abstractions of functions over processes, vi and uses them to derive vital syntactic properties of the -calculus.Finally, i t p r o ves that the shallow e m bedding is fully adequate with respect to a straightforward deep embedding.(2) The use of the -calculus to give semantics to higher-order imperative concurrent languages is studied.The thesis presents a translation of Concurrent Idealized Algol (CIA) into thecalculus, which i n tegrates previous encodings of imperative and concurrent features into CCS, and such of functional elements into the -calculus.It is proved by exhibiting an operational correspondence that the encoding is sound with respect to a straightforward small-step operational semantics of CIA employing a bisimulation-based operational congruence.The argument makes extensive use of proof-techniques such as bisimulation up to expansion and contextual reasoning.The encoding is then applied to validate classical benchmark laws and examples for CIA via a translation into the -calculus.Further, the thesis presents a correctness-proof for a more involved example employing procedures of higher order.This example emphasizes that the translation of programs from a higher-order syntax (CIA) into a rst-order syntax (-calculus) allows for a validation of examples that cannot be treated otherwise.Yet, even in the -calculus an application of involved proof-techniques|in particular, bisimulations up to expansion and context|is indispensable.During the last four years, many people have in uenced my life and work.First of all, I would like to thank my supervisors, Javier Esparza and Davide Sangiorgi, for accompanying this thesis.Many of the ideas discussed in this work are due to them.Their insistence on clarity and precision have made a great impression on me, and have certainly in uenced the development and presentation of this thesis.They have given me enduring support, and have taken my occasional stubbornness with patience.Further, I would like to express my gratitude to my head of chair, Wilfried Brauer, for creating an inspiring atmosphere in which I was able to dare my rst steps into research and teaching without having to bother about material questions.I h a ve a l w ays marvelled at his devotion and knowledge, and feel grateful for having him as a teacher and mentor.